:: Subgroup and Cosets of Subgroups. Lagrange theorem :: by Wojciech A. Trybulec :: :: Received July 23, 1990 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, STRUCT_0, SUBSET_1, FINSET_1, NAT_1, GROUP_1, RELAT_1, TARSKI, ALGSTR_0, BINOP_1, REALSET1, ZFMISC_1, FUNCT_1, RLSUB_1, CARD_1, XXREAL_0, NEWTON, SETFAM_1, CQC_SIM1, FINSUB_1, SETWISEO, ARYTM_3, GROUP_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, FINSUB_1, FINSET_1, REALSET1, XCMPLX_0, XXREAL_0, CARD_1, ORDINAL1, NUMBERS, STRUCT_0, ALGSTR_0, GROUP_1, WELLORD2, BINOP_1, SETWISEO, DOMAIN_1, RELAT_1, FUNCT_1, RELSET_1, NAT_1, NAT_D, MCART_1; constructors SETFAM_1, PARTFUN1, WELLORD2, BINOP_1, SETWISEO, XXREAL_0, NAT_1, NAT_D, MEMBERED, REALSET1, GROUP_1, RELSET_1; registrations SUBSET_1, RELSET_1, FINSET_1, FINSUB_1, MEMBERED, REALSET1, STRUCT_0, GROUP_1, ALGSTR_0, CARD_1, ORDINAL1, XCMPLX_0; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve x for object; reserve G for non empty 1-sorted; reserve A for Subset of G; theorem :: GROUP_2:1 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}; involutiveness; end; theorem :: GROUP_2:2 x in A" iff ex g st x = g" & g in A; theorem :: GROUP_2:3 {g}" = {g"}; theorem :: GROUP_2:4 {g,h}" = {g",h"}; theorem :: GROUP_2:5 ({}(the carrier of G))" = {}; theorem :: GROUP_2:6 ([#](the carrier of G))" = the carrier of G; theorem :: GROUP_2:7 A <> {} iff A" <> {}; registration let G; let A be empty Subset of G; cluster A" -> empty; end; registration let G; let A be non empty Subset of G; cluster A" -> non empty; end; reserve G for non empty multMagma, 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; definition let G be commutative non empty multMagma; let A,B be Subset of G; redefine func A * B; commutativity; end; theorem :: GROUP_2:8 x in A * B iff ex g,h st x = g * h & g in A & h in B; theorem :: GROUP_2:9 A <> {} & B <> {} iff A * B <> {}; theorem :: GROUP_2:10 G is associative implies A * B * C = A * (B * C); theorem :: GROUP_2:11 for G being Group, A,B being Subset of G holds (A * B)" = B" * A"; theorem :: GROUP_2:12 A * (B \/ C) = A * B \/ A * C; theorem :: GROUP_2:13 (A \/ B) * C = A * C \/ B * C; theorem :: GROUP_2:14 A * (B /\ C) c= (A * B) /\ (A * C); theorem :: GROUP_2:15 (A /\ B) * C c= (A * C) /\ (B * C); theorem :: GROUP_2:16 {}(the carrier of G) * A = {} & A * {}(the carrier of G) = {}; theorem :: GROUP_2:17 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:18 {g} * {h} = {g * h}; theorem :: GROUP_2:19 {g} * {g1,g2} = {g * g1,g * g2}; theorem :: GROUP_2:20 {g1,g2} * {g} = {g1 * g,g2 * g}; theorem :: GROUP_2:21 {g,h} * {g1,g2} = {g * g1, g * g2, h * g1, h * g2}; theorem :: GROUP_2:22 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:23 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:24 (for a,b st a in A & b in B holds a * b = b * a) implies A * B = B * A; theorem :: GROUP_2:25 G is commutative Group implies A * B = B * A; theorem :: GROUP_2:26 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; theorem :: GROUP_2:27 x in g * A iff ex h st x = g * h & h in A; theorem :: GROUP_2:28 x in A * g iff ex h st x = h * g & h in A; theorem :: GROUP_2:29 G is associative implies g * A * B = g * (A * B); theorem :: GROUP_2:30 G is associative implies A * g * B = A * (g * B); theorem :: GROUP_2:31 G is associative implies A * B * g = A * (B * g); theorem :: GROUP_2:32 G is associative implies g * h * A = g * (h * A); theorem :: GROUP_2:33 G is associative implies g * A * h = g * (A * h); theorem :: GROUP_2:34 G is associative implies A * g * h = A * (g * h); theorem :: GROUP_2:35 {}(the carrier of G) * a = {} & a * {}(the carrier of G) = {}; reserve G for Group-like non empty multMagma; reserve h,g,g1,g2 for Element of G; reserve A for Subset of G; theorem :: GROUP_2:36 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:37 1_G * A = A & A * 1_G = A; theorem :: GROUP_2:38 G is commutative Group implies g * A = A * g; definition let G be Group-like non empty multMagma; mode Subgroup of G -> Group-like non empty multMagma means :: GROUP_2:def 5 the carrier of it c= the carrier of G & the multF of it = (the multF of G)||the carrier of it; end; reserve H for Subgroup of G; reserve h,h1,h2 for Element of H; theorem :: GROUP_2:39 G is finite implies H is finite; theorem :: GROUP_2:40 x in H implies x in G; theorem :: GROUP_2:41 h in G; theorem :: GROUP_2:42 h is Element of G; theorem :: GROUP_2:43 h1 = g1 & h2 = g2 implies h1 * h2 = g1 * g2; registration let G be Group; cluster -> associative for 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 H,H1,H2,H3 for Subgroup of G; reserve h,h1,h2 for Element of H; theorem :: GROUP_2:44 1_H = 1_G; theorem :: GROUP_2:45 1_H1 = 1_H2; theorem :: GROUP_2:46 1_G in H; theorem :: GROUP_2:47 1_H1 in H2; theorem :: GROUP_2:48 h = g implies h" = g"; theorem :: GROUP_2:49 inverse_op(H) = inverse_op(G) | the carrier of H; theorem :: GROUP_2:50 g1 in H & g2 in H implies g1 * g2 in H; theorem :: GROUP_2:51 g in H implies g" in H; registration let G; cluster strict for Subgroup of G; end; theorem :: GROUP_2:52 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:53 G is commutative Group implies H is commutative; registration let G be commutative Group; cluster -> commutative for Subgroup of G; end; theorem :: GROUP_2:54 G is Subgroup of G; theorem :: GROUP_2:55 G1 is Subgroup of G2 & G2 is Subgroup of G1 implies the multMagma of G1 = the multMagma of G2; theorem :: GROUP_2:56 G1 is Subgroup of G2 & G2 is Subgroup of G3 implies G1 is Subgroup of G3; theorem :: GROUP_2:57 the carrier of H1 c= the carrier of H2 implies H1 is Subgroup of H2; theorem :: GROUP_2:58 (for g st g in H1 holds g in H2) implies H1 is Subgroup of H2; theorem :: GROUP_2:59 the carrier of H1 = the carrier of H2 implies the multMagma of H1 = the multMagma of H2; theorem :: GROUP_2:60 (for g holds g in H1 iff g in H2) implies the multMagma of H1 = the multMagma 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:61 for G being Group, H being Subgroup of G st the carrier of G c= the carrier of H holds the multMagma of H = the multMagma of G; theorem :: GROUP_2:62 (for g being Element of G holds g in H) implies the multMagma of H = the multMagma 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 multMagma of G; projectivity; end; theorem :: GROUP_2:63 (1).H = (1).G; theorem :: GROUP_2:64 (1).H1 = (1).H2; theorem :: GROUP_2:65 (1).G is Subgroup of H; theorem :: GROUP_2:66 for G being strict Group, H being Subgroup of G holds H is Subgroup of (Omega).G; theorem :: GROUP_2:67 for G being strict Group holds G is Subgroup of (Omega).G; theorem :: GROUP_2:68 (1).G is finite; registration let G; cluster (1).G -> finite; cluster strict finite for Subgroup of G; end; registration cluster strict finite for Group; end; registration let G be finite Group; cluster -> finite for Subgroup of G; end; theorem :: GROUP_2:69 card (1).G = 1; theorem :: GROUP_2:70 for H being strict finite Subgroup of G holds card H = 1 implies H = (1).G; theorem :: GROUP_2:71 card H c= card G; theorem :: GROUP_2:72 for G being finite Group, H being Subgroup of G holds card H <= card G; theorem :: GROUP_2:73 for G being finite Group, H being Subgroup of G holds card G = card H implies the multMagma of H = the multMagma of G; definition let G,H; func carr(H) -> Subset of G equals :: GROUP_2:def 9 the carrier of H; end; theorem :: GROUP_2:74 g1 in carr(H) & g2 in carr(H) implies g1 * g2 in carr(H); theorem :: GROUP_2:75 g in carr(H) implies g" in carr(H); theorem :: GROUP_2:76 carr(H) * carr(H) = carr(H); theorem :: GROUP_2:77 carr(H)" = carr H; theorem :: GROUP_2:78 (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:79 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; theorem :: GROUP_2:80 (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:81 carr(H1 /\ H2) = carr(H1) /\ carr(H2); theorem :: GROUP_2:82 x in H1 /\ H2 iff x in H1 & x in H2; theorem :: GROUP_2:83 for H being strict Subgroup of G holds H /\ H = H; definition let G,H1,H2; redefine func H1 /\ H2; commutativity; end; theorem :: GROUP_2:84 H1 /\ H2 /\ H3 = H1 /\ (H2 /\ H3); theorem :: GROUP_2:85 (1).G /\ H = (1).G & H /\ (1).G = (1).G; theorem :: GROUP_2:86 for G being strict Group, H being strict Subgroup of G holds H /\ (Omega).G = H & (Omega).G /\ H = H; theorem :: GROUP_2:87 for G being strict Group holds (Omega).G /\ (Omega).G = G; theorem :: GROUP_2:88 H1 /\ H2 is Subgroup of H1 & H1 /\ H2 is Subgroup of H2; theorem :: GROUP_2:89 for H1 being Subgroup of G holds H1 is Subgroup of H2 iff the multMagma of (H1 /\ H2) = the multMagma of H1; theorem :: GROUP_2:90 H1 is Subgroup of H2 implies H1 /\ H3 is Subgroup of H2; theorem :: GROUP_2:91 H1 is Subgroup of H2 & H1 is Subgroup of H3 implies H1 is Subgroup of H2 /\ H3; theorem :: GROUP_2:92 H1 is Subgroup of H2 implies H1 /\ H3 is Subgroup of H2 /\ H3; theorem :: GROUP_2:93 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; theorem :: GROUP_2:94 x in A * H iff ex g1,g2 st x = g1 * g2 & g1 in A & g2 in H; theorem :: GROUP_2:95 x in H * A iff ex g1,g2 st x = g1 * g2 & g1 in H & g2 in A; theorem :: GROUP_2:96 A * B * H = A * (B * H); theorem :: GROUP_2:97 A * H * B = A * (H * B); theorem :: GROUP_2:98 H * A * B = H * (A * B); theorem :: GROUP_2:99 A * H1 * H2 = A * (H1 * carr H2); theorem :: GROUP_2:100 H1 * A * H2 = H1 * (A * H2); theorem :: GROUP_2:101 H1 * carr(H2) * A = H1 * (H2 * A); theorem :: GROUP_2:102 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; theorem :: GROUP_2:103 x in a * H iff ex g st x = a * g & g in H; theorem :: GROUP_2:104 x in H * a iff ex g st x = g * a & g in H; theorem :: GROUP_2:105 a * b * H = a * (b * H); theorem :: GROUP_2:106 a * H * b = a * (H * b); theorem :: GROUP_2:107 H * a * b = H * (a * b); theorem :: GROUP_2:108 a in a * H & a in H * a; theorem :: GROUP_2:109 1_G * H = carr(H) & H * 1_G = carr(H); theorem :: GROUP_2:110 (1).G * a = {a} & a * (1).G = {a}; theorem :: GROUP_2:111 a * (Omega).G = the carrier of G & (Omega).G * a = the carrier of G; theorem :: GROUP_2:112 G is commutative Group implies a * H = H * a; theorem :: GROUP_2:113 a in H iff a * H = carr(H); theorem :: GROUP_2:114 a * H = b * H iff b" * a in H; theorem :: GROUP_2:115 a * H = b * H iff a * H meets b * H; theorem :: GROUP_2:116 a * b * H c= (a * H) * (b * H); theorem :: GROUP_2:117 carr(H) c= (a * H) * (a" * H) & carr(H) c= (a" * H) * (a * H); theorem :: GROUP_2:118 a |^ 2 * H c= (a * H) * (a * H); theorem :: GROUP_2:119 a in H iff H * a = carr(H); theorem :: GROUP_2:120 H * a = H * b iff b * a" in H; theorem :: GROUP_2:121 H * a = H * b iff H * a meets H * b; theorem :: GROUP_2:122 H * a * b c= (H * a) * (H * b); theorem :: GROUP_2:123 carr(H) c= (H * a) * (H * a") & carr(H) c= (H * a") * (H * a); theorem :: GROUP_2:124 H * (a |^ 2) c= (H * a) * (H * a); theorem :: GROUP_2:125 a * (H1 /\ H2) = (a * H1) /\ (a * H2); theorem :: GROUP_2:126 (H1 /\ H2) * a = (H1 * a) /\ (H2 * a); theorem :: GROUP_2:127 ex H1 being strict Subgroup of G st the carrier of H1 = a * H2 * a"; theorem :: GROUP_2:128 a * H,b * H are_equipotent; theorem :: GROUP_2:129 a * H,H * b are_equipotent; theorem :: GROUP_2:130 H * a,H * b are_equipotent; theorem :: GROUP_2:131 carr(H),a * H are_equipotent & carr(H),H * a are_equipotent; theorem :: GROUP_2:132 card(H) = card(a * H) & card(H) = card(H * a); theorem :: GROUP_2:133 for H being finite Subgroup of G ex B,C being finite set st B = a * H & C = H * a & card H = card B & card H = card C; 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; theorem :: GROUP_2:134 G is finite implies Right_Cosets H is finite & Left_Cosets H is finite; theorem :: GROUP_2:135 carr H in Left_Cosets H & carr H in Right_Cosets H; theorem :: GROUP_2:136 Left_Cosets H, Right_Cosets H are_equipotent; theorem :: GROUP_2:137 union Left_Cosets H = the carrier of G & union Right_Cosets H = the carrier of G; theorem :: GROUP_2:138 Left_Cosets (1).G = the set of all {a}; theorem :: GROUP_2:139 Right_Cosets (1).G = the set of all {a}; theorem :: GROUP_2:140 for H being strict Subgroup of G holds Left_Cosets H = the set of all {a} implies H = (1).G; theorem :: GROUP_2:141 for H being strict Subgroup of G holds Right_Cosets H = the set of all {a} implies H = (1).G; theorem :: GROUP_2:142 Left_Cosets (Omega).G = {the carrier of G} & Right_Cosets (Omega).G = {the carrier of G}; theorem :: GROUP_2:143 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:144 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:145 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 -> Element of NAT means :: GROUP_2:def 18 ex B being finite set st B = Left_Cosets H & it = card B; end; theorem :: GROUP_2:146 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; ::$N Lagrange Theorem for Groups theorem :: GROUP_2:147 for G being finite Group, H being Subgroup of G holds card G = card H * index H; theorem :: GROUP_2:148 for G being finite Group, H being Subgroup of G holds card H divides card G; theorem :: GROUP_2:149 for G being finite Group, I, H being Subgroup of G, J being Subgroup of H holds I = J implies index I = index J * index H; theorem :: GROUP_2:150 index (Omega).G = 1; theorem :: GROUP_2:151 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:152 Index (1).G = card G; theorem :: GROUP_2:153 for G being finite Group holds index (1).G = card G; theorem :: GROUP_2:154 for G being finite Group, H being strict Subgroup of G holds index H = card G implies H = (1).G; theorem :: GROUP_2:155 for H being strict Subgroup of G holds Left_Cosets H is finite & Index H = card G implies G is finite & H = (1).G; :: :: Auxiliary theorems. :: theorem :: GROUP_2:156 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;