:: 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;