RE: Union of two subgroups

Dear Viktor,

For the first question. (My source: ex.: https://math.stackexchange.com/questions/2386730/prove-that-the-union-of-two-subgroups-is-a-subgroup-iff-one-is-contained-in-othe/2386760)

Kind regards.

Roland

===========
environ

 vocabularies XBOOLE_0, STRUCT_0, SUBSET_1, GROUP_1, RELAT_1, TARSKI, ALGSTR_0,
      BINOP_1, REALSET1, ZFMISC_1, FUNCT_1, GROUP_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REALSET1, STRUCT_0, ALGSTR_0,
      GROUP_1, BINOP_1, FUNCT_1, RELSET_1, GROUP_2;
 constructors NAT_1, REALSET1, RELSET_1, GROUP_4;
 registrations RELSET_1, STRUCT_0, GROUP_1, XBOOLE_0, GROUP_2;
 requirements BOOLE, SUBSET;
 definitions TARSKI;
 equalities BINOP_1, REALSET1, ALGSTR_0;
 expansions STRUCT_0, TARSKI;
 theorems FUNCT_1, FUNCT_2, GROUP_1, ZFMISC_1, RELAT_1, XBOOLE_0, XBOOLE_1,
      GROUP_2, REALSET1;

begin

theorem
  for G being Group
  for H,K being Subgroup of G st
  the carrier of H c= the carrier of K or
  the carrier of K c= the carrier of H holds
  ex HK being Subgroup of G st
  the carrier of HK = (the carrier of H) \/ (the carrier of K)
  proof
    let G be Group;
    let H,K be Subgroup of G;
    assume that
A1: the carrier of H c= the carrier of K or
      the carrier of K c= the carrier of H;
    set X = (the carrier of H) \/ (the carrier of K);
    set B = (the multF of G)||X;
    reconsider M = the multF of G as BinOp of the carrier of G;
    X c= the carrier of G
    proof
      let x be object;
      assume x in X;
      then
A2:   x in the carrier of H or x in the carrier of K by XBOOLE_0:def 3;
      the carrier of H c= the carrier of G &
        the carrier of K c= the carrier of G by GROUP_2:def 5;
      hence thesis by A2;
    end;
    then reconsider X as Subset of the carrier of G;
    now
      let x be set;
      assume x in [:X,X:];
      then consider y,z be object such that
A3:   y in X and
A4:   z in X and
A5:   x = [y,z] by ZFMISC_1:def 2;
A6:   the carrier of H c= the carrier of G &
        the carrier of K c= the carrier of G by GROUP_2:def 5;
      per cases by A3,XBOOLE_0:def 3;
      suppose y in the carrier of H;
        then reconsider y as Element of H;
        per cases by A4,XBOOLE_0:def 3;
        suppose z in the carrier of H;
          then reconsider z as Element of H;
          reconsider y9 = y, z9 = z as Element of G by A6;
          M.x = y9 * z9 by A5
             .= y * z by GROUP_2:43;
          hence M.x in X by XBOOLE_0:def 3;
        end;
        suppose
A7:       z in the carrier of K;
          per cases by A1;
          suppose the carrier of H c= the carrier of K;
            then reconsider y,z as Element of K by A7;
            reconsider y9 = y, z9 = z as Element of G by A6;
            M.x = y9 * z9 by A5
               .= y * z by GROUP_2:43;
            hence M.x in X by XBOOLE_0:def 3;
          end;
          suppose the carrier of K c= the carrier of H;
            then reconsider y,z as Element of H by A7;
            reconsider y9 = y, z9 = z as Element of G by A6;
            M.x = y9 * z9 by A5
               .= y * z by GROUP_2:43;
            hence M.x in X by XBOOLE_0:def 3;
          end;
        end;
      end;
      suppose y in the carrier of K;
        then reconsider y as Element of K;
        per cases by A4,XBOOLE_0:def 3;
        suppose z in the carrier of H;
          then reconsider z as Element of H;
          per cases by A1;
          suppose the carrier of H c= the carrier of K;
            then reconsider y,z as Element of K;
            reconsider y9 = y, z9 = z as Element of G by A6;
            M.x = y9 * z9 by A5
               .= y * z by GROUP_2:43;
            hence M.x in X by XBOOLE_0:def 3;
          end;
          suppose the carrier of K c= the carrier of H;
            then reconsider y,z as Element of H;
            reconsider y9 = y, z9 = z as Element of G by A6;
            M.x = y9 * z9 by A5
               .= y * z by GROUP_2:43;
            hence M.x in X by XBOOLE_0:def 3;
          end;
        end;
        suppose z in the carrier of K;
          then reconsider z as Element of K;
          reconsider y9 = y, z9 = z as Element of G by A6;
          M.x = y9 * z9 by A5
             .= y * z by GROUP_2:43;
          hence M.x in X by XBOOLE_0:def 3;
        end;
      end;
    end;
    then X is M-binopclosed by REALSET1:def 1;
    then reconsider B as BinOp of X by REALSET1:2;
    set HK = multMagma (# X,B #);
    1_H in HK by XBOOLE_0:def 3;
    then reconsider e = 1_G as Element of HK by GROUP_2:44;
    now
      let h be Element of HK;
A9:   dom ((the multF of G)|[:X,X:]) = dom (the multF of G) /\ [:X,X:]
        by RELAT_1:61
                                    .= [:the carrier of G,the carrier of G:]
                                         /\ [:X,X:] by FUNCT_2:def 1
                                    .= [:X,X:] by XBOOLE_1:28,ZFMISC_1:96;
      then
A10:  [h,e] in dom ((the multF of G)|[:X,X:]) &
        [e,h] in dom ((the multF of G)|[:X,X:])
        by ZFMISC_1:def 2;
      the carrier of HK c= the carrier of G;
      then reconsider h9 = h, e9 = e as Element of G;
      thus h = h9 * e9 by GROUP_1:def 4
            .= h * e by A10,FUNCT_1:47;
      thus h = e9 * h9 by GROUP_1:def 4
            .= e * h by A10,FUNCT_1:47;
      per cases by XBOOLE_0:def 3;
      suppose h in H;
        then reconsider h99 = h as Element of H;
        reconsider gg = h99" as Element of HK by XBOOLE_0:def 3;
        h99" = h9" by GROUP_2:48;
        then reconsider hk = h9" as Element of X by XBOOLE_0:def 3;
A11:    [h9,hk] in dom ((the multF of G)|[:X,X:]) &
          [hk,h9] in dom ((the multF of G)|[:X,X:])
          by A9,ZFMISC_1:def 2;
A12:    h99" = h9" by GROUP_2:48;
A13:    h99 * h99" = 1_H & h99" * h99 = 1_H by GROUP_1:def 5;
        now
          thus e = h99 * h99" by A13,GROUP_2:44
                .= h9 * h9" by A12,GROUP_2:43
                .= B.[h9,h9"] by A11,FUNCT_1:47
                .= h * gg by GROUP_2:48;
          thus e = h99" * h99 by A13,GROUP_2:44
                .= h9" * h9 by A12,GROUP_2:43
                .= B.[h9",h9] by A11,FUNCT_1:47
                .= gg * h by GROUP_2:48;
        end;
        hence ex g be Element of HK st h * g = e & g * h = e;
      end;
      suppose h in K;
        then reconsider h99 = h as Element of K;
        reconsider gg = h99" as Element of HK by XBOOLE_0:def 3;
        h99" = h9" by GROUP_2:48;
        then reconsider hk = h9" as Element of X by XBOOLE_0:def 3;
A14:    [h9,hk] in dom ((the multF of G)|[:X,X:]) &
          [hk,h9] in dom ((the multF of G)|[:X,X:])
          by A9,ZFMISC_1:def 2;
A15:    h99" = h9" by GROUP_2:48;
A16:    h99 * h99" = 1_K & h99" * h99 = 1_K by GROUP_1:def 5;
        now
          thus e = h99 * h99" by A16,GROUP_2:44
                .= h9 * h9" by A15,GROUP_2:43
                .= B.[h9,h9"] by A14,FUNCT_1:47
                .= h * gg by GROUP_2:48;
          thus e = h99" * h99 by A16,GROUP_2:44
                .= h9" * h9 by A15,GROUP_2:43
                .= B.[h9",h9] by A14,FUNCT_1:47
                .= gg * h by GROUP_2:48;
        end;
        hence ex g be Element of HK st h * g = e & g * h = e;
      end;
    end;
    then reconsider HK as non empty Group-like multMagma by GROUP_1:def 2;
    reconsider HK as Subgroup of G by GROUP_2:def 5;
    the carrier of HK = (the carrier of H) \/ (the carrier of K);
    hence thesis;
  end;

theorem
  for G being Group for H,K,HK being Subgroup of G st
  the carrier of HK = (the carrier of H) \/ (the carrier of K) holds
  the carrier of H c= the carrier of K or
  the carrier of K c= the carrier of H
  proof
    let G be Group;
    let H,K,HK be Subgroup of G;
    assume that
A1: the carrier of HK = (the carrier of H) \/ (the carrier of K);
    assume that
A2: not the carrier of H c= the carrier of K and
A3: not the carrier of K c= the carrier of H;
    ex x be Element of H st not x is Element of K
    proof
      assume
A4:   for x be Element of H holds x is Element of K;
      now
        let x be set;
        assume x in the carrier of H;
        then x is Element of K by A4;
        hence x in the carrier of K;
      end;
      hence thesis by A2;
    end;
    then consider h be Element of H such that
A5: not h is Element of K;
    ex x be Element of K st not x is Element of H
    proof
      assume
A6:   for x be Element of K holds x is Element of H;
      now
        let x be set;
        assume x in the carrier of K;
        then x is Element of H by A6;
        hence x in the carrier of H;
      end;
      hence thesis by A3;
    end;
    then consider k be Element of K such that
A7: not k is Element of H;
    the carrier of H c= the carrier of HK &
      the carrier of K c= the carrier of HK by A1,XBOOLE_0:def 3;
    then
A8: H is Subgroup of HK & K is Subgroup of HK by GROUP_2:57;
    reconsider h9 = h, k9 = k as Element of HK by A1,XBOOLE_0:def 3;
    set u = k9 * h9;
    per cases by A1,XBOOLE_0:def 3;
    suppose u in the carrier of H;
      then reconsider u9 = u as Element of H;
A9:   h9" = h" by A8,GROUP_2:48;
      k9 = k9 * 1_HK by GROUP_1:def 4
        .= k9 * (h9 * h9") by GROUP_1:def 5
        .= u * h9" by GROUP_1:def 3
        .= u9 * h" by A8,A9,GROUP_2:43;
      hence thesis by A7;
    end;
    suppose u in the carrier of K;
      then reconsider u9 = u as Element of K;
A10:  k9" = k" by A8,GROUP_2:48;
      h9 = 1_HK * h9 by GROUP_1:def 4
        .= (k9" * k9) * h9 by GROUP_1:def 5
        .= k9" * u by GROUP_1:def 3
        .= k" * u9 by A8,A10,GROUP_2:43;
      hence thesis by A5;
    end;
  end;




________________________________
De : [email protected] <[email protected]> de la part de Victor Makarov <[email protected]>
Envoyé : mercredi 18 novembre 2020 04:13
À : [email protected] <[email protected]>
Objet : Re: [mizar] Union of two subgroups

Thanks, I'll check them out.

On Tue, Nov 17, 2020 at 7:51 AM Adam Naumowicz <[email protected]<mailto:[email protected]>> wrote:
Dear Victor,

On Mon, 16 Nov 2020, Victor Makarov wrote:

> Dear All:
>
> I cannot find in MML a theorem that the union of two subgroups is  a
> subgroup iff  one of the subgroups is a subset of the other subgroup.
>
> The same question about the product of two subgroups H and K:
>
> H*K is a subgroup iff H*K = K*H.

This may not be exactly what you want, but have you checked these
theorems:

theorem :: GROUP_4:50
   H1 "\/" H2 = gr(H1 * H2);

theorem :: GROUP_4:51
   H1 * H2 = H2 * H1 implies the carrier of H1 "\/" H2 = H1 * H2;

?

Best regards,

Adam Naumowicz

===========================================================================
Division of Programming and Formal Methods   Fax: +48(85)738-83-33
Institute of Computer Science                Tel: +48(85)738-83-06 (office)
University of Bialystok                      E-mail: [email protected]<mailto:[email protected]>
Ciolkowskiego 1M, 15-245 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
===========================================================================