The abstract of the Mizar article:

Lattice of Subgroups of a Group. Frattini Subgroup

by

Wojciech A. Trybulec

Received August 22, 1990

MML identifier: GROUP_4

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_1, ARYTM_1, REALSET1, GROUP_2, SETFAM_1, GROUP_1, BOOLE,
      RELAT_1, INT_1, GROUP_3, QC_LANG1, ABSVALUE, VECTSP_1, FINSOP_1, BINOP_1,
      SETWISEO, FUNCT_1, FINSEQ_2, FUNCT_2, RLSUB_1, TARSKI, LATTICES, NAT_1,
      SUBSET_1, RLSUB_2, GROUP_4, CARD_3, FINSEQ_4, ORDINAL2, ARYTM;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XREAL_0, FINSOP_1,
      ORDINAL1, ORDINAL2, INT_1, SETWISEO, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2,
      FINSEQ_1, FINSEQ_3, FINSEQ_4, BINOP_1, STRUCT_0, RLVECT_1, VECTSP_1,
      GROUP_2, GROUP_3, LATTICES, GROUP_1, DOMAIN_1, NAT_1;
 constructors FINSOP_1, SETWISEO, FUNCSDOM, FINSEQ_3, GROUP_3, LATTICES,
      DOMAIN_1, NAT_1, FINSEQ_4, MEMBERED, XBOOLE_0, ORDINAL2, ORDINAL1;
 clusters SUBSET_1, FINSEQ_1, GROUP_3, INT_1, LATTICES, GROUP_1, RELSET_1,
      STRUCT_0, RLSUB_2, GROUP_2, XREAL_0, ZFMISC_1, XBOOLE_0, ORDINAL2,
      NUMBERS, ARYTM_3;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin

definition let D be non empty set; let F be FinSequence of D; let X be set;
 redefine func F - X -> FinSequence of D;
end;

scheme MeetSbgEx{G() -> Group, P[set]}:
 ex H being strict Subgroup of G() st
  the carrier of H =
    meet{A where A is Subset of G() :
          ex K being strict Subgroup of G() st A = the carrier of K & P[K]}
 provided
   ex H being strict Subgroup of G() st P[H];

reserve x,y,y1,y2,X,Y for set,
        k,l,m,n for Nat,
        i,i1,i2,i3,j for Integer,
        G for Group,
        a,b,c,d for Element of G,
        A,B,C for Subset of G,
        H,H1,H2,H3 for Subgroup of G,
        h for Element of H,
        F,F1,F2 for FinSequence of the carrier of G,
        I,I1,I2 for FinSequence of INT;

scheme SubgrSep{G() -> Group,P[set]}:
 ex X st X c= Subgroups G() &
  for H being strict Subgroup of G() holds H in X iff P[H];

definition let i;
 canceled;

 func @i -> Element of INT equals
:: GROUP_4:def 2
    i;
end;

canceled 2;

theorem :: GROUP_4:3
 a = h implies a |^ n = h |^ n;

theorem :: GROUP_4:4
   a = h implies a |^ i = h |^ i;

theorem :: GROUP_4:5
 a in H implies a |^ n in H;

theorem :: GROUP_4:6
 a in H implies a |^ i in H;

definition let G be non empty HGrStr;
 let F be FinSequence of the carrier of G;
 func Product F -> Element of G equals
:: GROUP_4:def 3
    (the mult of G) "**" F;
end;

canceled;

theorem :: GROUP_4:8
 for G being associative unital (non empty HGrStr),
     F1,F2 being FinSequence of the carrier of G
 holds Product(F1 ^ F2) = Product(F1) * Product(F2);

theorem :: GROUP_4:9
 for G being unital (non empty HGrStr),
     F being FinSequence of the carrier of G,
     a being Element of G
 holds Product(F ^ <* a *>) = Product(F) * a;

theorem :: GROUP_4:10
  for G being associative unital (non empty HGrStr),
     F being FinSequence of the carrier of G,
     a being Element of G
 holds Product(<* a *> ^ F) = a * Product(F);

theorem :: GROUP_4:11
 for G being unital (non empty HGrStr)
 holds Product <*> the carrier of G = 1.G;

theorem :: GROUP_4:12
for G being non empty HGrStr, a being Element of G holds
 Product<* a *> = a;

theorem :: GROUP_4:13
for G being non empty HGrStr, a,b being Element of G holds
 Product<* a,b *> = a * b;

theorem :: GROUP_4:14
   Product<* a,b,c *> = a * b * c & Product<* a,b,c *> = a * (b * c);

theorem :: GROUP_4:15
   Product(n |-> a) = a |^ n;

theorem :: GROUP_4:16
   Product(F - {1.G}) = Product(F);

theorem :: GROUP_4:17
 len F1 = len F2 &
  (for k st k in dom F1 holds F2.(len F1 - k + 1) = (F1/.k)") implies
   Product(F1) = Product(F2)";

theorem :: GROUP_4:18
   G is commutative Group implies
  for P being Permutation of dom F1 st F2 = F1 * P holds
   Product(F1) = Product(F2);

theorem :: GROUP_4:19
   G is commutative Group & F1 is one-to-one & F2 is one-to-one & rng F1 = rng
F2
  implies Product(F1) = Product(F2);

theorem :: GROUP_4:20
   G is commutative Group & len F = len F1 & len F = len F2 &
  (for k st k in dom F holds F.k = (F1/.k) * (F2/.k)) implies
   Product(F) = Product(F1) * Product(F2);

theorem :: GROUP_4:21
 rng F c= carr H implies Product(F) in H;

definition let G,I,F;
 func F |^ I -> FinSequence of the carrier of G means
:: GROUP_4:def 4
   len it = len F &
        for k st k in dom F holds it.k = (F/.k) |^ @(I/.k);
end;

canceled 3;

theorem :: GROUP_4:25
 len F1 = len I1 & len F2 = len I2 implies
  (F1 ^ F2) |^ (I1 ^ I2) = (F1 |^ I1) ^ (F2 |^ I2);

theorem :: GROUP_4:26
 rng F c= carr H implies Product(F |^ I) in H;

theorem :: GROUP_4:27
 (<*> the carrier of G) |^ (<*> INT) = {};

theorem :: GROUP_4:28
 <* a *> |^ <* @i *> = <* a |^ i *>;

theorem :: GROUP_4:29
 <* a,b *> |^ <* @i,@j *> = <* a |^ i,b |^ j *>;

theorem :: GROUP_4:30
   <* a,b,c *> |^ <* @i1,@i2,@i3 *> = <* a |^ i1,b |^ i2,c |^ i3 *>;

theorem :: GROUP_4:31
   F |^ (len F |-> @(1)) = F;

theorem :: GROUP_4:32
   F |^ (len F |-> @(0)) = len F |-> 1.G;

theorem :: GROUP_4:33
   len I = n implies (n |-> 1.G) |^ I = n |-> 1.G;

definition let G,A;
 func gr A -> strict Subgroup of G means
:: GROUP_4:def 5
   A c= the carrier of it &
       (for H being strict Subgroup of G
         st A c= the carrier of H holds it is Subgroup of H);
end;

canceled 3;

theorem :: GROUP_4:37
 a in gr A iff ex F,I st len F = len I & rng F c= A & Product(F |^ I) = a;

theorem :: GROUP_4:38
 a in A implies a in gr A;

theorem :: GROUP_4:39
   gr {} the carrier of G = (1).G;

theorem :: GROUP_4:40
 for H being strict Subgroup of G holds gr carr H = H;

theorem :: GROUP_4:41
 A c= B implies gr A is Subgroup of gr B;

theorem :: GROUP_4:42
   gr(A /\ B) is Subgroup of gr A /\ gr B;

theorem :: GROUP_4:43
 the carrier of gr A =
  meet{B : ex H being strict Subgroup of G
   st B = the carrier of H & A c= carr H};

theorem :: GROUP_4:44
 gr A = gr(A \ {1.G});

definition let G,a;
 attr a is generating means
:: GROUP_4:def 6

   not for A st gr A = the HGrStr of G holds gr(A \ {a}) = the HGrStr of G;
end;

canceled;

theorem :: GROUP_4:46
   1.G is non generating;

definition let G, H;
 attr H is maximal means
:: GROUP_4:def 7
   the HGrStr of H <> the HGrStr of G &
   for K being strict Subgroup of G st
    the HGrStr of H <> K & H is Subgroup of K
     holds K = the HGrStr of G;
end;

canceled;

theorem :: GROUP_4:48
 for G being strict Group, H being strict Subgroup of G,
    a being Element of G holds
 H is maximal & not a in H implies gr(carr H \/ {a}) = G;

::
::  Frattini subgroup.
::

definition let G be Group;
 func Phi(G) -> strict Subgroup of G means
:: GROUP_4:def 8
   the carrier of it =
              meet{A where A is Subset of G :
                 ex H being strict Subgroup of G
                 st A = the carrier of H & H is maximal} if
               ex H being strict Subgroup of G st H is maximal otherwise
             it = the HGrStr of G;
end;

canceled 3;

theorem :: GROUP_4:52
 for G being Group holds
 (ex H being strict Subgroup of G st H is maximal) implies
  (a in Phi(G) iff
    for H being strict Subgroup of G st H is maximal holds a in H);

theorem :: GROUP_4:53
   for G being Group, a being Element of G holds
 (for H being strict Subgroup of G holds H is not maximal) implies a in Phi(G);

theorem :: GROUP_4:54
 for G being Group, H being strict Subgroup of G holds
 H is maximal implies Phi(G) is Subgroup of H;

theorem :: GROUP_4:55
 for G being strict Group holds
 the carrier of Phi(G) = {a where a is Element of
 G: a is non generating};

theorem :: GROUP_4:56
   for G being strict Group, a being Element of G holds
  a in Phi(G) iff a is non generating;

definition let G,H1,H2;
 func H1 * H2 -> Subset of G equals
:: GROUP_4:def 9
    carr H1 * carr H2;
end;

theorem :: GROUP_4:57
 H1 * H2 = carr H1 * carr H2 & H1 * H2 = H1 * carr H2 &
  H1 * H2 = carr H1 * H2;

theorem :: GROUP_4:58
   H * H = carr H;

theorem :: GROUP_4:59
   H1 * H2 * H3 = H1 * (H2 * H3);

theorem :: GROUP_4:60
   a * H1 * H2 = a * (H1 * H2);

theorem :: GROUP_4:61
   H1 * H2 * a = H1 * (H2 * a);

theorem :: GROUP_4:62
   A * H1 * H2 = A * (H1 * H2);

theorem :: GROUP_4:63
   H1 * H2 * A = H1 * (H2 * A);

theorem :: GROUP_4:64
 for N1,N2 being strict normal Subgroup of G
 holds N1 * N2 = N2 * N1;

theorem :: GROUP_4:65
 G is commutative Group implies H1 * H2 = H2 * H1;

definition let G,H1,H2;
 func H1 "\/" H2 -> strict Subgroup of G equals
:: GROUP_4:def 10
    gr(carr H1 \/ carr H2);
end;

canceled;

theorem :: GROUP_4:67
 a in H1 "\/" H2 iff
  ex F,I st len F = len I & rng F c= carr H1 \/ carr H2 & a = Product(F |^ I);

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

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

theorem :: GROUP_4:70
   G is commutative Group implies the carrier of H1 "\/" H2 = H1 * H2;

theorem :: GROUP_4:71
 for N1,N2 being strict normal Subgroup of G
 holds the carrier of N1 "\/" N2 = N1 * N2;

theorem :: GROUP_4:72
   for N1,N2 being strict normal Subgroup of G
  holds N1 "\/" N2 is normal Subgroup of G;

theorem :: GROUP_4:73
 for H being strict Subgroup of G holds H "\/" H = H;

theorem :: GROUP_4:74
 H1 "\/" H2 = H2 "\/" H1;

theorem :: GROUP_4:75
 H1 "\/" H2 "\/" H3 = H1 "\/" (H2 "\/" H3);

theorem :: GROUP_4:76
   for H being strict Subgroup of G holds
 (1).G "\/" H = H & H "\/" (1).G = H;

theorem :: GROUP_4:77
 (Omega).G "\/" H = (Omega).G & H "\/" (Omega).G = (Omega).G;

theorem :: GROUP_4:78
 H1 is Subgroup of H1 "\/" H2 & H2 is Subgroup of H1 "\/" H2;

theorem :: GROUP_4:79
 for H2 being strict Subgroup of G holds
 H1 is Subgroup of H2 iff H1 "\/" H2 = H2;

theorem :: GROUP_4:80
   H1 is Subgroup of H2 implies H1 is Subgroup of H2 "\/" H3;

theorem :: GROUP_4:81
   for H3 being strict Subgroup of G holds
 H1 is Subgroup of H3 & H2 is Subgroup of H3 implies H1 "\/"
 H2 is Subgroup of H3;

theorem :: GROUP_4:82
   for H3,H2 being strict Subgroup of G holds
 H1 is Subgroup of H2 implies H1 "\/" H3 is Subgroup of H2 "\/" H3;

theorem :: GROUP_4:83
   H1 /\ H2 is Subgroup of H1 "\/" H2;

theorem :: GROUP_4:84
 for H2 being strict Subgroup of G holds (H1 /\ H2) "\/" H2 = H2;

theorem :: GROUP_4:85
 for H1 being strict Subgroup of G holds H1 /\ (H1 "\/" H2) = H1;

theorem :: GROUP_4:86
   for H1,H2 being strict Subgroup of G holds H1 "\/" H2 = H2 iff H1 /\ H2 = H1
;

reserve S1,S2 for Element of Subgroups G;

definition let G;
 func SubJoin G -> BinOp of Subgroups G means
:: GROUP_4:def 11
   for S1,S2,H1,H2 st S1 = H1 & S2 = H2 holds it.(S1,S2) = H1 "\/" H2;
end;

definition let G;
 func SubMeet G -> BinOp of Subgroups G means
:: GROUP_4:def 12
   for S1,S2,H1,H2 st S1 = H1 & S2 = H2 holds it.(S1,S2) = H1 /\ H2;
end;

definition let G be Group;
 func lattice G -> strict Lattice equals
:: GROUP_4:def 13
    LattStr (# Subgroups G, SubJoin G, SubMeet G #);
end;

canceled 5;

theorem :: GROUP_4:92
 for G being Group holds
 the carrier of lattice G = Subgroups G;

theorem :: GROUP_4:93
 for G being Group holds
 the L_join of lattice G = SubJoin G;

theorem :: GROUP_4:94
 for G being Group holds
 the L_meet of lattice G = SubMeet G;

definition let G be Group;
  cluster lattice G -> lower-bounded upper-bounded;
end;

canceled 3;

theorem :: GROUP_4:98
   for G being Group holds Bottom lattice G = (1).G;

theorem :: GROUP_4:99
   for G being Group holds Top lattice G = (Omega).G;

::
::  Auxiliary theorems.
::

 reserve k, l, m, n for natural number;

theorem :: GROUP_4:100
   n mod 2 = 0 or n mod 2 = 1;

theorem :: GROUP_4:101
  for k, n being Nat holds (k * n) mod k = 0;

theorem :: GROUP_4:102
   k > 1 implies 1 mod k = 1;

theorem :: GROUP_4:103
   k mod n = 0 & l = k - m * n implies l mod n = 0;

 reserve k, n, l, m for Nat;

theorem :: GROUP_4:104
    n <> 0 & k mod n = 0 & l < n implies k + l mod n = l;

theorem :: GROUP_4:105
   k mod n = 0 implies k + l mod n = l mod n;

theorem :: GROUP_4:106
   n <> 0 & k mod n = 0 implies
  (k + l) div n = (k div n) + (l div n);

theorem :: GROUP_4:107
   k <> 0 implies (k * n) div k = n;