Re: [mizar] Union of two subgroups

[Victor Makarov <viktmak@gmail.com>]

Thanks a lot! 

On Fri, Nov 20, 2020 at 3:41 AM Coghetto Roland <roland_coghetto@hotmail.com> 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 : owner-mizar-forum@mizar.uwb.edu.pl <owner-mizar-forum@mizar.uwb.edu.pl> de la part de Victor Makarov <viktmak@gmail.com>
Envoyé : mercredi 18 novembre 2020 04:13
À : mizar-forum@mizar.uwb.edu.pl <mizar-forum@mizar.uwb.edu.pl>
Objet : Re: [mizar] Union of two subgroups

 

Thanks, I'll check them out. 

On Tue, Nov 17, 2020 at 7:51 AM Adam Naumowicz <adamn@math.uwb.edu.pl> 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: adamn@mizar.org
Ciolkowskiego 1M, 15-245 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
===========================================================================