Volume 3, 1991

University of Bialystok

Copyright (c) 1991 Association of Mizar Users

### The abstract of the Mizar article:

### Commutator and Center of a Group

**by****Wojciech A. Trybulec**- Received May 15, 1991
- MML identifier: GROUP_5

- [ Mizar article, MML identifier index ]

environ vocabulary INT_1, REALSET1, GROUP_2, GROUP_3, FINSEQ_1, GROUP_1, RELAT_1, LATTICES, BINOP_1, FUNCT_1, BOOLE, QC_LANG1, RCOMP_1, ARYTM_1, GROUP_4, RLSUB_1, VECTSP_1, SUBSET_1, FINSET_1, CARD_1, TARSKI, GROUP_5, CARD_3, FINSEQ_4; notation TARSKI, XBOOLE_0, SUBSET_1, NAT_1, STRUCT_0, XCMPLX_0, FUNCT_1, CARD_1, FINSEQ_1, FINSET_1, FINSEQ_4, INT_1, RLVECT_1, VECTSP_1, GROUP_1, GROUP_2, GROUP_3, GROUP_4, DOMAIN_1; constructors REAL_1, GROUP_4, DOMAIN_1, NAT_1, FINSEQ_4, MEMBERED, XBOOLE_0; clusters CARD_1, INT_1, GROUP_1, GROUP_2, GROUP_3, RELSET_1, STRUCT_0, MEMBERED, ZFMISC_1, XBOOLE_0; requirements NUMERALS, BOOLE, SUBSET; begin :: Preliminaries. scheme SubsetFD3{C,D,E() -> non empty set, F(set,set,set) -> Element of D(), P[set,set,set]}: {F(c,d,e) where c is Element of C(),d is Element of D(), e is Element of E() : P[c,d,e]} is Subset of D(); reserve x,y for set, k,n for Nat, i for Integer, G for Group, a,b,c,d,e for Element of G, A,B,C,D for Subset of G, H,H1,H2,H3,H4 for Subgroup of G, N1,N2 for normal Subgroup of G, F,F1,F2 for FinSequence of the carrier of G, I,I1,I2 for FinSequence of INT; theorem :: GROUP_5:1 x in (1).G iff x = 1.G; theorem :: GROUP_5:2 a in H & b in H implies a |^ b in H; theorem :: GROUP_5:3 for N being strict normal Subgroup of G holds a in N implies a |^ b in N; theorem :: GROUP_5:4 x in H1 * H2 iff ex a,b st x = a * b & a in H1 & b in H2; theorem :: GROUP_5:5 H1 * H2 = H2 * H1 implies (x in H1 "\/" H2 iff ex a,b st x = a * b & a in H1 & b in H2); theorem :: GROUP_5:6 G is commutative Group implies (x in H1 "\/" H2 iff ex a,b st x = a * b & a in H1 & b in H2); theorem :: GROUP_5:7 for N1,N2 being strict normal Subgroup of G holds x in N1 "\/" N2 iff ex a,b st x = a * b & a in N1 & b in N2; theorem :: GROUP_5:8 for N being normal Subgroup of G holds H * N = N * H; definition let G,F,a; func F |^ a -> FinSequence of the carrier of G means :: GROUP_5:def 1 len it = len F & for k st k in dom F holds it.k = (F/.k) |^ a; end; canceled 3; theorem :: GROUP_5:12 (F1 |^ a) ^ (F2 |^ a) = (F1 ^ F2) |^ a; theorem :: GROUP_5:13 (<*> the carrier of G) |^ a = {}; theorem :: GROUP_5:14 <* a *> |^ b = <* a |^ b *>; theorem :: GROUP_5:15 <* a,b *> |^ c = <* a |^ c,b |^ c *>; theorem :: GROUP_5:16 <* a,b,c *> |^ d = <* a |^ d,b |^ d,c |^ d *>; theorem :: GROUP_5:17 Product(F |^ a) = Product(F) |^ a; theorem :: GROUP_5:18 (F |^ a) |^ I = (F |^ I) |^ a; begin :: Commutators. definition let G,a,b; func [.a,b.] -> Element of G equals :: GROUP_5:def 2 a" * b" * a * b; end; theorem :: GROUP_5:19 [.a,b.] = a" * b" * a * b & [.a,b.] = a" * (b" * a) * b & [.a,b.] = a" * (b" * a * b) & [.a,b.] = a" * (b" * (a * b)) & [.a,b.] = (a" * b") * (a * b); theorem :: GROUP_5:20 [.a,b.] = (b * a)" * (a * b); theorem :: GROUP_5:21 [.a,b.] = (b" |^ a) * b & [.a,b.] = a" * (a |^ b); theorem :: GROUP_5:22 [.1.G,a.] = 1.G & [.a,1.G.] = 1.G; theorem :: GROUP_5:23 [.a,a.] = 1.G; theorem :: GROUP_5:24 [.a,a".] = 1.G & [.a",a.] = 1.G; theorem :: GROUP_5:25 [.a,b.]" = [.b,a.]; theorem :: GROUP_5:26 [.a,b.] |^ c = [.a |^ c,b |^ c.]; theorem :: GROUP_5:27 [.a,b.] = (a" |^ 2) * ((a * b") |^ 2)* (b |^ 2); theorem :: GROUP_5:28 [.a * b,c.] = [.a,c.] |^ b * [.b,c.]; theorem :: GROUP_5:29 [.a,b * c.] = [.a,c.] * ([.a,b.] |^ c); theorem :: GROUP_5:30 [.a",b.] = [.b,a.] |^ a"; theorem :: GROUP_5:31 [.a,b".] = [.b,a.] |^ b"; theorem :: GROUP_5:32 [.a",b".] = [.a,b.] |^ (a * b)" & [.a",b".] = [.a,b.] |^ (b * a)"; theorem :: GROUP_5:33 [.a,b |^ a".] = [.b,a".]; theorem :: GROUP_5:34 [.a |^ b",b.] = [.b",a.]; theorem :: GROUP_5:35 [.a |^ n,b.] = a |^ (- n) * ((a |^ b) |^ n); theorem :: GROUP_5:36 [.a,b |^ n.] = (b |^ a) |^ (- n) * (b |^ n); theorem :: GROUP_5:37 [.a |^ i,b.] = a |^ (- i) * ((a |^ b) |^ i); theorem :: GROUP_5:38 [.a,b |^ i.] = (b |^ a) |^ (- i) * (b |^ i); theorem :: GROUP_5:39 [.a,b.] = 1.G iff a * b = b * a; theorem :: GROUP_5:40 G is commutative Group iff for a,b holds [.a,b.] = 1.G; theorem :: GROUP_5:41 a in H & b in H implies [.a,b.] in H; definition let G,a,b,c; func [.a,b,c.] -> Element of G equals :: GROUP_5:def 3 [.[.a,b.],c.]; end; canceled; theorem :: GROUP_5:43 [.a,b,1.G.] = 1.G & [.a,1.G,b.] = 1.G & [.1.G,a,b.] = 1.G; theorem :: GROUP_5:44 [.a,a,b.] = 1.G; theorem :: GROUP_5:45 [.a,b,a.] = [.a |^ b,a.]; theorem :: GROUP_5:46 [.b,a,a.] = ([.b,a".] * [.b,a.]) |^ a; theorem :: GROUP_5:47 [.a,b,b |^ a.] = [.b,[.b,a.].]; theorem :: GROUP_5:48 [.a * b,c.] = [.a,c.] * [.a,c,b.] * [.b,c.]; theorem :: GROUP_5:49 [.a,b * c.] = [.a,c.] * [.a,b.] * [.a,b,c.]; :: :: P. Hall Identity. :: theorem :: GROUP_5:50 ([.a,b",c.] |^ b) * ([.b,c",a.] |^ c) * ([.c,a",b.] |^ a) = 1.G; definition let G,A,B; func commutators(A,B) -> Subset of G equals :: GROUP_5:def 4 {[.a,b.] : a in A & b in B}; end; canceled; theorem :: GROUP_5:52 x in commutators(A,B) iff ex a,b st x = [.a,b.] & a in A & b in B; theorem :: GROUP_5:53 commutators({} the carrier of G,A) = {} & commutators(A,{} the carrier of G) = {}; theorem :: GROUP_5:54 commutators({a},{b}) = {[.a,b.]}; theorem :: GROUP_5:55 A c= B & C c= D implies commutators(A,C) c= commutators(B,D); theorem :: GROUP_5:56 G is commutative Group iff for A,B st A <> {} & B <> {} holds commutators(A,B) = {1.G}; definition let G,H1,H2; func commutators(H1,H2) -> Subset of G equals :: GROUP_5:def 5 commutators(carr H1,carr H2); end; canceled; theorem :: GROUP_5:58 x in commutators(H1,H2) iff ex a,b st x = [.a,b.] & a in H1 & b in H2; theorem :: GROUP_5:59 1.G in commutators(H1,H2); theorem :: GROUP_5:60 commutators((1).G,H) = {1.G} & commutators(H,(1).G) = {1.G}; theorem :: GROUP_5:61 for N being strict normal Subgroup of G holds commutators(H,N) c= carr N & commutators(N,H) c= carr N; theorem :: GROUP_5:62 H1 is Subgroup of H2 & H3 is Subgroup of H4 implies commutators(H1,H3) c= commutators(H2,H4); theorem :: GROUP_5:63 G is commutative Group iff for H1,H2 holds commutators(H1,H2) = {1.G}; definition let G; func commutators G -> Subset of G equals :: GROUP_5:def 6 commutators((Omega).G,(Omega).G); end; canceled; theorem :: GROUP_5:65 x in commutators G iff ex a,b st x = [.a,b.]; theorem :: GROUP_5:66 G is commutative Group iff commutators G = {1.G}; definition let G,A,B; func [.A,B.] -> strict Subgroup of G equals :: GROUP_5:def 7 gr commutators(A,B); end; canceled; theorem :: GROUP_5:68 a in A & b in B implies [.a,b.] in [.A,B.]; theorem :: GROUP_5:69 x in [.A,B.] iff ex F,I st len F = len I & rng F c= commutators(A,B) & x = Product(F |^ I); theorem :: GROUP_5:70 A c= C & B c= D implies [.A,B.] is Subgroup of [.C,D.]; definition let G,H1,H2; func [.H1,H2.] -> strict Subgroup of G equals :: GROUP_5:def 8 [.carr H1,carr H2.]; end; canceled; theorem :: GROUP_5:72 [.H1,H2.] = gr commutators(H1,H2); theorem :: GROUP_5:73 x in [.H1,H2.] iff ex F,I st len F = len I & rng F c= commutators(H1,H2) & x = Product(F |^ I); theorem :: GROUP_5:74 a in H1 & b in H2 implies [.a,b.] in [.H1,H2.]; theorem :: GROUP_5:75 H1 is Subgroup of H2 & H3 is Subgroup of H4 implies [.H1,H3.] is Subgroup of [.H2,H4.]; theorem :: GROUP_5:76 for N being strict normal Subgroup of G holds [.N,H.] is Subgroup of N & [.H,N.] is Subgroup of N; theorem :: GROUP_5:77 for N1,N2 being strict normal Subgroup of G holds [.N1,N2.] is normal Subgroup of G; theorem :: GROUP_5:78 [.N1,N2.] = [.N2,N1.]; theorem :: GROUP_5:79 for N1,N2,N3 being strict normal Subgroup of G holds [.N1 "\/" N2,N3.] = [.N1,N3.] "\/" [.N2,N3.]; theorem :: GROUP_5:80 for N1,N2,N3 being strict normal Subgroup of G holds [.N1,N2 "\/" N3.] = [.N1,N2.] "\/" [.N1,N3.]; definition let G be Group; func G` -> strict normal Subgroup of G equals :: GROUP_5:def 9 [.(Omega).G,(Omega).G.]; end; canceled; theorem :: GROUP_5:82 for G being Group holds G` = gr commutators G; theorem :: GROUP_5:83 for G being Group holds x in G` iff ex F being FinSequence of the carrier of G,I st len F = len I & rng F c= commutators G & x = Product(F |^ I); theorem :: GROUP_5:84 for G being strict Group, a,b be Element of G holds [.a,b.] in G`; theorem :: GROUP_5:85 for G being strict Group holds G is commutative Group iff G` = (1).G; theorem :: GROUP_5:86 for G being Group, H being strict Subgroup of G holds Left_Cosets H is finite & index H = 2 implies G` is Subgroup of H; begin :: Center of a Group. definition let G; func center G -> strict Subgroup of G means :: GROUP_5:def 10 the carrier of it = {a : for b holds a * b = b * a}; end; canceled 2; theorem :: GROUP_5:89 a in center G iff for b holds a * b = b * a; theorem :: GROUP_5:90 center G is normal Subgroup of G; theorem :: GROUP_5:91 for H being Subgroup of G holds H is Subgroup of center G implies H is normal Subgroup of G; theorem :: GROUP_5:92 center G is commutative; theorem :: GROUP_5:93 a in center G iff con_class a = {a}; theorem :: GROUP_5:94 for G being strict Group holds G is commutative Group iff center G = G; begin :: Auxiliary theorems. reserve E for non empty set, p, q for FinSequence of E; theorem :: GROUP_5:95 k in dom p implies (p ^ q)/.k = p/.k; theorem :: GROUP_5:96 k in dom q implies (p ^ q)/.(len p + k) = q/.k;

Back to top