latsubgr.miz



    begin

    theorem :: LATSUBGR:1

    

     Th1: for G be Group holds for H1,H2 be Subgroup of G holds the carrier of (H1 /\ H2) = (the carrier of H1 /\ the carrier of H2)

    proof

      let G be Group;

      let H1,H2 be Subgroup of G;

      the carrier of H2 = ( carr H2) by GROUP_2:def 9;

      then (the carrier of H1 /\ the carrier of H2) = (( carr H1) /\ ( carr H2)) by GROUP_2:def 9;

      hence thesis by GROUP_2:def 10;

    end;

    theorem :: LATSUBGR:2

    

     Th2: for G be Group holds for h be set holds h in ( Subgroups G) iff ex H be strict Subgroup of G st h = H

    proof

      let G be Group;

      let h be set;

      thus h in ( Subgroups G) implies ex H be strict Subgroup of G st h = H

      proof

        assume h in ( Subgroups G);

        then h is strict Subgroup of G by GROUP_3:def 1;

        hence thesis;

      end;

      thus thesis by GROUP_3:def 1;

    end;

    theorem :: LATSUBGR:3

    

     Th3: for G be Group holds for A be Subset of G holds for H be strict Subgroup of G st A = the carrier of H holds ( gr A) = H

    proof

      let G be Group;

      let A be Subset of G;

      let H be strict Subgroup of G such that

       A1: A = the carrier of H;

      ( gr ( carr H)) = H by GROUP_4: 31;

      hence thesis by A1, GROUP_2:def 9;

    end;

    theorem :: LATSUBGR:4

    

     Th4: for G be Group holds for H1,H2 be Subgroup of G holds for A be Subset of G st A = (the carrier of H1 \/ the carrier of H2) holds (H1 "\/" H2) = ( gr A)

    proof

      let G be Group;

      let H1,H2 be Subgroup of G;

      

       A1: the carrier of H2 = ( carr H2) by GROUP_2:def 9;

      let A be Subset of G;

      assume A = (the carrier of H1 \/ the carrier of H2);

      hence thesis by A1, GROUP_2:def 9;

    end;

    theorem :: LATSUBGR:5

    

     Th5: for G be Group holds for H1,H2 be Subgroup of G holds for g be Element of G holds g in H1 or g in H2 implies g in (H1 "\/" H2)

    proof

      let G be Group;

      let H1,H2 be Subgroup of G;

      let g be Element of G;

      assume

       A1: g in H1 or g in H2;

      now

        per cases by A1;

          suppose

           A2: g in H1;

          the carrier of H1 c= the carrier of G & the carrier of H2 c= the carrier of G by GROUP_2:def 5;

          then

          reconsider A = (the carrier of H1 \/ the carrier of H2) as Subset of G by XBOOLE_1: 8;

          g in the carrier of H1 by A2, STRUCT_0:def 5;

          then g in A by XBOOLE_0:def 3;

          then g in ( gr A) by GROUP_4: 29;

          hence thesis by Th4;

        end;

          suppose

           A3: g in H2;

          the carrier of H1 c= the carrier of G & the carrier of H2 c= the carrier of G by GROUP_2:def 5;

          then

          reconsider A = (the carrier of H1 \/ the carrier of H2) as Subset of G by XBOOLE_1: 8;

          g in the carrier of H2 by A3, STRUCT_0:def 5;

          then g in A by XBOOLE_0:def 3;

          then g in ( gr A) by GROUP_4: 29;

          hence thesis by Th4;

        end;

      end;

      hence thesis;

    end;

    theorem :: LATSUBGR:6

    for G1,G2 be Group holds for f be Homomorphism of G1, G2 holds for H1 be Subgroup of G1 holds ex H2 be strict Subgroup of G2 st the carrier of H2 = (f .: the carrier of H1)

    proof

      let G1,G2 be Group;

      let f be Homomorphism of G1, G2;

      let H1 be Subgroup of G1;

      reconsider y = (f . ( 1_ G1)) as Element of G2;

      

       A1: for g be Element of G2 st g in (f .: the carrier of H1) holds (g " ) in (f .: the carrier of H1)

      proof

        let g be Element of G2;

        assume g in (f .: the carrier of H1);

        then

        consider x be Element of G1 such that

         A2: x in the carrier of H1 and

         A3: g = (f . x) by FUNCT_2: 65;

        x in H1 by A2, STRUCT_0:def 5;

        then (x " ) in H1 by GROUP_2: 51;

        then

         A4: (x " ) in the carrier of H1 by STRUCT_0:def 5;

        (f . (x " )) = ((f . x) " ) by GROUP_6: 32;

        hence thesis by A3, A4, FUNCT_2: 35;

      end;

      

       A5: for g1,g2 be Element of G2 st g1 in (f .: the carrier of H1) & g2 in (f .: the carrier of H1) holds (g1 * g2) in (f .: the carrier of H1)

      proof

        let g1,g2 be Element of G2;

        assume that

         A6: g1 in (f .: the carrier of H1) and

         A7: g2 in (f .: the carrier of H1);

        consider x be Element of G1 such that

         A8: x in the carrier of H1 and

         A9: g1 = (f . x) by A6, FUNCT_2: 65;

        consider y be Element of G1 such that

         A10: y in the carrier of H1 and

         A11: g2 = (f . y) by A7, FUNCT_2: 65;

        

         A12: y in H1 by A10, STRUCT_0:def 5;

        x in H1 by A8, STRUCT_0:def 5;

        then (x * y) in H1 by A12, GROUP_2: 50;

        then

         A13: (x * y) in the carrier of H1 by STRUCT_0:def 5;

        (f . (x * y)) = ((f . x) * (f . y)) by GROUP_6:def 6;

        hence thesis by A9, A11, A13, FUNCT_2: 35;

      end;

      ( 1_ G1) in H1 by GROUP_2: 46;

      then ( dom f) = the carrier of G1 & ( 1_ G1) in the carrier of H1 by FUNCT_2:def 1, STRUCT_0:def 5;

      then y in (f .: the carrier of H1) by FUNCT_1:def 6;

      then

      consider H2 be strict Subgroup of G2 such that

       A14: the carrier of H2 = (f .: the carrier of H1) by A1, A5, GROUP_2: 52;

      take H2;

      thus thesis by A14;

    end;

    theorem :: LATSUBGR:7

    for G1,G2 be Group holds for f be Homomorphism of G1, G2 holds for H2 be Subgroup of G2 holds ex H1 be strict Subgroup of G1 st the carrier of H1 = (f " the carrier of H2)

    proof

      let G1,G2 be Group;

      let f be Homomorphism of G1, G2;

      let H2 be Subgroup of G2;

      

       A1: for g be Element of G1 st g in (f " the carrier of H2) holds (g " ) in (f " the carrier of H2)

      proof

        let g be Element of G1;

        assume g in (f " the carrier of H2);

        then (f . g) in the carrier of H2 by FUNCT_2: 38;

        then (f . g) in H2 by STRUCT_0:def 5;

        then ((f . g) " ) in H2 by GROUP_2: 51;

        then (f . (g " )) in H2 by GROUP_6: 32;

        then (f . (g " )) in the carrier of H2 by STRUCT_0:def 5;

        hence thesis by FUNCT_2: 38;

      end;

      

       A2: for g1,g2 be Element of G1 st g1 in (f " the carrier of H2) & g2 in (f " the carrier of H2) holds (g1 * g2) in (f " the carrier of H2)

      proof

        let g1,g2 be Element of G1;

        assume that

         A3: g1 in (f " the carrier of H2) and

         A4: g2 in (f " the carrier of H2);

        (f . g2) in the carrier of H2 by A4, FUNCT_2: 38;

        then

         A5: (f . g2) in H2 by STRUCT_0:def 5;

        (f . g1) in the carrier of H2 by A3, FUNCT_2: 38;

        then (f . g1) in H2 by STRUCT_0:def 5;

        then ((f . g1) * (f . g2)) in H2 by A5, GROUP_2: 50;

        then (f . (g1 * g2)) in H2 by GROUP_6:def 6;

        then (f . (g1 * g2)) in the carrier of H2 by STRUCT_0:def 5;

        hence thesis by FUNCT_2: 38;

      end;

      ( 1_ G2) in H2 by GROUP_2: 46;

      then ( 1_ G2) in the carrier of H2 by STRUCT_0:def 5;

      then (f . ( 1_ G1)) in the carrier of H2 by GROUP_6: 31;

      then (f " the carrier of H2) <> {} by FUNCT_2: 38;

      then

      consider H1 be strict Subgroup of G1 such that

       A6: the carrier of H1 = (f " the carrier of H2) by A1, A2, GROUP_2: 52;

      take H1;

      thus thesis by A6;

    end;

    theorem :: LATSUBGR:8

    for G1,G2 be Group holds for f be Homomorphism of G1, G2 holds for H1,H2 be Subgroup of G1 holds for H3,H4 be Subgroup of G2 st the carrier of H3 = (f .: the carrier of H1) & the carrier of H4 = (f .: the carrier of H2) holds H1 is Subgroup of H2 implies H3 is Subgroup of H4

    proof

      let G1,G2 be Group;

      let f be Homomorphism of G1, G2;

      let H1,H2 be Subgroup of G1;

      let H3,H4 be Subgroup of G2 such that

       A1: the carrier of H3 = (f .: the carrier of H1) & the carrier of H4 = (f .: the carrier of H2);

      assume H1 is Subgroup of H2;

      then the carrier of H1 c= the carrier of H2 by GROUP_2:def 5;

      hence thesis by A1, GROUP_2: 57, RELAT_1: 123;

    end;

    theorem :: LATSUBGR:9

    for G1,G2 be Group holds for f be Homomorphism of G1, G2 holds for H1,H2 be Subgroup of G2 holds for H3,H4 be Subgroup of G1 st the carrier of H3 = (f " the carrier of H1) & the carrier of H4 = (f " the carrier of H2) holds H1 is Subgroup of H2 implies H3 is Subgroup of H4

    proof

      let G1,G2 be Group;

      let f be Homomorphism of G1, G2;

      let H1,H2 be Subgroup of G2;

      let H3,H4 be Subgroup of G1 such that

       A1: the carrier of H3 = (f " the carrier of H1) & the carrier of H4 = (f " the carrier of H2);

      assume H1 is Subgroup of H2;

      then the carrier of H1 c= the carrier of H2 by GROUP_2:def 5;

      hence thesis by A1, GROUP_2: 57, RELAT_1: 143;

    end;

    theorem :: LATSUBGR:10

    for G1,G2 be Group holds for f be Function of the carrier of G1, the carrier of G2 holds for A be Subset of G1 holds (f .: A) c= (f .: the carrier of ( gr A))

    proof

      let G1,G2 be Group;

      let f be Function of the carrier of G1, the carrier of G2;

      let A be Subset of G1;

      A c= the carrier of ( gr A) by GROUP_4:def 4;

      hence thesis by RELAT_1: 123;

    end;

    theorem :: LATSUBGR:11

    for G1,G2 be Group holds for H1,H2 be Subgroup of G1 holds for f be Function of the carrier of G1, the carrier of G2 holds for A be Subset of G1 st A = (the carrier of H1 \/ the carrier of H2) holds (f .: the carrier of (H1 "\/" H2)) = (f .: the carrier of ( gr A)) by Th4;

    theorem :: LATSUBGR:12

    

     Th12: for G be Group holds for A be Subset of G st A = {( 1_ G)} holds ( gr A) = ( (1). G)

    proof

      let G be Group;

      let A be Subset of G;

      assume A = {( 1_ G)};

      then A = the carrier of ( (1). G) by GROUP_2:def 7;

      hence thesis by Th3;

    end;

    definition

      let G be Group;

      :: LATSUBGR:def1

      func carr G -> Function of ( Subgroups G), ( bool the carrier of G) means

      : Def1: for H be strict Subgroup of G holds (it . H) = the carrier of H;

      existence

      proof

        defpred P[ object, object] means for h be strict Subgroup of G st h = $1 holds $2 = the carrier of h;

        

         A1: for e be object st e in ( Subgroups G) holds ex u be object st u in ( bool the carrier of G) & P[e, u]

        proof

          let e be object;

          assume e in ( Subgroups G);

          then

          reconsider E = e as strict Subgroup of G by GROUP_3:def 1;

          reconsider u = ( carr E) as Subset of G;

          take u;

          thus thesis by GROUP_2:def 9;

        end;

        consider f be Function of ( Subgroups G), ( bool the carrier of G) such that

         A2: for e be object st e in ( Subgroups G) holds P[e, (f . e)] from FUNCT_2:sch 1( A1);

        take f;

        let H be strict Subgroup of G;

        H in ( Subgroups G) by GROUP_3:def 1;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let F1,F2 be Function of ( Subgroups G), ( bool the carrier of G) such that

         A3: for H1 be strict Subgroup of G holds (F1 . H1) = the carrier of H1 and

         A4: for H2 be strict Subgroup of G holds (F2 . H2) = the carrier of H2;

        for h be object st h in ( Subgroups G) holds (F1 . h) = (F2 . h)

        proof

          let h be object;

          assume h in ( Subgroups G);

          then

          reconsider H = h as strict Subgroup of G by GROUP_3:def 1;

          

          thus (F1 . h) = the carrier of H by A3

          .= (F2 . h) by A4;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: LATSUBGR:13

    

     Th13: for G be Group holds for H be strict Subgroup of G holds for x be Element of G holds x in (( carr G) . H) iff x in H

    proof

      let G be Group;

      let H be strict Subgroup of G;

      let x be Element of G;

      thus x in (( carr G) . H) implies x in H

      proof

        assume x in (( carr G) . H);

        then x in the carrier of H by Def1;

        hence thesis by STRUCT_0:def 5;

      end;

      assume

       A1: x in H;

      (( carr G) . H) = the carrier of H by Def1;

      hence thesis by A1, STRUCT_0:def 5;

    end;

    theorem :: LATSUBGR:14

    for G be Group holds for H be strict Subgroup of G holds ( 1_ G) in (( carr G) . H)

    proof

      let G be Group;

      let H be strict Subgroup of G;

      (( carr G) . H) = the carrier of H & ( 1_ H) = ( 1_ G) by Def1, GROUP_2: 44;

      hence thesis;

    end;

    theorem :: LATSUBGR:15

    for G be Group holds for H be strict Subgroup of G holds (( carr G) . H) <> {} by Def1;

    theorem :: LATSUBGR:16

    for G be Group holds for H be strict Subgroup of G holds for g1,g2 be Element of G holds g1 in (( carr G) . H) & g2 in (( carr G) . H) implies (g1 * g2) in (( carr G) . H)

    proof

      let G be Group;

      let H be strict Subgroup of G;

      let g1,g2 be Element of G;

      assume g1 in (( carr G) . H) & g2 in (( carr G) . H);

      then g1 in H & g2 in H by Th13;

      then (g1 * g2) in H by GROUP_2: 50;

      hence thesis by Th13;

    end;

    theorem :: LATSUBGR:17

    for G be Group holds for H be strict Subgroup of G holds for g be Element of G holds g in (( carr G) . H) implies (g " ) in (( carr G) . H)

    proof

      let G be Group;

      let H be strict Subgroup of G;

      let g be Element of G;

      assume g in (( carr G) . H);

      then g in H by Th13;

      then (g " ) in H by GROUP_2: 51;

      hence thesis by Th13;

    end;

    theorem :: LATSUBGR:18

    

     Th18: for G be Group holds for H1,H2 be strict Subgroup of G holds the carrier of (H1 /\ H2) = ((( carr G) . H1) /\ (( carr G) . H2))

    proof

      let G be Group;

      let H1,H2 be strict Subgroup of G;

      (( carr G) . H1) = the carrier of H1 & (( carr G) . H2) = the carrier of H2 by Def1;

      hence thesis by Th1;

    end;

    theorem :: LATSUBGR:19

    for G be Group holds for H1,H2 be strict Subgroup of G holds (( carr G) . (H1 /\ H2)) = ((( carr G) . H1) /\ (( carr G) . H2))

    proof

      let G be Group;

      let H1,H2 be strict Subgroup of G;

      ((( carr G) . H1) /\ (( carr G) . H2)) = the carrier of (H1 /\ H2) by Th18;

      hence thesis by Def1;

    end;

    definition

      let G be Group;

      let F be non empty Subset of ( Subgroups G);

      :: LATSUBGR:def2

      func meet F -> strict Subgroup of G means

      : Def2: the carrier of it = ( meet (( carr G) .: F));

      existence

      proof

        reconsider CG = (( carr G) .: F) as Subset-Family of G;

        

         A1: (( carr G) .: F) <> {}

        proof

          consider x be Element of ( Subgroups G) such that

           A2: x in F by SUBSET_1: 4;

          (( carr G) . x) in (( carr G) .: F) by A2, FUNCT_2: 35;

          hence thesis;

        end;

        

         A3: for g be Element of G st g in ( meet CG) holds (g " ) in ( meet CG)

        proof

          let g be Element of G such that

           A4: g in ( meet CG);

          for X be set st X in (( carr G) .: F) holds (g " ) in X

          proof

            reconsider h = g as Element of G;

            let X be set;

            assume

             A5: X in (( carr G) .: F);

            then

             A6: g in X by A4, SETFAM_1:def 1;

            reconsider X as Subset of G by A5;

            consider X1 be Element of ( Subgroups G) such that X1 in F and

             A7: X = (( carr G) . X1) by A5, FUNCT_2: 65;

            reconsider X1 as strict Subgroup of G by GROUP_3:def 1;

            

             A8: X = the carrier of X1 by A7, Def1;

            then h in X1 by A6, STRUCT_0:def 5;

            then (h " ) in X1 by GROUP_2: 51;

            hence thesis by A8, STRUCT_0:def 5;

          end;

          hence thesis by A1, SETFAM_1:def 1;

        end;

        

         A9: for g1,g2 be Element of G st g1 in ( meet (( carr G) .: F)) & g2 in ( meet (( carr G) .: F)) holds (g1 * g2) in ( meet (( carr G) .: F))

        proof

          let g1,g2 be Element of G such that

           A10: g1 in ( meet (( carr G) .: F)) and

           A11: g2 in ( meet (( carr G) .: F));

          for X be set st X in (( carr G) .: F) holds (g1 * g2) in X

          proof

            reconsider h1 = g1, h2 = g2 as Element of G;

            let X be set;

            assume

             A12: X in (( carr G) .: F);

            then

             A13: g1 in X by A10, SETFAM_1:def 1;

            

             A14: g2 in X by A11, A12, SETFAM_1:def 1;

            reconsider X as Subset of G by A12;

            consider X1 be Element of ( Subgroups G) such that X1 in F and

             A15: X = (( carr G) . X1) by A12, FUNCT_2: 65;

            reconsider X1 as strict Subgroup of G by GROUP_3:def 1;

            

             A16: X = the carrier of X1 by A15, Def1;

            then

             A17: h2 in X1 by A14, STRUCT_0:def 5;

            h1 in X1 by A13, A16, STRUCT_0:def 5;

            then (h1 * h2) in X1 by A17, GROUP_2: 50;

            hence thesis by A16, STRUCT_0:def 5;

          end;

          hence thesis by A1, SETFAM_1:def 1;

        end;

        for X be set st X in (( carr G) .: F) holds ( 1_ G) in X

        proof

          let X be set;

          assume

           A18: X in (( carr G) .: F);

          then

          reconsider X as Subset of G;

          consider X1 be Element of ( Subgroups G) such that X1 in F and

           A19: X = (( carr G) . X1) by A18, FUNCT_2: 65;

          reconsider X1 as strict Subgroup of G by GROUP_3:def 1;

          

           A20: ( 1_ G) in X1 by GROUP_2: 46;

          X = the carrier of X1 by A19, Def1;

          hence thesis by A20, STRUCT_0:def 5;

        end;

        then ( meet (( carr G) .: F)) <> {} by A1, SETFAM_1:def 1;

        hence thesis by A9, A3, GROUP_2: 52;

      end;

      uniqueness by GROUP_2: 59;

    end

    theorem :: LATSUBGR:20

    for G be Group holds for F be non empty Subset of ( Subgroups G) holds ( (1). G) in F implies ( meet F) = ( (1). G)

    proof

      let G be Group;

      let F be non empty Subset of ( Subgroups G);

      assume

       A1: ( (1). G) in F;

      reconsider 1G = ( (1). G) as Element of ( Subgroups G) by GROUP_3:def 1;

      (( carr G) . 1G) = the carrier of ( (1). G) by Def1;

      then the carrier of ( (1). G) in (( carr G) .: F) by A1, FUNCT_2: 35;

      then {( 1_ G)} in (( carr G) .: F) by GROUP_2:def 7;

      then ( meet (( carr G) .: F)) c= {( 1_ G)} by SETFAM_1: 3;

      then

       A2: the carrier of ( meet F) c= {( 1_ G)} by Def2;

      ( (1). G) is Subgroup of ( meet F) by GROUP_2: 65;

      then the carrier of ( (1). G) c= the carrier of ( meet F) by GROUP_2:def 5;

      then {( 1_ G)} c= the carrier of ( meet F) by GROUP_2:def 7;

      then the carrier of ( meet F) = {( 1_ G)} by A2;

      hence thesis by GROUP_2:def 7;

    end;

    theorem :: LATSUBGR:21

    for G be Group holds for h be Element of ( Subgroups G) holds for F be non empty Subset of ( Subgroups G) st F = {h} holds ( meet F) = h

    proof

      let G be Group;

      let h be Element of ( Subgroups G);

      let F be non empty Subset of ( Subgroups G) such that

       A1: F = {h};

      reconsider H = h as strict Subgroup of G by GROUP_3:def 1;

      h in ( Subgroups G);

      then h in ( dom ( carr G)) by FUNCT_2:def 1;

      then ( meet ( Im (( carr G),h))) = ( meet {(( carr G) . h)}) by FUNCT_1: 59;

      then

       A2: ( meet ( Im (( carr G),h))) = (( carr G) . h) by SETFAM_1: 10;

      the carrier of ( meet F) = ( meet (( carr G) .: F)) by Def2;

      then the carrier of ( meet F) = the carrier of H by A1, A2, Def1;

      hence thesis by GROUP_2: 59;

    end;

    theorem :: LATSUBGR:22

    

     Th22: for G be Group holds for H1,H2 be Subgroup of G holds for h1,h2 be Element of ( lattice G) st h1 = H1 & h2 = H2 holds (h1 "\/" h2) = (H1 "\/" H2)

    proof

      let G be Group;

      let H1,H2 be Subgroup of G;

      let h1,h2 be Element of ( lattice G);

      

       A1: (h1 "\/" h2) = (( SubJoin G) . (h1,h2)) by LATTICES:def 1;

      assume

       A2: h1 = H1 & h2 = H2;

      then H1 is strict & H2 is strict by GROUP_3:def 1;

      hence thesis by A2, A1, GROUP_4:def 10;

    end;

    theorem :: LATSUBGR:23

    

     Th23: for G be Group holds for H1,H2 be Subgroup of G holds for h1,h2 be Element of ( lattice G) st h1 = H1 & h2 = H2 holds (h1 "/\" h2) = (H1 /\ H2)

    proof

      let G be Group;

      let H1,H2 be Subgroup of G;

      let h1,h2 be Element of ( lattice G);

      

       A1: (h1 "/\" h2) = (( SubMeet G) . (h1,h2)) by LATTICES:def 2;

      assume

       A2: h1 = H1 & h2 = H2;

      then H1 is strict & H2 is strict by GROUP_3:def 1;

      hence thesis by A2, A1, GROUP_4:def 11;

    end;

    theorem :: LATSUBGR:24

    for G be Group holds for p be Element of ( lattice G) holds for H be Subgroup of G st p = H holds H is strict Subgroup of G by GROUP_3:def 1;

    theorem :: LATSUBGR:25

    

     Th25: for G be Group holds for H1,H2 be Subgroup of G holds for p,q be Element of ( lattice G) st p = H1 & q = H2 holds p [= q iff the carrier of H1 c= the carrier of H2

    proof

      let G be Group;

      let H1,H2 be Subgroup of G;

      let p,q be Element of ( lattice G) such that

       A1: p = H1 and

       A2: q = H2;

      

       A3: H1 is strict Subgroup of G by A1, GROUP_3:def 1;

      

       A4: H2 is strict Subgroup of G by A2, GROUP_3:def 1;

      thus p [= q implies the carrier of H1 c= the carrier of H2

      proof

        assume p [= q;

        then

         A5: (p "/\" q) = p by LATTICES: 4;

        (p "/\" q) = (the L_meet of ( lattice G) . (p,q)) by LATTICES:def 2

        .= (H1 /\ H2) by A1, A2, A3, A4, GROUP_4:def 11;

        then (the carrier of H1 /\ the carrier of H2) = the carrier of H1 by A1, A5, Th1;

        hence thesis by XBOOLE_1: 17;

      end;

      thus the carrier of H1 c= the carrier of H2 implies p [= q

      proof

        assume the carrier of H1 c= the carrier of H2;

        then H1 is Subgroup of H2 by GROUP_2: 57;

        then

         A6: (H1 /\ H2) = H1 by A3, GROUP_2: 89;

        (H1 /\ H2) = (the L_meet of ( lattice G) . (p,q)) by A1, A2, A3, A4, GROUP_4:def 11

        .= (p "/\" q) by LATTICES:def 2;

        hence thesis by A1, A6, LATTICES: 4;

      end;

    end;

    theorem :: LATSUBGR:26

    for G be Group holds for H1,H2 be Subgroup of G holds for p,q be Element of ( lattice G) st p = H1 & q = H2 holds p [= q iff H1 is Subgroup of H2

    proof

      let G be Group;

      let H1,H2 be Subgroup of G;

      let p,q be Element of ( lattice G);

      assume that

       A1: p = H1 and

       A2: q = H2;

      thus p [= q implies H1 is Subgroup of H2

      proof

        assume p [= q;

        then the carrier of H1 c= the carrier of H2 by A1, A2, Th25;

        hence thesis by GROUP_2: 57;

      end;

      

       A3: H1 is strict Subgroup of G by A1, GROUP_3:def 1;

      

       A4: H2 is strict Subgroup of G by A2, GROUP_3:def 1;

      thus H1 is Subgroup of H2 implies p [= q

      proof

        assume H1 is Subgroup of H2;

        then

         A5: (H1 /\ H2) = H1 by A3, GROUP_2: 89;

        (H1 /\ H2) = (the L_meet of ( lattice G) . (p,q)) by A1, A2, A3, A4, GROUP_4:def 11

        .= (p "/\" q) by LATTICES:def 2;

        hence thesis by A1, A5, LATTICES: 4;

      end;

    end;

    theorem :: LATSUBGR:27

    for G be Group holds ( lattice G) is complete

    proof

      let G be Group;

      let Y be Subset of ( lattice G);

      per cases ;

        suppose

         A1: Y = {} ;

        take ( Top ( lattice G));

        thus ( Top ( lattice G)) is_less_than Y by A1;

        let b be Element of ( lattice G);

        assume b is_less_than Y;

        thus thesis by LATTICES: 19;

      end;

        suppose Y <> {} ;

        then

        reconsider X = Y as non empty Subset of ( Subgroups G);

        reconsider p = ( meet X) as Element of ( lattice G) by GROUP_3:def 1;

        take p;

        set x = the Element of X;

        thus p is_less_than Y

        proof

          let q be Element of ( lattice G);

          reconsider H = q as strict Subgroup of G by GROUP_3:def 1;

          reconsider h = q as Element of ( Subgroups G);

          assume

           A2: q in Y;

          (( carr G) . h) = the carrier of H by Def1;

          then ( meet (( carr G) .: X)) c= the carrier of H by A2, FUNCT_2: 35, SETFAM_1: 3;

          then the carrier of ( meet X) c= the carrier of H by Def2;

          hence thesis by Th25;

        end;

        let r be Element of ( lattice G);

        reconsider H = r as Subgroup of G by GROUP_3:def 1;

        assume

         A3: r is_less_than Y;

        

         A4: for Z1 be set st Z1 in (( carr G) .: X) holds the carrier of H c= Z1

        proof

          let Z1 be set;

          assume

           A5: Z1 in (( carr G) .: X);

          then

          reconsider Z2 = Z1 as Subset of G;

          consider z1 be Element of ( Subgroups G) such that

           A6: z1 in X & Z2 = (( carr G) . z1) by A5, FUNCT_2: 65;

          reconsider z1 as Element of ( lattice G);

          reconsider z3 = z1 as strict Subgroup of G by GROUP_3:def 1;

          Z1 = the carrier of z3 & r [= z1 by A3, A6, Def1;

          hence thesis by Th25;

        end;

        (( carr G) . x) in (( carr G) .: X) by FUNCT_2: 35;

        then the carrier of H c= ( meet (( carr G) .: X)) by A4, SETFAM_1: 5;

        then the carrier of H c= the carrier of ( meet X) by Def2;

        hence thesis by Th25;

      end;

    end;

    definition

      let G1,G2 be Group;

      let f be Function of the carrier of G1, the carrier of G2;

      :: LATSUBGR:def3

      func FuncLatt f -> Function of the carrier of ( lattice G1), the carrier of ( lattice G2) means

      : Def3: for H be strict Subgroup of G1, A be Subset of G2 st A = (f .: the carrier of H) holds (it . H) = ( gr A);

      existence

      proof

        defpred P[ object, object] means for H be strict Subgroup of G1 st H = $1 holds for A be Subset of G2 st A = (f .: the carrier of H) holds $2 = ( gr (f .: the carrier of H));

        

         A1: for e be object st e in the carrier of ( lattice G1) holds ex u be object st u in the carrier of ( lattice G2) & P[e, u]

        proof

          let e be object;

          assume e in the carrier of ( lattice G1);

          then

          reconsider E = e as strict Subgroup of G1 by GROUP_3:def 1;

          reconsider u = ( gr (f .: the carrier of E)) as strict Subgroup of G2;

          reconsider u as Element of ( lattice G2) by GROUP_3:def 1;

          take u;

          thus thesis;

        end;

        consider f1 be Function of the carrier of ( lattice G1), the carrier of ( lattice G2) such that

         A2: for e be object st e in the carrier of ( lattice G1) holds P[e, (f1 . e)] from FUNCT_2:sch 1( A1);

        take f1;

        let H be strict Subgroup of G1;

        let A be Subset of G2;

        

         A3: H in the carrier of ( lattice G1) by GROUP_3:def 1;

        assume A = (f .: the carrier of H);

        hence thesis by A2, A3;

      end;

      uniqueness

      proof

        let f1,f2 be Function of the carrier of ( lattice G1), the carrier of ( lattice G2) such that

         A4: for H be strict Subgroup of G1, A be Subset of G2 st A = (f .: the carrier of H) holds (f1 . H) = ( gr A) and

         A5: for H be strict Subgroup of G1, A be Subset of G2 st A = (f .: the carrier of H) holds (f2 . H) = ( gr A);

        for h be object st h in the carrier of ( lattice G1) holds (f1 . h) = (f2 . h)

        proof

          let h be object;

          assume h in the carrier of ( lattice G1);

          then

          reconsider H = h as strict Subgroup of G1 by GROUP_3:def 1;

          

          thus (f1 . h) = ( gr (f .: the carrier of H)) by A4

          .= (f2 . h) by A5;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: LATSUBGR:28

    for G be Group holds ( FuncLatt ( id the carrier of G)) = ( id the carrier of ( lattice G))

    proof

      let G be Group;

      set f = ( id the carrier of G);

      

       A1: for x be object st x in the carrier of ( lattice G) holds (( FuncLatt f) . x) = x

      proof

        let x be object;

        assume x in the carrier of ( lattice G);

        then

        reconsider x as strict Subgroup of G by GROUP_3:def 1;

        

         A2: the carrier of x c= (f .: the carrier of x)

        proof

          let z be object;

          assume

           A3: z in the carrier of x;

          the carrier of x c= the carrier of G by GROUP_2:def 5;

          then

          reconsider z as Element of G by A3;

          (f . z) = z;

          hence thesis by A3, FUNCT_2: 35;

        end;

        

         A4: (f .: the carrier of x) c= the carrier of x

        proof

          let z be object;

          assume

           A5: z in (f .: the carrier of x);

          then

          reconsider z as Element of G;

          ex Z be Element of G st Z in the carrier of x & z = (f . Z) by A5, FUNCT_2: 65;

          hence thesis;

        end;

        then

        reconsider X = the carrier of x as Subset of G by A2, XBOOLE_0:def 10;

        (f .: the carrier of x) = the carrier of x by A4, A2;

        then (( FuncLatt f) . x) = ( gr X) by Def3;

        hence thesis by Th3;

      end;

      ( dom ( FuncLatt f)) = the carrier of ( lattice G) by FUNCT_2:def 1;

      hence thesis by A1, FUNCT_1: 17;

    end;

    theorem :: LATSUBGR:29

    for G1,G2 be Group holds for f be Homomorphism of G1, G2 st f is one-to-one holds ( FuncLatt f) is one-to-one

    proof

      let G1,G2 be Group;

      let f be Homomorphism of G1, G2 such that

       A1: f is one-to-one;

      for x1,x2 be object st x1 in ( dom ( FuncLatt f)) & x2 in ( dom ( FuncLatt f)) & (( FuncLatt f) . x1) = (( FuncLatt f) . x2) holds x1 = x2

      proof

        reconsider y = (f . ( 1_ G1)) as Element of G2;

        let x1,x2 be object;

        assume that

         A2: x1 in ( dom ( FuncLatt f)) & x2 in ( dom ( FuncLatt f)) and

         A3: (( FuncLatt f) . x1) = (( FuncLatt f) . x2);

        reconsider x1, x2 as strict Subgroup of G1 by A2, GROUP_3:def 1;

        reconsider A1 = (f .: the carrier of x1), A2 = (f .: the carrier of x2) as Subset of G2;

        

         A4: for g be Element of G2 st g in (f .: the carrier of x1) holds (g " ) in (f .: the carrier of x1)

        proof

          let g be Element of G2;

          assume g in (f .: the carrier of x1);

          then

          consider x be Element of G1 such that

           A5: x in the carrier of x1 and

           A6: g = (f . x) by FUNCT_2: 65;

          x in x1 by A5, STRUCT_0:def 5;

          then (x " ) in x1 by GROUP_2: 51;

          then

           A7: (x " ) in the carrier of x1 by STRUCT_0:def 5;

          (f . (x " )) = ((f . x) " ) by GROUP_6: 32;

          hence thesis by A6, A7, FUNCT_2: 35;

        end;

        

         A8: for g1,g2 be Element of G2 st g1 in (f .: the carrier of x1) & g2 in (f .: the carrier of x1) holds (g1 * g2) in (f .: the carrier of x1)

        proof

          let g1,g2 be Element of G2;

          assume that

           A9: g1 in (f .: the carrier of x1) and

           A10: g2 in (f .: the carrier of x1);

          consider x be Element of G1 such that

           A11: x in the carrier of x1 and

           A12: g1 = (f . x) by A9, FUNCT_2: 65;

          consider y be Element of G1 such that

           A13: y in the carrier of x1 and

           A14: g2 = (f . y) by A10, FUNCT_2: 65;

          

           A15: y in x1 by A13, STRUCT_0:def 5;

          x in x1 by A11, STRUCT_0:def 5;

          then (x * y) in x1 by A15, GROUP_2: 50;

          then

           A16: (x * y) in the carrier of x1 by STRUCT_0:def 5;

          (f . (x * y)) = ((f . x) * (f . y)) by GROUP_6:def 6;

          hence thesis by A12, A14, A16, FUNCT_2: 35;

        end;

        

         A17: for g be Element of G2 st g in (f .: the carrier of x2) holds (g " ) in (f .: the carrier of x2)

        proof

          let g be Element of G2;

          assume g in (f .: the carrier of x2);

          then

          consider x be Element of G1 such that

           A18: x in the carrier of x2 and

           A19: g = (f . x) by FUNCT_2: 65;

          x in x2 by A18, STRUCT_0:def 5;

          then (x " ) in x2 by GROUP_2: 51;

          then

           A20: (x " ) in the carrier of x2 by STRUCT_0:def 5;

          (f . (x " )) = ((f . x) " ) by GROUP_6: 32;

          hence thesis by A19, A20, FUNCT_2: 35;

        end;

        

         A21: ( dom f) = the carrier of G1 by FUNCT_2:def 1;

        

         A22: for g1,g2 be Element of G2 st g1 in (f .: the carrier of x2) & g2 in (f .: the carrier of x2) holds (g1 * g2) in (f .: the carrier of x2)

        proof

          let g1,g2 be Element of G2;

          assume that

           A23: g1 in (f .: the carrier of x2) and

           A24: g2 in (f .: the carrier of x2);

          consider x be Element of G1 such that

           A25: x in the carrier of x2 and

           A26: g1 = (f . x) by A23, FUNCT_2: 65;

          consider y be Element of G1 such that

           A27: y in the carrier of x2 and

           A28: g2 = (f . y) by A24, FUNCT_2: 65;

          

           A29: y in x2 by A27, STRUCT_0:def 5;

          x in x2 by A25, STRUCT_0:def 5;

          then (x * y) in x2 by A29, GROUP_2: 50;

          then

           A30: (x * y) in the carrier of x2 by STRUCT_0:def 5;

          (f . (x * y)) = ((f . x) * (f . y)) by GROUP_6:def 6;

          hence thesis by A26, A28, A30, FUNCT_2: 35;

        end;

        ( 1_ G1) in x2 by GROUP_2: 46;

        then

         A31: ( 1_ G1) in the carrier of x2 by STRUCT_0:def 5;

        

         A32: (( FuncLatt f) . x1) = ( gr A1) & (( FuncLatt f) . x2) = ( gr A2) by Def3;

        ex y be Element of G2 st y = (f . ( 1_ G1));

        then (f .: the carrier of x2) <> {} by A21, A31, FUNCT_1:def 6;

        then

        consider B2 be strict Subgroup of G2 such that

         A33: the carrier of B2 = (f .: the carrier of x2) by A17, A22, GROUP_2: 52;

        ( 1_ G1) in x1 by GROUP_2: 46;

        then ( 1_ G1) in the carrier of x1 by STRUCT_0:def 5;

        then y in (f .: the carrier of x1) by A21, FUNCT_1:def 6;

        then

         A34: ex B1 be strict Subgroup of G2 st the carrier of B1 = (f .: the carrier of x1) by A4, A8, GROUP_2: 52;

        ( gr (f .: the carrier of x2)) = B2 by A33, Th3;

        then

         A35: (f .: the carrier of x1) = (f .: the carrier of x2) by A3, A32, A34, A33, Th3;

        the carrier of x2 c= ( dom f) by A21, GROUP_2:def 5;

        then

         A36: the carrier of x2 c= the carrier of x1 by A1, A35, FUNCT_1: 87;

        the carrier of x1 c= ( dom f) by A21, GROUP_2:def 5;

        then the carrier of x1 c= the carrier of x2 by A1, A35, FUNCT_1: 87;

        then the carrier of x1 = the carrier of x2 by A36;

        hence thesis by GROUP_2: 59;

      end;

      hence thesis by FUNCT_1:def 4;

    end;

    theorem :: LATSUBGR:30

    for G1,G2 be Group holds for f be Homomorphism of G1, G2 holds (( FuncLatt f) . ( (1). G1)) = ( (1). G2)

    proof

      let G1,G2 be Group;

      let f be Homomorphism of G1, G2;

      consider A be Subset of G2 such that

       A1: A = (f .: the carrier of ( (1). G1));

      

       A2: A = (f .: {( 1_ G1)}) by A1, GROUP_2:def 7;

      

       A3: ( 1_ G1) in {( 1_ G1)} & ( 1_ G2) = (f . ( 1_ G1)) by GROUP_6: 31, TARSKI:def 1;

      for x be object holds x in A iff x = ( 1_ G2)

      proof

        let x be object;

        thus x in A implies x = ( 1_ G2)

        proof

          assume

           A4: x in A;

          then

          reconsider x as Element of G2;

          consider y be Element of G1 such that

           A5: y in {( 1_ G1)} and

           A6: x = (f . y) by A2, A4, FUNCT_2: 65;

          y = ( 1_ G1) by A5, TARSKI:def 1;

          hence thesis by A6, GROUP_6: 31;

        end;

        thus thesis by A2, A3, FUNCT_2: 35;

      end;

      then A = {( 1_ G2)} by TARSKI:def 1;

      then ( gr A) = ( (1). G2) by Th12;

      hence thesis by A1, Def3;

    end;

    theorem :: LATSUBGR:31

    

     Th31: for G1,G2 be Group holds for f be Homomorphism of G1, G2 st f is one-to-one holds ( FuncLatt f) is Semilattice-Homomorphism of ( lattice G1), ( lattice G2)

    proof

      let G1,G2 be Group;

      let f be Homomorphism of G1, G2 such that

       A1: f is one-to-one;

      for a,b be Element of ( lattice G1) holds (( FuncLatt f) . (a "/\" b)) = ((( FuncLatt f) . a) "/\" (( FuncLatt f) . b))

      proof

        let a,b be Element of ( lattice G1);

        consider A1 be strict Subgroup of G1 such that

         A2: A1 = a by Th2;

        consider B1 be strict Subgroup of G1 such that

         A3: B1 = b by Th2;

        thus thesis

        proof

          

           A4: for g1,g2 be Element of G2 st g1 in (f .: the carrier of B1) & g2 in (f .: the carrier of B1) holds (g1 * g2) in (f .: the carrier of B1)

          proof

            let g1,g2 be Element of G2;

            assume that

             A5: g1 in (f .: the carrier of B1) and

             A6: g2 in (f .: the carrier of B1);

            consider x be Element of G1 such that

             A7: x in the carrier of B1 and

             A8: g1 = (f . x) by A5, FUNCT_2: 65;

            consider y be Element of G1 such that

             A9: y in the carrier of B1 and

             A10: g2 = (f . y) by A6, FUNCT_2: 65;

            

             A11: y in B1 by A9, STRUCT_0:def 5;

            x in B1 by A7, STRUCT_0:def 5;

            then (x * y) in B1 by A11, GROUP_2: 50;

            then

             A12: (x * y) in the carrier of B1 by STRUCT_0:def 5;

            (f . (x * y)) = ((f . x) * (f . y)) by GROUP_6:def 6;

            hence thesis by A8, A10, A12, FUNCT_2: 35;

          end;

          

           A13: for g be Element of G2 st g in (f .: the carrier of B1) holds (g " ) in (f .: the carrier of B1)

          proof

            let g be Element of G2;

            assume g in (f .: the carrier of B1);

            then

            consider x be Element of G1 such that

             A14: x in the carrier of B1 and

             A15: g = (f . x) by FUNCT_2: 65;

            x in B1 by A14, STRUCT_0:def 5;

            then (x " ) in B1 by GROUP_2: 51;

            then

             A16: (x " ) in the carrier of B1 by STRUCT_0:def 5;

            (f . (x " )) = ((f . x) " ) by GROUP_6: 32;

            hence thesis by A15, A16, FUNCT_2: 35;

          end;

          

           A17: for g be Element of G2 st g in (f .: the carrier of A1) holds (g " ) in (f .: the carrier of A1)

          proof

            let g be Element of G2;

            assume g in (f .: the carrier of A1);

            then

            consider x be Element of G1 such that

             A18: x in the carrier of A1 and

             A19: g = (f . x) by FUNCT_2: 65;

            x in A1 by A18, STRUCT_0:def 5;

            then (x " ) in A1 by GROUP_2: 51;

            then

             A20: (x " ) in the carrier of A1 by STRUCT_0:def 5;

            (f . (x " )) = ((f . x) " ) by GROUP_6: 32;

            hence thesis by A19, A20, FUNCT_2: 35;

          end;

          ( 1_ G1) in A1 by GROUP_2: 46;

          then

           A21: ( 1_ G1) in the carrier of A1 by STRUCT_0:def 5;

          

           A22: (( FuncLatt f) . (A1 /\ B1)) = ( gr (f .: the carrier of (A1 /\ B1))) by Def3;

          consider C1 be strict Subgroup of G1 such that

           A23: C1 = (A1 /\ B1);

          

           A24: for g1,g2 be Element of G2 st g1 in (f .: the carrier of A1) & g2 in (f .: the carrier of A1) holds (g1 * g2) in (f .: the carrier of A1)

          proof

            let g1,g2 be Element of G2;

            assume that

             A25: g1 in (f .: the carrier of A1) and

             A26: g2 in (f .: the carrier of A1);

            consider x be Element of G1 such that

             A27: x in the carrier of A1 and

             A28: g1 = (f . x) by A25, FUNCT_2: 65;

            consider y be Element of G1 such that

             A29: y in the carrier of A1 and

             A30: g2 = (f . y) by A26, FUNCT_2: 65;

            

             A31: y in A1 by A29, STRUCT_0:def 5;

            x in A1 by A27, STRUCT_0:def 5;

            then (x * y) in A1 by A31, GROUP_2: 50;

            then

             A32: (x * y) in the carrier of A1 by STRUCT_0:def 5;

            (f . (x * y)) = ((f . x) * (f . y)) by GROUP_6:def 6;

            hence thesis by A28, A30, A32, FUNCT_2: 35;

          end;

          ( 1_ G1) in B1 by GROUP_2: 46;

          then

           A33: ( 1_ G1) in the carrier of B1 by STRUCT_0:def 5;

          

           A34: (( FuncLatt f) . a) = ( gr (f .: the carrier of A1)) & (( FuncLatt f) . b) = ( gr (f .: the carrier of B1)) by A2, A3, Def3;

          

           A35: ( dom f) = the carrier of G1 by FUNCT_2:def 1;

          

           A36: for g1,g2 be Element of G2 st g1 in (f .: the carrier of C1) & g2 in (f .: the carrier of C1) holds (g1 * g2) in (f .: the carrier of C1)

          proof

            let g1,g2 be Element of G2;

            assume that

             A37: g1 in (f .: the carrier of C1) and

             A38: g2 in (f .: the carrier of C1);

            consider x be Element of G1 such that

             A39: x in the carrier of C1 and

             A40: g1 = (f . x) by A37, FUNCT_2: 65;

            consider y be Element of G1 such that

             A41: y in the carrier of C1 and

             A42: g2 = (f . y) by A38, FUNCT_2: 65;

            

             A43: y in C1 by A41, STRUCT_0:def 5;

            x in C1 by A39, STRUCT_0:def 5;

            then (x * y) in C1 by A43, GROUP_2: 50;

            then

             A44: (x * y) in the carrier of C1 by STRUCT_0:def 5;

            (f . (x * y)) = ((f . x) * (f . y)) by GROUP_6:def 6;

            hence thesis by A40, A42, A44, FUNCT_2: 35;

          end;

          

           A45: for g be Element of G2 st g in (f .: the carrier of C1) holds (g " ) in (f .: the carrier of C1)

          proof

            let g be Element of G2;

            assume g in (f .: the carrier of C1);

            then

            consider x be Element of G1 such that

             A46: x in the carrier of C1 and

             A47: g = (f . x) by FUNCT_2: 65;

            x in C1 by A46, STRUCT_0:def 5;

            then (x " ) in C1 by GROUP_2: 51;

            then

             A48: (x " ) in the carrier of C1 by STRUCT_0:def 5;

            (f . (x " )) = ((f . x) " ) by GROUP_6: 32;

            hence thesis by A47, A48, FUNCT_2: 35;

          end;

          ( 1_ G1) in C1 by GROUP_2: 46;

          then

           A49: ( 1_ G1) in the carrier of C1 by STRUCT_0:def 5;

          ex y2 be Element of G2 st y2 = (f . ( 1_ G1));

          then (f .: the carrier of C1) <> {} by A35, A49, FUNCT_1:def 6;

          then

          consider C3 be strict Subgroup of G2 such that

           A50: the carrier of C3 = (f .: the carrier of C1) by A45, A36, GROUP_2: 52;

          ex y1 be Element of G2 st y1 = (f . ( 1_ G1));

          then (f .: the carrier of B1) <> {} by A35, A33, FUNCT_1:def 6;

          then

          consider B3 be strict Subgroup of G2 such that

           A51: the carrier of B3 = (f .: the carrier of B1) by A13, A4, GROUP_2: 52;

          ex y be Element of G2 st y = (f . ( 1_ G1));

          then (f .: the carrier of A1) <> {} by A35, A21, FUNCT_1:def 6;

          then

          consider A3 be strict Subgroup of G2 such that

           A52: the carrier of A3 = (f .: the carrier of A1) by A17, A24, GROUP_2: 52;

          

           A53: the carrier of C3 c= the carrier of (A3 /\ B3)

          proof

            

             A54: (f .: the carrier of (A1 /\ B1)) c= (f .: the carrier of B1)

            proof

              let x be object;

              assume

               A55: x in (f .: the carrier of (A1 /\ B1));

              then

              reconsider x as Element of G2;

              consider y be Element of G1 such that

               A56: y in the carrier of (A1 /\ B1) and

               A57: x = (f . y) by A55, FUNCT_2: 65;

              y in (the carrier of A1 /\ the carrier of B1) by A56, Th1;

              then y in the carrier of B1 by XBOOLE_0:def 4;

              hence thesis by A57, FUNCT_2: 35;

            end;

            

             A58: (f .: the carrier of (A1 /\ B1)) c= (f .: the carrier of A1)

            proof

              let x be object;

              assume

               A59: x in (f .: the carrier of (A1 /\ B1));

              then

              reconsider x as Element of G2;

              consider y be Element of G1 such that

               A60: y in the carrier of (A1 /\ B1) and

               A61: x = (f . y) by A59, FUNCT_2: 65;

              y in (the carrier of A1 /\ the carrier of B1) by A60, Th1;

              then y in the carrier of A1 by XBOOLE_0:def 4;

              hence thesis by A61, FUNCT_2: 35;

            end;

            let x be object;

            assume

             A62: x in the carrier of C3;

            the carrier of C3 c= the carrier of G2 by GROUP_2:def 5;

            then

            reconsider x as Element of G2 by A62;

            consider y be Element of G1 such that

             A63: y in the carrier of (A1 /\ B1) and

             A64: x = (f . y) by A23, A50, A62, FUNCT_2: 65;

            (f . y) in (f .: the carrier of (A1 /\ B1)) by A63, FUNCT_2: 35;

            then (f . y) in (the carrier of A3 /\ the carrier of B3) by A52, A51, A58, A54, XBOOLE_0:def 4;

            hence thesis by A64, Th1;

          end;

          

           A65: ( gr (f .: the carrier of B1)) = B3 by A51, Th3;

          the carrier of (A3 /\ B3) c= the carrier of C3

          proof

            let x be object;

            assume x in the carrier of (A3 /\ B3);

            then x in (the carrier of A3 /\ the carrier of B3) by Th1;

            then x in (f .: (the carrier of A1 /\ the carrier of B1)) by A1, A52, A51, FUNCT_1: 62;

            hence thesis by A23, A50, Th1;

          end;

          then the carrier of (A3 /\ B3) = the carrier of C3 by A53;

          

          then ( gr (f .: the carrier of (A1 /\ B1))) = (A3 /\ B3) by A23, A50, Th3

          .= (( gr (f .: the carrier of A1)) /\ ( gr (f .: the carrier of B1))) by A52, A65, Th3

          .= ((( FuncLatt f) . a) "/\" (( FuncLatt f) . b)) by A34, Th23;

          hence thesis by A2, A3, A22, Th23;

        end;

      end;

      hence thesis by LATTICE4:def 2;

    end;

    theorem :: LATSUBGR:32

    

     Th32: for G1,G2 be Group holds for f be Homomorphism of G1, G2 holds ( FuncLatt f) is sup-Semilattice-Homomorphism of ( lattice G1), ( lattice G2)

    proof

      let G1,G2 be Group;

      let f be Homomorphism of G1, G2;

      for a,b be Element of ( lattice G1) holds (( FuncLatt f) . (a "\/" b)) = ((( FuncLatt f) . a) "\/" (( FuncLatt f) . b))

      proof

        let a,b be Element of ( lattice G1);

        consider A1 be strict Subgroup of G1 such that

         A1: A1 = a by Th2;

        consider B1 be strict Subgroup of G1 such that

         A2: B1 = b by Th2;

        thus thesis

        proof

          

           A3: for g be Element of G2 st g in (f .: the carrier of B1) holds (g " ) in (f .: the carrier of B1)

          proof

            let g be Element of G2;

            assume g in (f .: the carrier of B1);

            then

            consider x be Element of G1 such that

             A4: x in the carrier of B1 and

             A5: g = (f . x) by FUNCT_2: 65;

            x in B1 by A4, STRUCT_0:def 5;

            then (x " ) in B1 by GROUP_2: 51;

            then

             A6: (x " ) in the carrier of B1 by STRUCT_0:def 5;

            (f . (x " )) = ((f . x) " ) by GROUP_6: 32;

            hence thesis by A5, A6, FUNCT_2: 35;

          end;

          ( 1_ G1) in A1 by GROUP_2: 46;

          then

           A7: ( 1_ G1) in the carrier of A1 by STRUCT_0:def 5;

          

           A8: ex y be Element of G2 st y = (f . ( 1_ G1));

          the carrier of A1 c= the carrier of G1 & the carrier of B1 c= the carrier of G1 by GROUP_2:def 5;

          then

          reconsider A = (the carrier of A1 \/ the carrier of B1) as Subset of G1 by XBOOLE_1: 8;

          

           A9: for g be Element of G2 st g in (f .: the carrier of A1) holds (g " ) in (f .: the carrier of A1)

          proof

            let g be Element of G2;

            assume g in (f .: the carrier of A1);

            then

            consider x be Element of G1 such that

             A10: x in the carrier of A1 and

             A11: g = (f . x) by FUNCT_2: 65;

            x in A1 by A10, STRUCT_0:def 5;

            then (x " ) in A1 by GROUP_2: 51;

            then

             A12: (x " ) in the carrier of A1 by STRUCT_0:def 5;

            (f . (x " )) = ((f . x) " ) by GROUP_6: 32;

            hence thesis by A11, A12, FUNCT_2: 35;

          end;

          reconsider B = ((f .: the carrier of A1) \/ (f .: the carrier of B1)) as Subset of G2;

          

           A13: ( dom f) = the carrier of G1 by FUNCT_2:def 1;

          

           A14: for g1,g2 be Element of G2 st g1 in (f .: the carrier of B1) & g2 in (f .: the carrier of B1) holds (g1 * g2) in (f .: the carrier of B1)

          proof

            let g1,g2 be Element of G2;

            assume that

             A15: g1 in (f .: the carrier of B1) and

             A16: g2 in (f .: the carrier of B1);

            consider x be Element of G1 such that

             A17: x in the carrier of B1 and

             A18: g1 = (f . x) by A15, FUNCT_2: 65;

            consider y be Element of G1 such that

             A19: y in the carrier of B1 and

             A20: g2 = (f . y) by A16, FUNCT_2: 65;

            

             A21: y in B1 by A19, STRUCT_0:def 5;

            x in B1 by A17, STRUCT_0:def 5;

            then (x * y) in B1 by A21, GROUP_2: 50;

            then

             A22: (x * y) in the carrier of B1 by STRUCT_0:def 5;

            (f . (x * y)) = ((f . x) * (f . y)) by GROUP_6:def 6;

            hence thesis by A18, A20, A22, FUNCT_2: 35;

          end;

          ( 1_ G1) in B1 by GROUP_2: 46;

          then

           A23: ( 1_ G1) in the carrier of B1 by STRUCT_0:def 5;

          

           A24: (( FuncLatt f) . (A1 "\/" B1)) = ( gr (f .: the carrier of (A1 "\/" B1))) by Def3;

          ex y1 be Element of G2 st y1 = (f . ( 1_ G1));

          then (f .: the carrier of B1) <> {} by A13, A23, FUNCT_1:def 6;

          then

          consider B3 be strict Subgroup of G2 such that

           A25: the carrier of B3 = (f .: the carrier of B1) by A3, A14, GROUP_2: 52;

          

           A26: for g1,g2 be Element of G2 st g1 in (f .: the carrier of A1) & g2 in (f .: the carrier of A1) holds (g1 * g2) in (f .: the carrier of A1)

          proof

            let g1,g2 be Element of G2;

            assume that

             A27: g1 in (f .: the carrier of A1) and

             A28: g2 in (f .: the carrier of A1);

            consider x be Element of G1 such that

             A29: x in the carrier of A1 and

             A30: g1 = (f . x) by A27, FUNCT_2: 65;

            consider y be Element of G1 such that

             A31: y in the carrier of A1 and

             A32: g2 = (f . y) by A28, FUNCT_2: 65;

            

             A33: y in A1 by A31, STRUCT_0:def 5;

            x in A1 by A29, STRUCT_0:def 5;

            then (x * y) in A1 by A33, GROUP_2: 50;

            then

             A34: (x * y) in the carrier of A1 by STRUCT_0:def 5;

            (f . (x * y)) = ((f . x) * (f . y)) by GROUP_6:def 6;

            hence thesis by A30, A32, A34, FUNCT_2: 35;

          end;

          

           A35: (( FuncLatt f) . a) = ( gr (f .: the carrier of A1)) & (( FuncLatt f) . b) = ( gr (f .: the carrier of B1)) by A1, A2, Def3;

          consider C1 be strict Subgroup of G1 such that

           A36: C1 = (A1 "\/" B1);

          

           A37: for g1,g2 be Element of G2 st g1 in (f .: the carrier of C1) & g2 in (f .: the carrier of C1) holds (g1 * g2) in (f .: the carrier of C1)

          proof

            let g1,g2 be Element of G2;

            assume that

             A38: g1 in (f .: the carrier of C1) and

             A39: g2 in (f .: the carrier of C1);

            consider x be Element of G1 such that

             A40: x in the carrier of C1 and

             A41: g1 = (f . x) by A38, FUNCT_2: 65;

            consider y be Element of G1 such that

             A42: y in the carrier of C1 and

             A43: g2 = (f . y) by A39, FUNCT_2: 65;

            

             A44: y in C1 by A42, STRUCT_0:def 5;

            x in C1 by A40, STRUCT_0:def 5;

            then (x * y) in C1 by A44, GROUP_2: 50;

            then

             A45: (x * y) in the carrier of C1 by STRUCT_0:def 5;

            (f . (x * y)) = ((f . x) * (f . y)) by GROUP_6:def 6;

            hence thesis by A41, A43, A45, FUNCT_2: 35;

          end;

          

           A46: for g be Element of G2 st g in (f .: the carrier of C1) holds (g " ) in (f .: the carrier of C1)

          proof

            let g be Element of G2;

            assume g in (f .: the carrier of C1);

            then

            consider x be Element of G1 such that

             A47: x in the carrier of C1 and

             A48: g = (f . x) by FUNCT_2: 65;

            x in C1 by A47, STRUCT_0:def 5;

            then (x " ) in C1 by GROUP_2: 51;

            then

             A49: (x " ) in the carrier of C1 by STRUCT_0:def 5;

            (f . (x " )) = ((f . x) " ) by GROUP_6: 32;

            hence thesis by A48, A49, FUNCT_2: 35;

          end;

          ( 1_ G1) in C1 by GROUP_2: 46;

          then ( 1_ G1) in the carrier of C1 by STRUCT_0:def 5;

          then (f .: the carrier of C1) <> {} by A13, A8, FUNCT_1:def 6;

          then

          consider C3 be strict Subgroup of G2 such that

           A50: the carrier of C3 = (f .: the carrier of C1) by A46, A37, GROUP_2: 52;

          ex y be Element of G2 st y = (f . ( 1_ G1));

          then (f .: the carrier of A1) <> {} by A13, A7, FUNCT_1:def 6;

          then

          consider A3 be strict Subgroup of G2 such that

           A51: the carrier of A3 = (f .: the carrier of A1) by A9, A26, GROUP_2: 52;

          

           A52: ( gr (f .: the carrier of B1)) = B3 by A25, Th3;

          the carrier of (A3 "\/" B3) = the carrier of C3

          proof

            

             A53: (f .: the carrier of B1) c= the carrier of C3

            proof

              let x be object;

              assume

               A54: x in (f .: the carrier of B1);

              then

              reconsider x as Element of G2;

              consider y be Element of G1 such that

               A55: y in the carrier of B1 and

               A56: x = (f . y) by A54, FUNCT_2: 65;

              y in A by A55, XBOOLE_0:def 3;

              then y in ( gr A) by GROUP_4: 29;

              then y in the carrier of ( gr A) by STRUCT_0:def 5;

              then y in the carrier of (A1 "\/" B1) by Th4;

              hence thesis by A36, A50, A56, FUNCT_2: 35;

            end;

            (f .: the carrier of A1) c= the carrier of C3

            proof

              let x be object;

              assume

               A57: x in (f .: the carrier of A1);

              then

              reconsider x as Element of G2;

              consider y be Element of G1 such that

               A58: y in the carrier of A1 and

               A59: x = (f . y) by A57, FUNCT_2: 65;

              y in A by A58, XBOOLE_0:def 3;

              then y in ( gr A) by GROUP_4: 29;

              then y in the carrier of ( gr A) by STRUCT_0:def 5;

              then y in the carrier of (A1 "\/" B1) by Th4;

              hence thesis by A36, A50, A59, FUNCT_2: 35;

            end;

            then B c= the carrier of C3 by A53, XBOOLE_1: 8;

            then ( gr B) is Subgroup of C3 by GROUP_4:def 4;

            then the carrier of ( gr B) c= the carrier of C3 by GROUP_2:def 5;

            hence the carrier of (A3 "\/" B3) c= the carrier of C3 by A51, A25, Th4;

            reconsider AA = ((f " the carrier of A3) \/ (f " the carrier of B3)) as Subset of G1;

            

             A60: for g be Element of G1 st g in (f " the carrier of (A3 "\/" B3)) holds (g " ) in (f " the carrier of (A3 "\/" B3))

            proof

              let g be Element of G1;

              assume g in (f " the carrier of (A3 "\/" B3));

              then (f . g) in the carrier of (A3 "\/" B3) by FUNCT_2: 38;

              then (f . g) in (A3 "\/" B3) by STRUCT_0:def 5;

              then ((f . g) " ) in (A3 "\/" B3) by GROUP_2: 51;

              then (f . (g " )) in (A3 "\/" B3) by GROUP_6: 32;

              then (f . (g " )) in the carrier of (A3 "\/" B3) by STRUCT_0:def 5;

              hence thesis by FUNCT_2: 38;

            end;

            the carrier of B1 c= the carrier of G1 by GROUP_2:def 5;

            then

             A61: the carrier of B1 c= (f " the carrier of B3) by A25, FUNCT_2: 42;

            the carrier of A1 c= the carrier of G1 by GROUP_2:def 5;

            then the carrier of A1 c= (f " the carrier of A3) by A51, FUNCT_2: 42;

            then

             A62: A c= AA by A61, XBOOLE_1: 13;

            

             A63: for g1,g2 be Element of G1 st g1 in (f " the carrier of (A3 "\/" B3)) & g2 in (f " the carrier of (A3 "\/" B3)) holds (g1 * g2) in (f " the carrier of (A3 "\/" B3))

            proof

              let g1,g2 be Element of G1;

              assume that

               A64: g1 in (f " the carrier of (A3 "\/" B3)) and

               A65: g2 in (f " the carrier of (A3 "\/" B3));

              (f . g2) in the carrier of (A3 "\/" B3) by A65, FUNCT_2: 38;

              then

               A66: (f . g2) in (A3 "\/" B3) by STRUCT_0:def 5;

              (f . g1) in the carrier of (A3 "\/" B3) by A64, FUNCT_2: 38;

              then (f . g1) in (A3 "\/" B3) by STRUCT_0:def 5;

              then ((f . g1) * (f . g2)) in (A3 "\/" B3) by A66, GROUP_2: 50;

              then (f . (g1 * g2)) in (A3 "\/" B3) by GROUP_6:def 6;

              then (f . (g1 * g2)) in the carrier of (A3 "\/" B3) by STRUCT_0:def 5;

              hence thesis by FUNCT_2: 38;

            end;

            

             A67: (f " the carrier of B3) c= (f " the carrier of (A3 "\/" B3))

            proof

              let x be object;

              assume

               A68: x in (f " the carrier of B3);

              then (f . x) in the carrier of B3 by FUNCT_2: 38;

              then

               A69: (f . x) in B3 by STRUCT_0:def 5;

              (f . x) in the carrier of G2 by A68, FUNCT_2: 5;

              then (f . x) in (A3 "\/" B3) by A69, Th5;

              then (f . x) in the carrier of (A3 "\/" B3) by STRUCT_0:def 5;

              hence thesis by A68, FUNCT_2: 38;

            end;

            ( 1_ G2) in (A3 "\/" B3) by GROUP_2: 46;

            then ( 1_ G2) in the carrier of (A3 "\/" B3) by STRUCT_0:def 5;

            then (f . ( 1_ G1)) in the carrier of (A3 "\/" B3) by GROUP_6: 31;

            then (f " the carrier of (A3 "\/" B3)) <> {} by FUNCT_2: 38;

            then

            consider H be strict Subgroup of G1 such that

             A70: the carrier of H = (f " the carrier of (A3 "\/" B3)) by A60, A63, GROUP_2: 52;

            (f " the carrier of A3) c= (f " the carrier of (A3 "\/" B3))

            proof

              let x be object;

              assume

               A71: x in (f " the carrier of A3);

              then (f . x) in the carrier of A3 by FUNCT_2: 38;

              then

               A72: (f . x) in A3 by STRUCT_0:def 5;

              (f . x) in the carrier of G2 by A71, FUNCT_2: 5;

              then (f . x) in (A3 "\/" B3) by A72, Th5;

              then (f . x) in the carrier of (A3 "\/" B3) by STRUCT_0:def 5;

              hence thesis by A71, FUNCT_2: 38;

            end;

            then ((f " the carrier of A3) \/ (f " the carrier of B3)) c= (f " the carrier of (A3 "\/" B3)) by A67, XBOOLE_1: 8;

            then A c= the carrier of H by A62, A70;

            then ( gr A) is Subgroup of H by GROUP_4:def 4;

            then the carrier of ( gr A) c= the carrier of H by GROUP_2:def 5;

            then

             A73: the carrier of C1 c= (f " the carrier of (A3 "\/" B3)) by A36, A70, Th4;

            

             A74: (f .: the carrier of C1) c= (f .: (f " the carrier of (A3 "\/" B3)))

            proof

              let x be object;

              assume

               A75: x in (f .: the carrier of C1);

              then

              reconsider x as Element of G2;

              ex y be Element of G1 st y in the carrier of C1 & x = (f . y) by A75, FUNCT_2: 65;

              hence thesis by A73, FUNCT_2: 35;

            end;

            (f .: (f " the carrier of (A3 "\/" B3))) c= the carrier of (A3 "\/" B3) by FUNCT_1: 75;

            hence thesis by A50, A74;

          end;

          

          then ( gr (f .: the carrier of (A1 "\/" B1))) = (A3 "\/" B3) by A36, A50, Th3

          .= (( gr (f .: the carrier of A1)) "\/" ( gr (f .: the carrier of B1))) by A51, A52, Th3

          .= ((( FuncLatt f) . a) "\/" (( FuncLatt f) . b)) by A35, Th22;

          hence thesis by A1, A2, A24, Th22;

        end;

      end;

      hence thesis by LATTICE4:def 1;

    end;

    theorem :: LATSUBGR:33

    for G1,G2 be Group holds for f be Homomorphism of G1, G2 st f is one-to-one holds ( FuncLatt f) is Homomorphism of ( lattice G1), ( lattice G2) by Th31, Th32;