:: Groups -- Additive Notation :: by Roland Coghetto :: :: Received April 30, 2015 :: Copyright (c) 2015-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, NAT_1, INT_1, XBOOLE_0, ALGSTR_0, SUBSET_1, BINOP_2, RELAT_1, REAL_1, ARYTM_3, CARD_1, ARYTM_1, BINOP_1, STRUCT_0, FUNCT_1, SETWISEO, FINSEQOP, ZFMISC_1, COMPLEX1, XXREAL_0, FINSET_1, TARSKI, RLVECT_1, SUPINF_2, GROUP_1, POLYNOM1, GROUP_1A, REALSET1, RLSUB_1, SETFAM_1, CQC_SIM1, GROUP_2, PRE_TOPC, GROUP_3, FUNCT_2, VALUED_1, ORDINAL2, CONNSP_2, TOPS_1, RCOMP_1, UNIALG_1, CARD_5, COMPTS_1, RLVECT_3, TOPGRP_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, RELAT_1, PARTFUN1, SETFAM_1, FINSUB_1, FINSET_1, REALSET1, WELLORD2, DOMAIN_1, NAT_D, MCART_1, XREAL_0, PRE_TOPC, TOPS_1, TOPS_2, FUNCT_1, RELSET_1, FUNCT_2, BINOP_2, BINOP_1, INT_1, NAT_1, INT_2, FINSEQOP, SETWISEO, STRUCT_0, ALGSTR_0, RLVECT_1, CONNSP_2, COMPTS_1, BORSUK_1, CANTOR_1, YELLOW_8, TOPGRP_1, IDEAL_1; constructors SETWISEO, NAT_1, NAT_D, BINOP_2, FINSEQOP, RLVECT_1, SETFAM_1, WELLORD2, MEMBERED, REALSET1, RELSET_1, INT_2, TOPS_1, TOPS_2, COMPTS_1, BORSUK_1, GRCAT_1, CANTOR_1, YELLOW_8, TOPGRP_1, IDEAL_1; registrations ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XREAL_0, NAT_1, INT_1, STRUCT_0, ALGSTR_0, CARD_1, SUBSET_1, REALSET1, XCMPLX_0, XBOOLE_0, FUNCT_1, FUNCT_2, PRE_TOPC, TOPS_1, COMPTS_1, BORSUK_1, TOPGRP_1; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin ::: A copy of GROUP_1 reserve m,n for Nat; reserve i,j for Integer; reserve S for non empty addMagma; reserve r,r1,r2,s,s1,s2,t,t1,t2 for Element of S; scheme :: GROUP_1A:sch 1 SeqEx2Dbis{X,Z() -> non empty set, P[set,set,set]}: ex f being Function of [:NAT,X():],Z() st for x being Nat, y being Element of X() holds P[x,y,f.(x,y)] provided for x being Nat, y being Element of X() ex z being Element of Z() st P[x,y,z]; definition let IT be addMagma; attr IT is add-unital means :: GROUP_1A:def 1 ex e being Element of IT st for h being Element of IT holds h + e = h & e + h = h; attr IT is addGroup-like means :: GROUP_1A:def 2 ex e being Element of IT st for h being Element of IT holds h + e = h & e + h = h & ex g being Element of IT st h + g = e & g + h = e; end; registration cluster addGroup-like -> add-unital for addMagma; end; registration cluster strict addGroup-like add-associative non empty for addMagma; end; definition mode addGroup is addGroup-like add-associative non empty addMagma; end; theorem :: GROUP_1A:1 ((for r,s,t holds (r + s) + t = r + (s + t)) & ex t st for s1 holds s1 + t = s1 & t + s1 = s1 & ex s2 st s1 + s2 = t & s2 + s1 = t) implies S is addGroup; theorem :: GROUP_1A:2 (for r,s,t holds r + s + t = r + (s + t)) & (for r,s holds (ex t st r + t = s) & (ex t st t + r = s)) implies S is add-associative addGroup-like; theorem :: GROUP_1A:3 addMagma (# REAL, addreal #) is add-associative addGroup-like; reserve G for addGroup-like non empty addMagma; reserve e,h for Element of G; definition let G be addMagma such that G is add-unital; func 0_G -> Element of G means :: GROUP_1A:def 3 for h being Element of G holds h + it = h & it + h = h; end; theorem :: GROUP_1A:4 (for h holds h + e = h & e + h = h) implies e = 0_G; reserve G for addGroup; reserve f,g,h for Element of G; definition let G,h; func -h -> Element of G means :: GROUP_1A:def 4 h + it = 0_G & it + h = 0_G; involutiveness; end; theorem :: GROUP_1A:5 h + g = 0_G & g + h = 0_G implies g = -h; theorem :: GROUP_1A:6 h + g = h + f or g + h = f + h implies g = f; theorem :: GROUP_1A:7 h + g = h or g + h = h implies g = 0_G; theorem :: GROUP_1A:8 -(0_G) = 0_G; theorem :: GROUP_1A:9 -h = -g implies h = g; theorem :: GROUP_1A:10 -h = 0_G implies h = 0_G; theorem :: GROUP_1A:11 h + g = 0_G implies h = -g & g = -h; theorem :: GROUP_1A:12 h + f = g iff f = -h + g; theorem :: GROUP_1A:13 f + h = g iff f = g + -h; theorem :: GROUP_1A:14 ex f st g + f = h; theorem :: GROUP_1A:15 ex f st f + g = h; theorem :: GROUP_1A:16 -(h + g) = -g + -h; theorem :: GROUP_1A:17 g + h = h + g iff -(g + h) = -g + -h; theorem :: GROUP_1A:18 g + h = h + g iff -g + -h = -h + -g; theorem :: GROUP_1A:19 g + h = h + g iff g + -h = -h + g; reserve u for UnOp of G; definition let G; func add_inverse(G) -> UnOp of G means :: GROUP_1A:def 5 it.h = -h; end; registration let G be add-associative non empty addMagma; cluster the addF of G -> associative; end; theorem :: GROUP_1A:20 for G being add-unital non empty addMagma holds 0_G is_a_unity_wrt the addF of G; theorem :: GROUP_1A:21 for G being add-unital non empty addMagma holds the_unity_wrt the addF of G = 0_G; registration let G be add-unital non empty addMagma; cluster the addF of G -> having_a_unity; end; theorem :: GROUP_1A:22 add_inverse(G) is_an_inverseOp_wrt the addF of G; registration let G; cluster the addF of G -> having_an_inverseOp; end; theorem :: GROUP_1A:23 the_inverseOp_wrt the addF of G = add_inverse(G); definition let G be non empty addMagma; func mult G -> Function of [:NAT,the carrier of G:], the carrier of G means :: GROUP_1A:def 6 for h being Element of G holds it.(0,h) = 0_G & for n being Nat holds it.(n + 1, h) = it.(n,h) + h; end; definition let G,i,h; func i * h -> Element of G equals :: GROUP_1A:def 7 mult(G).(|.i.|,h) if 0 <= i otherwise -(mult(G).(|.i.|,h)); end; definition let G,n,h; redefine func n * h equals :: GROUP_1A:def 8 mult(G).(n,h); end; theorem :: GROUP_1A:24 0 * h = 0_G; theorem :: GROUP_1A:25 1 * h = h; theorem :: GROUP_1A:26 2 * h = h + h; theorem :: GROUP_1A:27 3 * h = h + h + h; theorem :: GROUP_1A:28 2 * h = 0_G iff -h = h; theorem :: GROUP_1A:29 i <= 0 implies i * h = -( |.i.| * h); theorem :: GROUP_1A:30 i * (0_G) = 0_G; theorem :: GROUP_1A:31 (-1) * h = -h; theorem :: GROUP_1A:32 (i + j) * h = (i * h) + (j * h); theorem :: GROUP_1A:33 (i + 1) * h = i * h + h & (i + 1) * h = h + ( i * h); theorem :: GROUP_1A:34 -i * h = -(i * h); theorem :: GROUP_1A:35 g + h = h + g implies i * (g + h) = i * g + ( i *h); theorem :: GROUP_1A:36 g + h = h + g implies i * g + ( j * h) = j * h + ( i * g); theorem :: GROUP_1A:37 g + h = h + g implies g + ( i * h) = i * h + g; definition let G,h; attr h is being_of_order_0 means :: GROUP_1A:def 9 n * h = 0_G implies n = 0; end; registration let G; cluster 0_G -> non being_of_order_0; end; definition let G,h; func ord h -> Element of NAT means :: GROUP_1A:def 10 it = 0 if h is being_of_order_0 otherwise it * h = 0_G & it <> 0 & for m st m * h = 0_G & m <> 0 holds it <= m; end; theorem :: GROUP_1A:38 ord h * h = 0_G; theorem :: GROUP_1A:39 ord 0_G = 1; theorem :: GROUP_1A:40 ord h = 1 implies h = 0_G; registration cluster strict Abelian for addGroup; end; theorem :: GROUP_1A:41 addMagma (# REAL, addreal #) is Abelian addGroup; reserve A for Abelian addGroup; reserve a,b for Element of A; theorem :: GROUP_1A:42 -(a + b) = -a + -b; theorem :: GROUP_1A:43 i * (a + b) = i * a + (i * b); theorem :: GROUP_1A:44 addLoopStr (# the carrier of A, the addF of A, 0_A #) is Abelian add-associative right_zeroed right_complementable; theorem :: GROUP_1A:45 for L be add-unital non empty addMagma for x be Element of L holds (mult L).(1,x) = x; theorem :: GROUP_1A:46 for L be add-unital non empty addMagma for x be Element of L holds (mult L).(2,x) = x+x; theorem :: GROUP_1A:47 for L be add-associative Abelian add-unital non empty addMagma for x,y be Element of L for n be Nat holds (mult L).(n,x+y) = (mult L).(n,x) + (mult L).(n,y); definition let G,H be addMagma; let IT be Function of G,H; attr IT is zero-preserving means :: GROUP_1A:def 11 IT.0_G = 0_H; end; begin ::: GROUP_2B reserve x for object; reserve y,y1,y2,Y,Z for set; reserve k for Nat; reserve G for addGroup; 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_1A:def 12 {-g : g in A}; involutiveness; end; theorem :: GROUP_1A:48 x in -A iff ex g st x = -g & g in A; theorem :: GROUP_1A:49 -{g} = {-g}; theorem :: GROUP_1A:50 -{g,h} = {-g,-h}; theorem :: GROUP_1A:51 -({}(the carrier of G)) = {}; theorem :: GROUP_1A:52 -([#](the carrier of G)) = the carrier of G; theorem :: GROUP_1A:53 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 addMagma, A,B,C for Subset of G; reserve a,b,g,g1,g2,h,h1,h2 for Element of G; definition let G be Abelian non empty addMagma; let A,B be Subset of G; redefine func A + B; commutativity; end; theorem :: GROUP_1A:54 x in A + B iff ex g,h st x = g + h & g in A & h in B; theorem :: GROUP_1A:55 A <> {} & B <> {} iff A + B <> {}; theorem :: GROUP_1A:56 G is add-associative implies A + B + C = A + (B + C); theorem :: GROUP_1A:57 for G being addGroup, A,B being Subset of G holds -(A + B) = -B + -A; theorem :: GROUP_1A:58 A + (B \/ C) = (A + B) \/ (A + C); theorem :: GROUP_1A:59 (A \/ B) + C = (A + C) \/ (B + C); theorem :: GROUP_1A:60 A + (B /\ C) c= (A + B) /\ (A + C); theorem :: GROUP_1A:61 (A /\ B) + C c= (A + C) /\ (B + C); theorem :: GROUP_1A:62 {}(the carrier of G) + A = {} & A + {}(the carrier of G) = {}; theorem :: GROUP_1A:63 for G being addGroup, 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_1A:64 {g} + {h} = {g + h}; theorem :: GROUP_1A:65 {g} + {g1,g2} = {g + g1,g + g2}; theorem :: GROUP_1A:66 {g1,g2} + {g} = {g1 + g,g2 + g}; theorem :: GROUP_1A:67 {g,h} + {g1,g2} = {g + g1, g + g2, h + g1, h + g2}; theorem :: GROUP_1A:68 for G being addGroup, 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_1A:69 for G being addGroup, 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_1A:70 (for a,b st a in A & b in B holds a + b = b + a) implies A + B = B + A; theorem :: GROUP_1A:71 G is Abelian addGroup implies A + B = B + A; theorem :: GROUP_1A:72 for G being Abelian addGroup, A,B being Subset of G holds -(A + B) = -A + -B; definition let G,g,A; func g + A -> Subset of G equals :: GROUP_1A:def 13 {g} + A; func A + g -> Subset of G equals :: GROUP_1A:def 14 A + {g}; end; theorem :: GROUP_1A:73 x in g + A iff ex h st x = g + h & h in A; theorem :: GROUP_1A:74 x in A + g iff ex h st x = h + g & h in A; theorem :: GROUP_1A:75 G is add-associative implies g + A + B = g + (A + B); theorem :: GROUP_1A:76 G is add-associative implies A + g + B = A + (g + B); theorem :: GROUP_1A:77 G is add-associative implies A + B + g = A + (B + g); theorem :: GROUP_1A:78 G is add-associative implies g + h + A = g + (h + A); theorem :: GROUP_1A:79 G is add-associative implies g + A + h = g + (A + h); theorem :: GROUP_1A:80 G is add-associative implies A + g + h = A + (g + h); theorem :: GROUP_1A:81 {}(the carrier of G) + a = {} & a + {}(the carrier of G) = {}; reserve G for addGroup-like non empty addMagma; reserve h,g,g1,g2 for Element of G; reserve A for Subset of G; theorem :: GROUP_1A:82 for G being addGroup, 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_1A:83 0_G + A = A & A + 0_G = A; theorem :: GROUP_1A:84 G is Abelian addGroup implies g + A = A + g; definition let G be addGroup-like non empty addMagma; mode Subgroup of G -> addGroup-like non empty addMagma means :: GROUP_1A:def 15 the carrier of it c= the carrier of G & the addF of it = (the addF of G)||the carrier of it; end; reserve H for Subgroup of G; reserve h,h1,h2 for Element of H; theorem :: GROUP_1A:85 G is finite implies H is finite; theorem :: GROUP_1A:86 x in H implies x in G; theorem :: GROUP_1A:87 h in G; theorem :: GROUP_1A:88 h is Element of G; theorem :: GROUP_1A:89 h1 = g1 & h2 = g2 implies h1 + h2 = g1 + g2; registration let G be addGroup; cluster -> add-associative for Subgroup of G; end; reserve G,G1,G2,G3 for addGroup; 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_1A:90 0_H = 0_G; theorem :: GROUP_1A:91 0_H1 = 0_H2; theorem :: GROUP_1A:92 0_G in H; theorem :: GROUP_1A:93 0_H1 in H2; theorem :: GROUP_1A:94 h = g implies -h = -g; theorem :: GROUP_1A:95 add_inverse(H) = add_inverse(G) | the carrier of H; theorem :: GROUP_1A:96 g1 in H & g2 in H implies g1 + g2 in H; theorem :: GROUP_1A:97 g in H implies -g in H; registration let G; cluster strict for Subgroup of G; end; theorem :: GROUP_1A:98 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_1A:99 G is Abelian addGroup implies H is Abelian; registration let G be Abelian addGroup; cluster -> Abelian for Subgroup of G; end; theorem :: GROUP_1A:100 G is Subgroup of G; theorem :: GROUP_1A:101 G1 is Subgroup of G2 & G2 is Subgroup of G1 implies the addMagma of G1 = the addMagma of G2; theorem :: GROUP_1A:102 G1 is Subgroup of G2 & G2 is Subgroup of G3 implies G1 is Subgroup of G3; theorem :: GROUP_1A:103 the carrier of H1 c= the carrier of H2 implies H1 is Subgroup of H2; theorem :: GROUP_1A:104 (for g st g in H1 holds g in H2) implies H1 is Subgroup of H2; theorem :: GROUP_1A:105 the carrier of H1 = the carrier of H2 implies the addMagma of H1 = the addMagma of H2; theorem :: GROUP_1A:106 (for g holds g in H1 iff g in H2) implies the addMagma of H1 = the addMagma of H2; definition let G; let H1,H2 be strict Subgroup of G; redefine pred H1 = H2 means :: GROUP_1A:def 16 for g holds g in H1 iff g in H2; end; theorem :: GROUP_1A:107 for G being addGroup, H being Subgroup of G st the carrier of G c= the carrier of H holds the addMagma of H = the addMagma of G; theorem :: GROUP_1A:108 (for g being Element of G holds g in H) implies the addMagma of H = the addMagma of G; definition let G; func (0).G -> strict Subgroup of G means :: GROUP_1A:def 17 the carrier of it = {0_G}; end; definition let G; func (Omega).G -> strict Subgroup of G equals :: GROUP_1A:def 18 the addMagma of G; projectivity; end; theorem :: GROUP_1A:109 (0).H = (0).G; theorem :: GROUP_1A:110 (0).H1 = (0).H2; theorem :: GROUP_1A:111 (0).G is Subgroup of H; theorem :: GROUP_1A:112 for G being strict addGroup, H being Subgroup of G holds H is Subgroup of (Omega).G; theorem :: GROUP_1A:113 for G being strict addGroup holds G is Subgroup of (Omega).G; theorem :: GROUP_1A:114 (0).G is finite; registration let G; cluster (0).G -> finite; cluster strict finite for Subgroup of G; end; registration cluster strict finite for addGroup; end; registration let G be finite addGroup; cluster -> finite for Subgroup of G; end; theorem :: GROUP_1A:115 card (0).G = 1; theorem :: GROUP_1A:116 for H being strict finite Subgroup of G holds card H = 1 implies H = (0).G; theorem :: GROUP_1A:117 card H c= card G; theorem :: GROUP_1A:118 for G being finite addGroup, H being Subgroup of G holds card H <= card G; theorem :: GROUP_1A:119 for G being finite addGroup, H being Subgroup of G holds card G = card H implies the addMagma of H = the addMagma of G; definition let G,H; func carr(H) -> Subset of G equals :: GROUP_1A:def 19 the carrier of H; end; theorem :: GROUP_1A:120 g1 in carr(H) & g2 in carr(H) implies g1 + g2 in carr(H); theorem :: GROUP_1A:121 g in carr(H) implies -g in carr(H); theorem :: GROUP_1A:122 carr(H) + carr(H) = carr(H); theorem :: GROUP_1A:123 -carr(H) = carr H; theorem :: GROUP_1A:124 (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_1A:125 G is Abelian addGroup 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_1A:def 20 the carrier of it = carr (H1) /\ carr(H2); end; theorem :: GROUP_1A:126 (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_1A:127 carr(H1 /\ H2) = carr(H1) /\ carr(H2); theorem :: GROUP_1A:128 x in H1 /\ H2 iff x in H1 & x in H2; theorem :: GROUP_1A:129 for H being strict Subgroup of G holds H /\ H = H; definition let G,H1,H2; redefine func H1 /\ H2; commutativity; end; theorem :: GROUP_1A:130 H1 /\ H2 /\ H3 = H1 /\ (H2 /\ H3); theorem :: GROUP_1A:131 (0).G /\ H = (0).G & H /\ (0).G = (0).G; theorem :: GROUP_1A:132 for G being strict addGroup, H being strict Subgroup of G holds H /\ (Omega).G = H & (Omega).G /\ H = H; theorem :: GROUP_1A:133 for G being strict addGroup holds (Omega).G /\ (Omega).G = G; theorem :: GROUP_1A:134 H1 /\ H2 is Subgroup of H1 & H1 /\ H2 is Subgroup of H2; theorem :: GROUP_1A:135 for H1 being Subgroup of G holds H1 is Subgroup of H2 iff the addMagma of (H1 /\ H2) = the addMagma of H1; theorem :: GROUP_1A:136 H1 is Subgroup of H2 implies H1 /\ H3 is Subgroup of H2; theorem :: GROUP_1A:137 H1 is Subgroup of H2 & H1 is Subgroup of H3 implies H1 is Subgroup of H2 /\ H3; theorem :: GROUP_1A:138 H1 is Subgroup of H2 implies H1 /\ H3 is Subgroup of H2 /\ H3; theorem :: GROUP_1A:139 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_1A:def 21 A + carr H; func H + A -> Subset of G equals :: GROUP_1A:def 22 carr H + A; end; theorem :: GROUP_1A:140 x in A + H iff ex g1,g2 st x = g1 + g2 & g1 in A & g2 in H; theorem :: GROUP_1A:141 x in H + A iff ex g1,g2 st x = g1 + g2 & g1 in H & g2 in A; theorem :: GROUP_1A:142 A + B + H = A + (B + H); theorem :: GROUP_1A:143 A + H + B = A + (H + B); theorem :: GROUP_1A:144 H + A + B = H + (A + B); theorem :: GROUP_1A:145 A + H1 + H2 = A + (H1 + carr H2); theorem :: GROUP_1A:146 H1 + A + H2 = H1 + (A + H2); theorem :: GROUP_1A:147 H1 + carr(H2) + A = H1 + (H2 + A); theorem :: GROUP_1A:148 G is Abelian addGroup implies A + H = H + A; definition let G,H,a; func a + H -> Subset of G equals :: GROUP_1A:def 23 a + carr(H); func H + a -> Subset of G equals :: GROUP_1A:def 24 carr(H) + a; end; theorem :: GROUP_1A:149 x in a + H iff ex g st x = a + g & g in H; theorem :: GROUP_1A:150 x in H + a iff ex g st x = g + a & g in H; theorem :: GROUP_1A:151 a + b + H = a + (b + H); theorem :: GROUP_1A:152 a + H + b = a + (H + b); theorem :: GROUP_1A:153 H + a + b = H + (a + b); theorem :: GROUP_1A:154 a in a + H & a in H + a; theorem :: GROUP_1A:155 0_G + H = carr(H) & H + 0_G = carr(H); theorem :: GROUP_1A:156 (0).G + a = {a} & a + (0).G = {a}; theorem :: GROUP_1A:157 a + (Omega).G = the carrier of G & (Omega).G + a = the carrier of G; theorem :: GROUP_1A:158 G is Abelian addGroup implies a + H = H + a; theorem :: GROUP_1A:159 a in H iff a + H = carr(H); theorem :: GROUP_1A:160 a + H = b + H iff -b + a in H; theorem :: GROUP_1A:161 a + H = b + H iff a + H meets b + H; theorem :: GROUP_1A:162 a + b + H c= (a + H) + (b + H); theorem :: GROUP_1A:163 carr(H) c= (a + H) + (-a + H) & carr(H) c= (-a + H) + (a + H); theorem :: GROUP_1A:164 2 * a + H c= (a + H) + (a + H); theorem :: GROUP_1A:165 a in H iff H + a = carr(H); theorem :: GROUP_1A:166 H + a = H + b iff b + -a in H; theorem :: GROUP_1A:167 H + a = H + b iff H + a meets H + b; theorem :: GROUP_1A:168 H + a + b c= (H + a) + (H + b); theorem :: GROUP_1A:169 carr(H) c= (H + a) + (H + -a) & carr(H) c= (H + -a) + (H + a); theorem :: GROUP_1A:170 H + (2 * a) c= (H + a) + (H + a); theorem :: GROUP_1A:171 a + (H1 /\ H2) = (a + H1) /\ (a + H2); theorem :: GROUP_1A:172 (H1 /\ H2) + a = (H1 + a) /\ (H2 + a); theorem :: GROUP_1A:173 ex H1 being strict Subgroup of G st the carrier of H1 = a + H2 + -a; theorem :: GROUP_1A:174 a + H,b + H are_equipotent; theorem :: GROUP_1A:175 a + H,H + b are_equipotent; theorem :: GROUP_1A:176 H + a,H + b are_equipotent; theorem :: GROUP_1A:177 carr(H),a + H are_equipotent & carr(H),H + a are_equipotent; theorem :: GROUP_1A:178 card(H) = card(a + H) & card(H) = card(H + a); theorem :: GROUP_1A:179 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_1A:def 25 A in it iff ex a st A = a + H; func Right_Cosets H -> Subset-Family of G means :: GROUP_1A:def 26 A in it iff ex a st A = H + a; end; theorem :: GROUP_1A:180 G is finite implies Right_Cosets H is finite & Left_Cosets H is finite; theorem :: GROUP_1A:181 carr H in Left_Cosets H & carr H in Right_Cosets H; theorem :: GROUP_1A:182 Left_Cosets H, Right_Cosets H are_equipotent; theorem :: GROUP_1A:183 union Left_Cosets H = the carrier of G & union Right_Cosets H = the carrier of G; theorem :: GROUP_1A:184 Left_Cosets (0).G = the set of all {a}; theorem :: GROUP_1A:185 Right_Cosets (0).G = the set of all {a}; theorem :: GROUP_1A:186 for H being strict Subgroup of G holds Left_Cosets H = the set of all {a} implies H = (0).G; theorem :: GROUP_1A:187 for H being strict Subgroup of G holds Right_Cosets H = the set of all {a} implies H = (0).G; theorem :: GROUP_1A:188 Left_Cosets (Omega).G = {the carrier of G} & Right_Cosets (Omega).G = {the carrier of G}; theorem :: GROUP_1A:189 for G being strict addGroup, H being strict Subgroup of G holds Left_Cosets H = {the carrier of G} implies H = G; theorem :: GROUP_1A:190 for G being strict addGroup, 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_1A:def 27 card Left_Cosets H; end; theorem :: GROUP_1A:191 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_1A:def 28 ex B being finite set st B = Left_Cosets H & it = card B; end; theorem :: GROUP_1A:192 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 addGroups theorem :: GROUP_1A:193 for G being finite addGroup, H being Subgroup of G holds card G = card H * index H; theorem :: GROUP_1A:194 for G being finite addGroup, H being Subgroup of G holds card H divides card G; theorem :: GROUP_1A:195 for G being finite addGroup, I, H being Subgroup of G, J being Subgroup of H holds I = J implies index I = index J * index H; theorem :: GROUP_1A:196 index (Omega).G = 1; theorem :: GROUP_1A:197 for G being strict addGroup, H being strict Subgroup of G holds Left_Cosets H is finite & index H = 1 implies H = G; theorem :: GROUP_1A:198 Index (0).G = card G; theorem :: GROUP_1A:199 for G being finite addGroup holds index (0).G = card G; theorem :: GROUP_1A:200 for G being finite addGroup, H being strict Subgroup of G holds index H = card G implies H = (0).G; theorem :: GROUP_1A:201 for H being strict Subgroup of G holds Left_Cosets H is finite & Index H = card G implies G is finite & H = (0).G; begin ::: GROUP_3B reserve x,y,y1,y2 for set; reserve G for addGroup; reserve a,b,c,d,g,h for Element of G; reserve A,B,C,D for Subset of G; reserve H,H1,H2,H3 for Subgroup of G; reserve n for Nat; reserve i for Integer; theorem :: GROUP_1A:202 a + b + (-b) = a & a + (-b) + b = a & (-b) + b + a = a & b + (-b) + a = a & a + (b + (-b)) = a & a + ((-b) + b) = a & (-b) + (b + a) = a & b + ((-b) + a) = a; theorem :: GROUP_1A:203 G is Abelian addGroup iff the addF of G is commutative; theorem :: GROUP_1A:204 (0).G is Abelian; theorem :: GROUP_1A:205 A c= B & C c= D implies A + C c= B + D; theorem :: GROUP_1A:206 A c= B implies a + A c= a + B & A + a c= B + a; theorem :: GROUP_1A:207 H1 is Subgroup of H2 implies a + H1 c= a + H2 & H1 + a c= H2 + a; theorem :: GROUP_1A:208 a + H = {a} + H; theorem :: GROUP_1A:209 H + a = H + {a}; theorem :: GROUP_1A:210 A + a + H = A + (a + H); theorem :: GROUP_1A:211 a + H + A = a + (H + A); theorem :: GROUP_1A:212 A + H + a = A + (H + a); theorem :: GROUP_1A:213 H + a + A = H + (a + A); theorem :: GROUP_1A:214 H1 + a + H2 = H1 + (a + H2); definition let G; func Subgroups G -> set means :: GROUP_1A:def 29 for x being object holds x in it iff x is strict Subgroup of G; end; registration let G; cluster Subgroups G -> non empty; end; theorem :: GROUP_1A:215 for G being strict addGroup holds G in Subgroups G; theorem :: GROUP_1A:216 G is finite implies Subgroups G is finite; definition let G,a,b; func a * b -> Element of G equals :: GROUP_1A:def 30 (-b) + a + b; end; theorem :: GROUP_1A:217 a * g = b * g implies a = b; theorem :: GROUP_1A:218 (0_G) * a = 0_G; theorem :: GROUP_1A:219 a * b = 0_G implies a = 0_G; theorem :: GROUP_1A:220 a * 0_G = a; theorem :: GROUP_1A:221 a * a = a; theorem :: GROUP_1A:222 a * (-a) = a & (-a) * a = (-a); theorem :: GROUP_1A:223 a * b = a iff a + b = b + a; theorem :: GROUP_1A:224 (a + b) * g = a * g + (b * g); theorem :: GROUP_1A:225 a * g * h = a * (g + h); theorem :: GROUP_1A:226 a * b * (-b) = a & a * (-b) * b = a; theorem :: GROUP_1A:227 (-a) * b = -(a * b); theorem :: GROUP_1A:228 (n * a) * b = n * (a * b); theorem :: GROUP_1A:229 (i * a) * b = i * (a * b); theorem :: GROUP_1A:230 G is Abelian addGroup implies a * b = a; theorem :: GROUP_1A:231 (for a,b holds a * b = a) implies G is Abelian; definition let G,A,B; func A * B -> Subset of G equals :: GROUP_1A:def 31 {g * h : g in A & h in B}; end; theorem :: GROUP_1A:232 x in A * B iff ex g,h st x = g * h & g in A & h in B; theorem :: GROUP_1A:233 A * B <> {} iff A <> {} & B <> {}; theorem :: GROUP_1A:234 A * B c= (-B) + A + B; theorem :: GROUP_1A:235 (A + B) * C c= A * C + (B * C); theorem :: GROUP_1A:236 A * B * C = A * (B + C); theorem :: GROUP_1A:237 (-A) * B = -(A * B); theorem :: GROUP_1A:238 {a} * {b} = {a * b}; theorem :: GROUP_1A:239 {a} * {b,c} = {a * b,a * c}; theorem :: GROUP_1A:240 {a,b} * {c} = {a * c,b * c}; theorem :: GROUP_1A:241 {a,b} * {c,d} = {a * c,a * d,b * c,b * d}; definition let G,A,g; func A * g -> Subset of G equals :: GROUP_1A:def 32 A * {g}; func g * A -> Subset of G equals :: GROUP_1A:def 33 {g} * A; end; theorem :: GROUP_1A:242 x in A * g iff ex h st x = h * g & h in A; theorem :: GROUP_1A:243 x in g * A iff ex h st x = g * h & h in A; theorem :: GROUP_1A:244 g * A c= (-A) + g + A; theorem :: GROUP_1A:245 A * B * g = A * (B + g); theorem :: GROUP_1A:246 A * g * B = A * (g + B); theorem :: GROUP_1A:247 g * A * B = g * (A + B); theorem :: GROUP_1A:248 A * a * b = A * (a + b); theorem :: GROUP_1A:249 a * A * b = a * (A + b); theorem :: GROUP_1A:250 a * b * A = a * (b + A); theorem :: GROUP_1A:251 A * g = (-g) + A + g; theorem :: GROUP_1A:252 (A + B) * a c= (A * a) + (B * a); theorem :: GROUP_1A:253 A * 0_G = A; theorem :: GROUP_1A:254 A <> {} implies (0_G) * A = {0_G}; theorem :: GROUP_1A:255 A * a * (-a) = A & A * (-a) * a = A; theorem :: GROUP_1A:256 G is Abelian addGroup iff for A,B st B <> {} holds A * B = A; theorem :: GROUP_1A:257 G is Abelian addGroup iff for A,g holds A * g = A; theorem :: GROUP_1A:258 G is Abelian addGroup iff for A,g st A <> {} holds g * A = {g}; definition let G,H,a; func H * a -> strict Subgroup of G means :: GROUP_1A:def 34 the carrier of it = carr(H) * a; end; theorem :: GROUP_1A:259 x in H * a iff ex g st x = g * a & g in H; theorem :: GROUP_1A:260 the carrier of H * a = (-a) + H + a; theorem :: GROUP_1A:261 H * a * b = H * (a + b); theorem :: GROUP_1A:262 for H being strict Subgroup of G holds H * 0_G = H; theorem :: GROUP_1A:263 for H being strict Subgroup of G holds H * a * (-a) = H & H * (-a) * a = H; theorem :: GROUP_1A:264 (H1 /\ H2) * a = (H1 * a) /\ (H2 * a); theorem :: GROUP_1A:265 card H = card(H * a); theorem :: GROUP_1A:266 H is finite iff H * a is finite; registration let G,a; let H be finite Subgroup of G; cluster H * a -> finite; end; theorem :: GROUP_1A:267 for H being finite Subgroup of G holds card H = card(H * a); theorem :: GROUP_1A:268 (0).G * a = (0).G; theorem :: GROUP_1A:269 for H being strict Subgroup of G holds H * a = (0).G implies H = (0).G; theorem :: GROUP_1A:270 for G being addGroup, a being Element of G holds (Omega).G * a = (Omega).G; theorem :: GROUP_1A:271 for H being strict Subgroup of G holds H * a = G implies H = G; theorem :: GROUP_1A:272 Index H = Index(H * a); theorem :: GROUP_1A:273 Left_Cosets H is finite implies index H = index(H * a); theorem :: GROUP_1A:274 G is Abelian addGroup implies for H being strict Subgroup of G for a holds H * a = H; definition let G,a,b; pred a,b are_conjugated means :: GROUP_1A:def 35 ex g st a = b * g; end; notation let G,a,b; antonym a,b are_not_conjugated for a,b are_conjugated; end; theorem :: GROUP_1A:275 a,b are_conjugated iff ex g st b = a * g; definition let G,a,b; redefine pred a,b are_conjugated; reflexivity; symmetry; end; theorem :: GROUP_1A:276 a,b are_conjugated & b,c are_conjugated implies a,c are_conjugated; theorem :: GROUP_1A:277 a,0_G are_conjugated or 0_G,a are_conjugated implies a = 0_G; theorem :: GROUP_1A:278 a * carr (Omega).G = {b : a,b are_conjugated}; definition let G,a; func con_class a -> Subset of G equals :: GROUP_1A:def 36 a * carr (Omega).G; end; theorem :: GROUP_1A:279 x in con_class a iff ex b st b = x & a,b are_conjugated; theorem :: GROUP_1A:280 a in con_class b iff a,b are_conjugated; theorem :: GROUP_1A:281 a * g in con_class a; theorem :: GROUP_1A:282 a in con_class a; theorem :: GROUP_1A:283 a in con_class b implies b in con_class a; theorem :: GROUP_1A:284 con_class a = con_class b iff con_class a meets con_class b; theorem :: GROUP_1A:285 con_class a = {0_G} iff a = 0_G; theorem :: GROUP_1A:286 con_class a + A = A + con_class a; definition let G,A,B; pred A,B are_conjugated means :: GROUP_1A:def 37 ex g st A = B * g; end; notation let G,A,B; antonym A,B are_not_conjugated for A,B are_conjugated; end; theorem :: GROUP_1A:287 A,B are_conjugated iff ex g st B = A * g; theorem :: GROUP_1A:288 A,A are_conjugated; theorem :: GROUP_1A:289 A,B are_conjugated implies B,A are_conjugated; definition let G,A,B; redefine pred A,B are_conjugated; reflexivity; symmetry; end; theorem :: GROUP_1A:290 A,B are_conjugated & B,C are_conjugated implies A,C are_conjugated; theorem :: GROUP_1A:291 {a},{b} are_conjugated iff a,b are_conjugated; theorem :: GROUP_1A:292 A,carr H1 are_conjugated implies ex H2 being strict Subgroup of G st the carrier of H2 = A; definition let G,A; func con_class A -> Subset-Family of G equals :: GROUP_1A:def 38 {B : A,B are_conjugated}; end; theorem :: GROUP_1A:293 x in con_class A iff ex B st x = B & A,B are_conjugated; theorem :: GROUP_1A:294 A in con_class B iff A,B are_conjugated; theorem :: GROUP_1A:295 A * g in con_class A; theorem :: GROUP_1A:296 A in con_class A; theorem :: GROUP_1A:297 A in con_class B implies B in con_class A; theorem :: GROUP_1A:298 con_class A = con_class B iff con_class A meets con_class B; theorem :: GROUP_1A:299 con_class{a} = {{b} : b in con_class a}; theorem :: GROUP_1A:300 G is finite implies con_class A is finite; definition let G,H1,H2; pred H1,H2 are_conjugated means :: GROUP_1A:def 39 ex g st the addMagma of H1 = H2 * g; end; notation let G,H1,H2; antonym H1,H2 are_not_conjugated for H1,H2 are_conjugated; end; theorem :: GROUP_1A:301 for H1,H2 being strict Subgroup of G holds H1,H2 are_conjugated iff ex g st H2 = H1 * g; theorem :: GROUP_1A:302 for H1 being strict Subgroup of G holds H1,H1 are_conjugated; theorem :: GROUP_1A:303 for H1,H2 being strict Subgroup of G holds H1,H2 are_conjugated implies H2,H1 are_conjugated; definition let G; let H1,H2 be strict Subgroup of G; redefine pred H1,H2 are_conjugated; reflexivity; symmetry; end; theorem :: GROUP_1A:304 for H1,H2 being strict Subgroup of G holds H1,H2 are_conjugated & H2,H3 are_conjugated implies H1,H3 are_conjugated; reserve L for Subset of Subgroups G; definition let G,H; func con_class H -> Subset of Subgroups G means :: GROUP_1A:def 40 for x being object holds x in it iff ex H1 being strict Subgroup of G st x = H1 & H,H1 are_conjugated; end; theorem :: GROUP_1A:305 x in con_class H implies x is strict Subgroup of G; theorem :: GROUP_1A:306 for H1,H2 being strict Subgroup of G holds H1 in con_class H2 iff H1,H2 are_conjugated; theorem :: GROUP_1A:307 for H being strict Subgroup of G holds H * g in con_class H; theorem :: GROUP_1A:308 for H being strict Subgroup of G holds H in con_class H; theorem :: GROUP_1A:309 for H1,H2 being strict Subgroup of G holds H1 in con_class H2 implies H2 in con_class H1; theorem :: GROUP_1A:310 for H1,H2 being strict Subgroup of G holds con_class H1 = con_class H2 iff con_class H1 meets con_class H2; theorem :: GROUP_1A:311 G is finite implies con_class H is finite; theorem :: GROUP_1A:312 for H1 being strict Subgroup of G holds H1,H2 are_conjugated iff carr H1,carr H2 are_conjugated; definition let G; let IT be Subgroup of G; attr IT is normal means :: GROUP_1A:def 41 for a holds IT * a = the addMagma of IT; end; registration let G; cluster strict normal for Subgroup of G; end; reserve N2 for normal Subgroup of G; theorem :: GROUP_1A:313 (0).G is normal & (Omega).G is normal; theorem :: GROUP_1A:314 for N1,N2 being strict normal Subgroup of G holds N1 /\ N2 is normal; theorem :: GROUP_1A:315 for H being strict Subgroup of G holds G is Abelian addGroup implies H is normal; theorem :: GROUP_1A:316 H is normal Subgroup of G iff for a holds a + H = H + a; theorem :: GROUP_1A:317 for H being Subgroup of G holds H is normal Subgroup of G iff for a holds a + H c= H + a; theorem :: GROUP_1A:318 for H being Subgroup of G holds H is normal Subgroup of G iff for a holds H + a c= a + H; theorem :: GROUP_1A:319 for H being Subgroup of G holds H is normal Subgroup of G iff for A holds A + H = H + A; theorem :: GROUP_1A:320 for H being strict Subgroup of G holds H is normal Subgroup of G iff for a holds H is Subgroup of H * a; theorem :: GROUP_1A:321 for H being strict Subgroup of G holds H is normal Subgroup of G iff for a holds H * a is Subgroup of H; theorem :: GROUP_1A:322 for H being strict Subgroup of G holds H is normal Subgroup of G iff con_class H = {H}; theorem :: GROUP_1A:323 for H being strict Subgroup of G holds H is normal Subgroup of G iff for a st a in H holds con_class a c= carr H; theorem :: GROUP_1A:324 for N1,N2 being strict normal Subgroup of G holds carr N1 + carr N2 = carr N2 + carr N1; theorem :: GROUP_1A:325 for N1,N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st the carrier of N = carr N1 + carr N2; theorem :: GROUP_1A:326 for N being normal Subgroup of G holds Left_Cosets N = Right_Cosets N; theorem :: GROUP_1A:327 for H being Subgroup of G holds Left_Cosets H is finite & index H = 2 implies H is normal Subgroup of G; definition let G, A; func Normalizer A -> strict Subgroup of G means :: GROUP_1A:def 42 the carrier of it = {h : A * h = A}; end; theorem :: GROUP_1A:328 x in Normalizer A iff ex h st x = h & A * h = A; theorem :: GROUP_1A:329 card con_class A = Index Normalizer A; theorem :: GROUP_1A:330 con_class A is finite or Left_Cosets Normalizer A is finite implies ex C being finite set st C = con_class A & card C = index Normalizer A; theorem :: GROUP_1A:331 card con_class a = Index Normalizer{a}; theorem :: GROUP_1A:332 con_class a is finite or Left_Cosets Normalizer{a} is finite implies ex C being finite set st C = con_class a & card C = index Normalizer{a}; definition let G,H; func Normalizer H -> strict Subgroup of G equals :: GROUP_1A:def 43 Normalizer carr H; end; theorem :: GROUP_1A:333 for H being strict Subgroup of G holds x in Normalizer H iff ex h st x = h & H * h = H; theorem :: GROUP_1A:334 for H being strict Subgroup of G holds card con_class H = Index Normalizer H; theorem :: GROUP_1A:335 for H being strict Subgroup of G holds con_class H is finite or Left_Cosets Normalizer H is finite implies ex C being finite set st C = con_class H & card C = index Normalizer H; theorem :: GROUP_1A:336 for G being strict addGroup, H being strict Subgroup of G holds H is normal Subgroup of G iff Normalizer H = G; theorem :: GROUP_1A:337 for G being strict addGroup holds Normalizer (0).G = G; theorem :: GROUP_1A:338 for G being strict addGroup holds Normalizer (Omega).G = G; begin ::: TOPGRP1B reserve S, R for 1-sorted, X for Subset of R, T for TopStruct, x for set; reserve H for non empty addMagma, P, Q, P1, Q1 for Subset of H, h for Element of H; theorem :: GROUP_1A:339 P c= P1 & Q c= Q1 implies P + Q c= P1 + Q1; theorem :: GROUP_1A:340 P c= Q implies P + h c= Q + h; theorem :: GROUP_1A:341 P c= Q implies h + P c= h + Q; reserve a for Element of G; theorem :: GROUP_1A:342 a in -A iff -a in A; theorem :: GROUP_1A:343 A c= B iff -A c= -B; theorem :: GROUP_1A:344 (add_inverse G).:A = -A; theorem :: GROUP_1A:345 (add_inverse G)" A = -A; theorem :: GROUP_1A:346 add_inverse G is one-to-one; theorem :: GROUP_1A:347 rng add_inverse G = the carrier of G; registration let G be addGroup; cluster add_inverse G -> one-to-one onto; end; theorem :: GROUP_1A:348 (add_inverse G)" = add_inverse G; theorem :: GROUP_1A:349 (the addF of H).:[:P,Q:] = P + Q; definition let G be non empty addMagma, a be Element of G; func a+ -> Function of G, G means :: GROUP_1A:def 44 for x being Element of G holds it.x = a + x; func +a -> Function of G, G means :: GROUP_1A:def 45 for x being Element of G holds it.x = x + a; end; registration let G be addGroup, a be Element of G; cluster a+ -> one-to-one onto; cluster +a -> one-to-one onto; end; theorem :: GROUP_1A:350 h+.:P = h + P; theorem :: GROUP_1A:351 (+h).:P = P + h; theorem :: GROUP_1A:352 a+/" = (-a)+; theorem :: GROUP_1A:353 (+a)/" = +(-a); :: On the topological groups definition struct (addMagma, TopStruct) TopaddGrStr (# carrier -> set, addF -> BinOp of the carrier, topology -> Subset-Family of the carrier #); end; registration let A be non empty set, R be BinOp of A, T be Subset-Family of A; cluster TopaddGrStr (#A, R, T#) -> non empty; end; registration let x be set, R be BinOp of {x}, T be Subset-Family of {x}; cluster TopaddGrStr (#{x}, R, T#) -> trivial; end; registration cluster -> addGroup-like add-associative Abelian for 1-element addMagma; end; registration cluster strict non empty for TopaddGrStr; end; registration cluster strict TopSpace-like 1-element for TopaddGrStr; end; definition let G be addGroup-like add-associative non empty TopaddGrStr; attr G is UnContinuous means :: GROUP_1A:def 46 add_inverse G is continuous; end; definition let G be TopSpace-like TopaddGrStr; attr G is BinContinuous means :: GROUP_1A:def 47 for f being Function of [:G,G:], G st f = the addF of G holds f is continuous; end; registration cluster strict Abelian UnContinuous BinContinuous for TopSpace-like addGroup-like add-associative 1-element TopaddGrStr; end; definition mode TopaddGroup is TopSpace-like addGroup-like add-associative non empty TopaddGrStr; end; definition mode TopologicaladdGroup is UnContinuous BinContinuous TopaddGroup; end; theorem :: GROUP_1A:354 for T being BinContinuous non empty TopSpace-like TopaddGrStr, a, b being Element of T, W being a_neighborhood of a+b ex A being open a_neighborhood of a, B being open a_neighborhood of b st A+B c= W; theorem :: GROUP_1A:355 for T being TopSpace-like non empty TopaddGrStr st (for a, b being Element of T, W being a_neighborhood of a+b ex A being a_neighborhood of a, B being a_neighborhood of b st A+B c= W) holds T is BinContinuous; theorem :: GROUP_1A:356 for T being UnContinuous TopaddGroup, a being Element of T, W being a_neighborhood of -a ex A being open a_neighborhood of a st -A c= W; theorem :: GROUP_1A:357 for T being TopaddGroup st for a being Element of T, W being a_neighborhood of -a ex A being a_neighborhood of a st -A c= W holds T is UnContinuous; theorem :: GROUP_1A:358 for T being TopologicaladdGroup, a, b being Element of T for W being a_neighborhood of a+ (-b) ex A being open a_neighborhood of a, B being open a_neighborhood of b st A + (-B) c= W; theorem :: GROUP_1A:359 for T being TopaddGroup st for a, b being Element of T, W being a_neighborhood of a+(-b) ex A being a_neighborhood of a, B being a_neighborhood of b st A+(-B) c= W holds T is TopologicaladdGroup; registration let G be BinContinuous non empty TopSpace-like TopaddGrStr, a be Element of G; cluster a+ -> continuous; cluster +a -> continuous; end; theorem :: GROUP_1A:360 for G being BinContinuous TopaddGroup, a being Element of G holds a+ is Homeomorphism of G; theorem :: GROUP_1A:361 for G being BinContinuous TopaddGroup, a being Element of G holds + a is Homeomorphism of G; definition let G be BinContinuous TopaddGroup, a be Element of G; redefine func a+ -> Homeomorphism of G; redefine func +a -> Homeomorphism of G; end; theorem :: GROUP_1A:362 for G being UnContinuous TopaddGroup holds add_inverse G is Homeomorphism of G; definition let G be UnContinuous TopaddGroup; redefine func add_inverse G -> Homeomorphism of G; end; registration cluster BinContinuous -> homogeneous for TopaddGroup; end; theorem :: GROUP_1A:363 for G being BinContinuous TopaddGroup, F being closed Subset of G, a being Element of G holds F + a is closed; theorem :: GROUP_1A:364 for G being BinContinuous TopaddGroup, F being closed Subset of G, a being Element of G holds a + F is closed; registration let G be BinContinuous TopaddGroup, F be closed Subset of G, a be Element of G; cluster F + a -> closed; cluster a + F -> closed; end; theorem :: GROUP_1A:365 for G being UnContinuous TopaddGroup, F being closed Subset of G holds -F is closed; registration let G be UnContinuous TopaddGroup, F be closed Subset of G; cluster -F -> closed; end; theorem :: GROUP_1A:366 for G being BinContinuous TopaddGroup, O being open Subset of G, a being Element of G holds O + a is open; theorem :: GROUP_1A:367 for G being BinContinuous TopaddGroup, O being open Subset of G, a being Element of G holds a + O is open; registration let G be BinContinuous TopaddGroup, A be open Subset of G, a be Element of G; cluster A + a -> open; cluster a + A -> open; end; theorem :: GROUP_1A:368 for G being UnContinuous TopaddGroup, O being open Subset of G holds -O is open; registration let G be UnContinuous TopaddGroup, A be open Subset of G; cluster -A -> open; end; theorem :: GROUP_1A:369 for G being BinContinuous TopaddGroup, A, O being Subset of G st O is open holds O + A is open; theorem :: GROUP_1A:370 for G being BinContinuous TopaddGroup, A, O being Subset of G st O is open holds A + O is open; registration let G be BinContinuous TopaddGroup, A be open Subset of G, B be Subset of G; cluster A + B -> open; cluster B + A -> open; end; theorem :: GROUP_1A:371 for G being UnContinuous TopaddGroup, a being Point of G, A being a_neighborhood of a holds -A is a_neighborhood of -a; theorem :: GROUP_1A:372 for G being TopologicaladdGroup, a being Point of G, A being a_neighborhood of a + (-a) ex B being open a_neighborhood of a st B + (-B) c= A; theorem :: GROUP_1A:373 for G being UnContinuous TopaddGroup, A being dense Subset of G holds -A is dense; registration let G be UnContinuous TopaddGroup, A be dense Subset of G; cluster -A -> dense; end; theorem :: GROUP_1A:374 for G being BinContinuous TopaddGroup, A being dense Subset of G, a being Point of G holds a+A is dense; theorem :: GROUP_1A:375 for G being BinContinuous TopaddGroup, A being dense Subset of G, a being Point of G holds A+a is dense; registration let G be BinContinuous TopaddGroup, A be dense Subset of G, a be Point of G; cluster A + a -> dense; cluster a + A -> dense; end; theorem :: GROUP_1A:376 for G being TopologicaladdGroup, B being Basis of 0_G, M being dense Subset of G holds { V + x where V is Subset of G, x is Point of G: V in B & x in M } is Basis of G; registration cluster -> regular for TopologicaladdGroup; end;