Re: Union of two subgroups

Thanks a lot!

On Fri, Nov 20, 2020 at 3:41 AM Coghetto Roland <[email protected]>
wrote:

> 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]>
> 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]
> Ciolkowskiego 1M, 15-245 Bialystok, Poland
> http://math.uwb.edu.pl/~adamn/
> ===========================================================================
>
>