Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Subgroup and Cosets of Subgroups

**by****Wojciech A. Trybulec**- Received July 23, 1990
- MML identifier: GROUP_2

- [ Mizar article, MML identifier index ]

environ vocabulary FINSET_1, REALSET1, RELAT_1, BOOLE, SUBSET_1, VECTSP_1, BINOP_1, GROUP_1, FUNCT_1, RLSUB_1, CARD_1, TARSKI, SETFAM_1, FINSUB_1, SETWISEO, ARYTM_3, GROUP_2; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, SETFAM_1, FINSUB_1, FINSET_1, STRUCT_0, RLVECT_1, VECTSP_1, WELLORD2, GROUP_1, CARD_1, BINOP_1, SETWISEO, DOMAIN_1, RELAT_1, FUNCT_1, RELSET_1, NAT_1, MCART_1; constructors WELLORD2, GROUP_1, BINOP_1, SETWISEO, DOMAIN_1, NAT_1, PARTFUN1, MEMBERED, XBOOLE_0; clusters SUBSET_1, FINSET_1, FINSUB_1, GROUP_1, FUNCT_1, STRUCT_0, RELSET_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin reserve x for set; reserve G for non empty 1-sorted; reserve A for Subset of G; canceled 2; theorem :: GROUP_2:3 G is finite implies A is finite; reserve y,y1,y2,Y,Z for set; reserve k for Nat; reserve G for Group; reserve a,g,h for Element of G; reserve A for Subset of G; definition let G,A; func A" -> Subset of G equals :: GROUP_2:def 1 {g" : g in A}; end; canceled; theorem :: GROUP_2:5 x in A" iff ex g st x = g" & g in A; theorem :: GROUP_2:6 {g}" = {g"}; theorem :: GROUP_2:7 {g,h}" = {g",h"}; theorem :: GROUP_2:8 ({}(the carrier of G))" = {}; theorem :: GROUP_2:9 ([#](the carrier of G))" = the carrier of G; theorem :: GROUP_2:10 A <> {} iff A" <> {}; reserve G for non empty HGrStr,A,B,C for Subset of G; reserve a,b,g,g1,g2,h,h1,h2 for Element of G; definition let G; let A,B; func A * B -> Subset of G equals :: GROUP_2:def 2 {g * h : g in A & h in B}; end; canceled; theorem :: GROUP_2:12 x in A * B iff ex g,h st x = g * h & g in A & h in B; theorem :: GROUP_2:13 A <> {} & B <> {} iff A * B <> {}; theorem :: GROUP_2:14 G is associative implies A * B * C = A * (B * C); theorem :: GROUP_2:15 for G being Group, A,B being Subset of G holds (A * B)" = B" * A"; theorem :: GROUP_2:16 A * (B \/ C) = A * B \/ A * C; theorem :: GROUP_2:17 (A \/ B) * C = A * C \/ B * C; theorem :: GROUP_2:18 A * (B /\ C) c= (A * B) /\ (A * C); theorem :: GROUP_2:19 (A /\ B) * C c= (A * C) /\ (B * C); theorem :: GROUP_2:20 {}(the carrier of G) * A = {} & A * {}(the carrier of G) = {}; theorem :: GROUP_2:21 for G being Group, A being Subset of G holds A <> {} implies [#](the carrier of G) * A = the carrier of G & A * [#](the carrier of G) = the carrier of G; theorem :: GROUP_2:22 {g} * {h} = {g * h}; theorem :: GROUP_2:23 {g} * {g1,g2} = {g * g1,g * g2}; theorem :: GROUP_2:24 {g1,g2} * {g} = {g1 * g,g2 * g}; theorem :: GROUP_2:25 {g,h} * {g1,g2} = {g * g1, g * g2, h * g1, h * g2}; theorem :: GROUP_2:26 for G being Group, A being Subset of G holds (for g1,g2 being Element of G st g1 in A & g2 in A holds g1 * g2 in A) & (for g being Element of G st g in A holds g" in A) implies A * A = A; theorem :: GROUP_2:27 for G being Group, A being Subset of G holds (for g being Element of G st g in A holds g" in A) implies A" = A; theorem :: GROUP_2:28 (for a,b st a in A & b in B holds a * b = b * a) implies A * B = B * A; theorem :: GROUP_2:29 G is commutative Group implies A * B = B * A; theorem :: GROUP_2:30 for G being commutative Group, A,B being Subset of G holds (A * B)" = A" * B"; definition let G,g,A; func g * A -> Subset of G equals :: GROUP_2:def 3 {g} * A; func A * g -> Subset of G equals :: GROUP_2:def 4 A * {g}; end; canceled 2; theorem :: GROUP_2:33 x in g * A iff ex h st x = g * h & h in A; theorem :: GROUP_2:34 x in A * g iff ex h st x = h * g & h in A; theorem :: GROUP_2:35 G is associative implies g * A * B = g * (A * B); theorem :: GROUP_2:36 G is associative implies A * g * B = A * (g * B); theorem :: GROUP_2:37 G is associative implies A * B * g = A * (B * g); theorem :: GROUP_2:38 G is associative implies g * h * A = g * (h * A); theorem :: GROUP_2:39 G is associative implies g * A * h = g * (A * h); theorem :: GROUP_2:40 G is associative implies A * g * h = A * (g * h); theorem :: GROUP_2:41 {}(the carrier of G) * a = {} & a * {}(the carrier of G) = {}; reserve G for Group-like (non empty HGrStr); reserve h,g,g1,g2 for Element of G; reserve A for Subset of G; theorem :: GROUP_2:42 for G being Group, a being Element of G holds [#](the carrier of G) * a = the carrier of G & a * [#](the carrier of G) = the carrier of G; theorem :: GROUP_2:43 1.G * A = A & A * 1.G = A; theorem :: GROUP_2:44 G is commutative Group implies g * A = A * g; definition let G be Group-like (non empty HGrStr); mode Subgroup of G -> Group-like (non empty HGrStr) means :: GROUP_2:def 5 the carrier of it c= the carrier of G & the mult of it = (the mult of G) | [:the carrier of it,the carrier of it:]; end; reserve H for Subgroup of G; reserve h,h1,h2 for Element of H; canceled 3; theorem :: GROUP_2:48 G is finite implies H is finite; theorem :: GROUP_2:49 x in H implies x in G; theorem :: GROUP_2:50 h in G; theorem :: GROUP_2:51 h is Element of G; theorem :: GROUP_2:52 h1 = g1 & h2 = g2 implies h1 * h2 = g1 * g2; definition let G be Group; cluster -> associative Subgroup of G; end; reserve G,G1,G2,G3 for Group; reserve a,a1,a2,b,b1,b2,g,g1,g2 for Element of G; reserve A,B for Subset of G; reserve I,H,H1,H2,H3 for Subgroup of G; reserve h,h1,h2 for Element of H; theorem :: GROUP_2:53 1.H = 1.G; theorem :: GROUP_2:54 1.H1 = 1.H2; theorem :: GROUP_2:55 1.G in H; theorem :: GROUP_2:56 1.H1 in H2; theorem :: GROUP_2:57 h = g implies h" = g"; theorem :: GROUP_2:58 inverse_op(H) = inverse_op(G) | the carrier of H; theorem :: GROUP_2:59 g1 in H & g2 in H implies g1 * g2 in H; theorem :: GROUP_2:60 g in H implies g" in H; definition let G; cluster strict Subgroup of G; end; theorem :: GROUP_2:61 A <> {} & (for g1,g2 st g1 in A & g2 in A holds g1 * g2 in A) & (for g st g in A holds g" in A) implies ex H being strict Subgroup of G st the carrier of H = A; theorem :: GROUP_2:62 G is commutative Group implies H is commutative; definition let G be commutative Group; cluster -> commutative Subgroup of G; end; theorem :: GROUP_2:63 G is Subgroup of G; theorem :: GROUP_2:64 G1 is Subgroup of G2 & G2 is Subgroup of G1 implies the HGrStr of G1 = the HGrStr of G2; theorem :: GROUP_2:65 G1 is Subgroup of G2 & G2 is Subgroup of G3 implies G1 is Subgroup of G3; theorem :: GROUP_2:66 the carrier of H1 c= the carrier of H2 implies H1 is Subgroup of H2; theorem :: GROUP_2:67 (for g st g in H1 holds g in H2) implies H1 is Subgroup of H2; theorem :: GROUP_2:68 the carrier of H1 = the carrier of H2 implies the HGrStr of H1 = the HGrStr of H2; theorem :: GROUP_2:69 (for g holds g in H1 iff g in H2) implies the HGrStr of H1 = the HGrStr of H2; definition let G; let H1,H2 be strict Subgroup of G; redefine pred H1 = H2 means :: GROUP_2:def 6 for g holds g in H1 iff g in H2; end; theorem :: GROUP_2:70 for G being strict Group, H being strict Subgroup of G holds the carrier of H = the carrier of G implies H = G; theorem :: GROUP_2:71 (for g being Element of G holds g in H) implies the HGrStr of H = the HGrStr of G; definition let G; func (1).G -> strict Subgroup of G means :: GROUP_2:def 7 the carrier of it = {1.G}; end; definition let G; func (Omega).G -> strict Subgroup of G equals :: GROUP_2:def 8 the HGrStr of G; end; canceled 3; theorem :: GROUP_2:75 (1).H = (1).G; theorem :: GROUP_2:76 (1).H1 = (1).H2; theorem :: GROUP_2:77 (1).G is Subgroup of H; theorem :: GROUP_2:78 for G being strict Group, H being Subgroup of G holds H is Subgroup of (Omega).G; theorem :: GROUP_2:79 for G being strict Group holds G is Subgroup of (Omega).G; theorem :: GROUP_2:80 (1).G is finite; definition let X be non empty set; cluster finite non empty Subset of X; end; theorem :: GROUP_2:81 ord (1).G = 1; theorem :: GROUP_2:82 for H being strict Subgroup of G holds H is finite & ord H = 1 implies H = (1).G; theorem :: GROUP_2:83 Ord H <=` Ord G; theorem :: GROUP_2:84 G is finite implies ord H <= ord G; theorem :: GROUP_2:85 for G being strict Group, H being strict Subgroup of G holds G is finite & ord G = ord H implies H = G; definition let G,H; func carr(H) -> Subset of G equals :: GROUP_2:def 9 the carrier of H; end; canceled; theorem :: GROUP_2:87 carr(H) <> {}; theorem :: GROUP_2:88 x in carr(H) iff x in H; theorem :: GROUP_2:89 g1 in carr(H) & g2 in carr(H) implies g1 * g2 in carr(H); theorem :: GROUP_2:90 g in carr(H) implies g" in carr(H); theorem :: GROUP_2:91 carr(H) * carr(H) = carr(H); theorem :: GROUP_2:92 carr(H)" = carr H; theorem :: GROUP_2:93 (carr H1 * carr H2 = carr H2 * carr H1 implies ex H being strict Subgroup of G st the carrier of H = carr H1 * carr H2) & ((ex H st the carrier of H = carr H1 * carr H2) implies carr H1 * carr H2 = carr H2 * carr H1); theorem :: GROUP_2:94 G is commutative Group implies ex H being strict Subgroup of G st the carrier of H = carr(H1) * carr(H2); definition let G,H1,H2; func H1 /\ H2 -> strict Subgroup of G means :: GROUP_2:def 10 the carrier of it = carr(H1) /\ carr(H2); end; canceled 2; theorem :: GROUP_2:97 (for H being Subgroup of G st H = H1 /\ H2 holds the carrier of H = (the carrier of H1) /\ (the carrier of H2)) & for H being strict Subgroup of G holds the carrier of H = (the carrier of H1) /\ (the carrier of H2) implies H = H1 /\ H2; theorem :: GROUP_2:98 carr(H1 /\ H2) = carr(H1) /\ carr(H2); theorem :: GROUP_2:99 x in H1 /\ H2 iff x in H1 & x in H2; theorem :: GROUP_2:100 for H being strict Subgroup of G holds H /\ H = H; theorem :: GROUP_2:101 H1 /\ H2 = H2 /\ H1; definition let G,H1,H2; redefine func H1 /\ H2; commutativity; end; theorem :: GROUP_2:102 H1 /\ H2 /\ H3 = H1 /\ (H2 /\ H3); theorem :: GROUP_2:103 (1).G /\ H = (1).G & H /\ (1).G = (1).G; theorem :: GROUP_2:104 for G being strict Group, H being strict Subgroup of G holds H /\ (Omega).G = H & (Omega).G /\ H = H; theorem :: GROUP_2:105 for G being strict Group holds (Omega).G /\ (Omega).G = G; theorem :: GROUP_2:106 H1 /\ H2 is Subgroup of H1 & H1 /\ H2 is Subgroup of H2; theorem :: GROUP_2:107 for H1 being strict Subgroup of G holds H1 is Subgroup of H2 iff H1 /\ H2 = H1; theorem :: GROUP_2:108 H1 is Subgroup of H2 implies H1 /\ H3 is Subgroup of H2; theorem :: GROUP_2:109 H1 is Subgroup of H2 & H1 is Subgroup of H3 implies H1 is Subgroup of H2 /\ H3; theorem :: GROUP_2:110 H1 is Subgroup of H2 implies H1 /\ H3 is Subgroup of H2 /\ H3; theorem :: GROUP_2:111 H1 is finite or H2 is finite implies H1 /\ H2 is finite; definition let G,H,A; func A * H -> Subset of G equals :: GROUP_2:def 11 A * carr H; func H * A -> Subset of G equals :: GROUP_2:def 12 carr H * A; end; canceled 2; theorem :: GROUP_2:114 x in A * H iff ex g1,g2 st x = g1 * g2 & g1 in A & g2 in H; theorem :: GROUP_2:115 x in H * A iff ex g1,g2 st x = g1 * g2 & g1 in H & g2 in A; theorem :: GROUP_2:116 A * B * H = A * (B * H); theorem :: GROUP_2:117 A * H * B = A * (H * B); theorem :: GROUP_2:118 H * A * B = H * (A * B); theorem :: GROUP_2:119 A * H1 * H2 = A * (H1 * carr H2); theorem :: GROUP_2:120 H1 * A * H2 = H1 * (A * H2); theorem :: GROUP_2:121 H1 * carr(H2) * A = H1 * (H2 * A); theorem :: GROUP_2:122 G is commutative Group implies A * H = H * A; definition let G,H,a; func a * H -> Subset of G equals :: GROUP_2:def 13 a * carr(H); func H * a -> Subset of G equals :: GROUP_2:def 14 carr(H) * a; end; canceled 2; theorem :: GROUP_2:125 x in a * H iff ex g st x = a * g & g in H; theorem :: GROUP_2:126 x in H * a iff ex g st x = g * a & g in H; theorem :: GROUP_2:127 a * b * H = a * (b * H); theorem :: GROUP_2:128 a * H * b = a * (H * b); theorem :: GROUP_2:129 H * a * b = H * (a * b); theorem :: GROUP_2:130 a in a * H & a in H * a; canceled; theorem :: GROUP_2:132 1.G * H = carr(H) & H * 1.G = carr(H); theorem :: GROUP_2:133 (1).G * a = {a} & a * (1).G = {a}; theorem :: GROUP_2:134 a * (Omega).G = the carrier of G & (Omega).G * a = the carrier of G; theorem :: GROUP_2:135 G is commutative Group implies a * H = H * a; theorem :: GROUP_2:136 a in H iff a * H = carr(H); theorem :: GROUP_2:137 a * H = b * H iff b" * a in H; theorem :: GROUP_2:138 a * H = b * H iff a * H meets b * H; theorem :: GROUP_2:139 a * b * H c= (a * H) * (b * H); theorem :: GROUP_2:140 carr(H) c= (a * H) * (a" * H) & carr(H) c= (a" * H) * (a * H); theorem :: GROUP_2:141 a |^ 2 * H c= (a * H) * (a * H); theorem :: GROUP_2:142 a in H iff H * a = carr(H); theorem :: GROUP_2:143 H * a = H * b iff b * a" in H; theorem :: GROUP_2:144 H * a = H * b iff H * a meets H * b; theorem :: GROUP_2:145 H * a * b c= (H * a) * (H * b); theorem :: GROUP_2:146 carr(H) c= (H * a) * (H * a") & carr(H) c= (H * a") * (H * a); theorem :: GROUP_2:147 H * (a |^ 2) c= (H * a) * (H * a); theorem :: GROUP_2:148 a * (H1 /\ H2) = (a * H1) /\ (a * H2); theorem :: GROUP_2:149 (H1 /\ H2) * a = (H1 * a) /\ (H2 * a); theorem :: GROUP_2:150 ex H1 being strict Subgroup of G st the carrier of H1 = a * H2 * a"; theorem :: GROUP_2:151 a * H,b * H are_equipotent; theorem :: GROUP_2:152 a * H,H * b are_equipotent; theorem :: GROUP_2:153 H * a,H * b are_equipotent; theorem :: GROUP_2:154 carr(H),a * H are_equipotent & carr(H),H * a are_equipotent; theorem :: GROUP_2:155 Ord(H) = Card(a * H) & Ord(H) = Card(H * a); theorem :: GROUP_2:156 H is finite implies ex B,C being finite set st B = a * H & C = H * a & ord H = card B & ord H = card C; scheme SubFamComp{A() -> set, F1() -> Subset-Family of A(), F2() -> Subset-Family of A(), P[set]}: F1() = F2() provided for X being Subset of A() holds X in F1() iff P[X] and for X being Subset of A() holds X in F2() iff P[X]; definition let G,H; func Left_Cosets H -> Subset-Family of G means :: GROUP_2:def 15 A in it iff ex a st A = a * H; func Right_Cosets H -> Subset-Family of G means :: GROUP_2:def 16 A in it iff ex a st A = H * a; end; canceled 7; theorem :: GROUP_2:164 G is finite implies Right_Cosets H is finite & Left_Cosets H is finite; theorem :: GROUP_2:165 carr H in Left_Cosets H & carr H in Right_Cosets H; theorem :: GROUP_2:166 Left_Cosets H, Right_Cosets H are_equipotent; theorem :: GROUP_2:167 union Left_Cosets H = the carrier of G & union Right_Cosets H = the carrier of G; theorem :: GROUP_2:168 Left_Cosets (1).G = {{a} : not contradiction}; theorem :: GROUP_2:169 Right_Cosets (1).G = {{a} : not contradiction}; theorem :: GROUP_2:170 for H being strict Subgroup of G holds Left_Cosets H = {{a} : not contradiction} implies H = (1).G; theorem :: GROUP_2:171 for H being strict Subgroup of G holds Right_Cosets H = {{a} : not contradiction} implies H = (1).G; theorem :: GROUP_2:172 Left_Cosets (Omega).G = {the carrier of G} & Right_Cosets (Omega).G = {the carrier of G}; theorem :: GROUP_2:173 for G being strict Group, H being strict Subgroup of G holds Left_Cosets H = {the carrier of G} implies H = G; theorem :: GROUP_2:174 for G being strict Group, H being strict Subgroup of G holds Right_Cosets H = {the carrier of G} implies H = G; definition let G,H; func Index H -> Cardinal equals :: GROUP_2:def 17 Card Left_Cosets H; end; theorem :: GROUP_2:175 Index H = Card Left_Cosets H & Index H = Card Right_Cosets H; definition let G,H; assume Left_Cosets(H) is finite; func index H -> Nat means :: GROUP_2:def 18 ex B being finite set st B = Left_Cosets H & it = card B; end; theorem :: GROUP_2:176 Left_Cosets H is finite implies (ex B being finite set st B = Left_Cosets H & index H = card B) & ex C being finite set st C = Right_Cosets H & index H = card C; definition let D be non empty set; let d be Element of D; redefine func {d} -> Element of Fin D; end; :: Lagrange Theorem theorem :: GROUP_2:177 G is finite implies ord G = ord H * index H; theorem :: GROUP_2:178 G is finite implies ord H divides ord G; reserve J for Subgroup of H; theorem :: GROUP_2:179 G is finite & I = J implies index I = index J * index H; theorem :: GROUP_2:180 index (Omega).G = 1; theorem :: GROUP_2:181 for G being strict Group, H being strict Subgroup of G holds Left_Cosets H is finite & index H = 1 implies H = G; theorem :: GROUP_2:182 Index (1).G = Ord G; theorem :: GROUP_2:183 G is finite implies index (1).G = ord G; theorem :: GROUP_2:184 for H being strict Subgroup of G holds G is finite & index H = ord G implies H = (1).G; theorem :: GROUP_2:185 for H being strict Subgroup of G holds Left_Cosets H is finite & Index H = Ord G implies G is finite & H = (1).G; :: :: Auxiliary theorems. :: theorem :: GROUP_2:186 for X being finite set st (for Y st Y in X ex B being finite set st B = Y & card B = k & for Z st Z in X & Y <> Z holds Y,Z are_equipotent & Y misses Z) ex C being finite set st C = union X & card C = k * card X;

Back to top