:: Groups -- Additive Notation
:: by Roland Coghetto
::
:: Received April 30, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users


scheme :: GROUP_1A:sch 1
SeqEx2Dbis{ F1() -> non empty set , F2() -> non empty set , P1[ set , set , set ] } :
ex f being Function of [:NAT,F1():],F2() st
for x being Nat
for y being Element of F1() holds P1[x,y,f . (x,y)]
provided
A1: for x being Nat
for y being Element of F1() ex z being Element of F2() st P1[x,y,z]
proof end;

Lm1: now :: thesis: ( ( for h, g, f being Element of addMagma(# REAL,addreal #) holds (h + g) + f = h + (g + f) ) & ex e being Element of addMagma(# REAL,addreal #) st
for h being Element of addMagma(# REAL,addreal #) holds
( h + e = h & e + h = h & ex g being Element of addMagma(# REAL,addreal #) st
( h + g = e & g + h = e ) ) )
set G = addMagma(# REAL,addreal #);
thus for h, g, f being Element of addMagma(# REAL,addreal #) holds (h + g) + f = h + (g + f) :: thesis: ex e being Element of addMagma(# REAL,addreal #) st
for h being Element of addMagma(# REAL,addreal #) holds
( h + e = h & e + h = h & ex g being Element of addMagma(# REAL,addreal #) st
( h + g = e & g + h = e ) )
proof
let h, g, f be Element of addMagma(# REAL,addreal #); :: thesis: (h + g) + f = h + (g + f)
reconsider A = h, B = g, C = f as Real ;
A1: g + f = B + C by BINOP_2:def 9;
h + g = A + B by BINOP_2:def 9;
hence (h + g) + f = (A + B) + C by BINOP_2:def 9
.= A + (B + C)
.= h + (g + f) by A1, BINOP_2:def 9 ;
:: thesis: verum
end;
reconsider e = 0 as Element of addMagma(# REAL,addreal #) by XREAL_0:def 1;
take e = e; :: thesis: for h being Element of addMagma(# REAL,addreal #) holds
( h + e = h & e + h = h & ex g being Element of addMagma(# REAL,addreal #) st
( h + g = e & g + h = e ) )

let h be Element of addMagma(# REAL,addreal #); :: thesis: ( h + e = h & e + h = h & ex g being Element of addMagma(# REAL,addreal #) st
( h + g = e & g + h = e ) )

reconsider A = h as Real ;
thus h + e = A + 0 by BINOP_2:def 9
.= h ; :: thesis: ( e + h = h & ex g being Element of addMagma(# REAL,addreal #) st
( h + g = e & g + h = e ) )

thus e + h = 0 + A by BINOP_2:def 9
.= h ; :: thesis: ex g being Element of addMagma(# REAL,addreal #) st
( h + g = e & g + h = e )

reconsider g = - A as Element of addMagma(# REAL,addreal #) by XREAL_0:def 1;
take g = g; :: thesis: ( h + g = e & g + h = e )
thus h + g = A + (- A) by BINOP_2:def 9
.= e ; :: thesis: g + h = e
thus g + h = (- A) + A by BINOP_2:def 9
.= e ; :: thesis: verum
end;

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

:: deftheorem defines add-unital GROUP_1A:def 1 :
for IT being addMagma holds
( IT is add-unital iff ex e being Element of IT st
for h being Element of IT holds
( h + e = h & e + h = h ) );

:: deftheorem Def2 defines addGroup-like GROUP_1A:def 2 :
for IT being addMagma holds
( IT is addGroup-like iff 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 ) ) );

registration
cluster addGroup-like -> add-unital for addMagma ;
coherence
for b1 being addMagma st b1 is addGroup-like holds
b1 is add-unital
;
end;

registration
cluster non empty strict add-associative addGroup-like for addMagma ;
existence
ex b1 being addMagma st
( b1 is strict & b1 is addGroup-like & b1 is add-associative & not b1 is empty )
proof end;
end;

definition
mode addGroup is non empty add-associative addGroup-like addMagma ;
end;

theorem :: GROUP_1A:1
for S being non empty addMagma st ( for r, s, t being Element of S holds (r + s) + t = r + (s + t) ) & ex t being Element of S st
for s1 being Element of S holds
( s1 + t = s1 & t + s1 = s1 & ex s2 being Element of S st
( s1 + s2 = t & s2 + s1 = t ) ) holds
S is addGroup by Def2, RLVECT_1:def 3;

theorem :: GROUP_1A:2
for S being non empty addMagma st ( for r, s, t being Element of S holds (r + s) + t = r + (s + t) ) & ( for r, s being Element of S holds
( ex t being Element of S st r + t = s & ex t being Element of S st t + r = s ) ) holds
( S is add-associative & S is addGroup-like )
proof end;

theorem Th3: :: GROUP_1A:3
( addMagma(# REAL,addreal #) is add-associative & addMagma(# REAL,addreal #) is addGroup-like )
proof end;

definition
let G be addMagma ;
assume A1: G is add-unital ;
func 0_ G -> Element of G means :Def4: :: GROUP_1A:def 3
for h being Element of G holds
( h + it = h & it + h = h );
existence
ex b1 being Element of G st
for h being Element of G holds
( h + b1 = h & b1 + h = h )
by A1;
uniqueness
for b1, b2 being Element of G st ( for h being Element of G holds
( h + b1 = h & b1 + h = h ) ) & ( for h being Element of G holds
( h + b2 = h & b2 + h = h ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines 0_ GROUP_1A:def 3 :
for G being addMagma st G is add-unital holds
for b2 being Element of G holds
( b2 = 0_ G iff for h being Element of G holds
( h + b2 = h & b2 + h = h ) );

theorem :: GROUP_1A:4
for G being non empty addGroup-like addMagma
for e being Element of G st ( for h being Element of G holds
( h + e = h & e + h = h ) ) holds
e = 0_ G by Def4;

definition
let G be addGroup;
let h be Element of G;
func - h -> Element of G means :Def5: :: GROUP_1A:def 4
( h + it = 0_ G & it + h = 0_ G );
existence
ex b1 being Element of G st
( h + b1 = 0_ G & b1 + h = 0_ G )
proof end;
uniqueness
for b1, b2 being Element of G st h + b1 = 0_ G & b1 + h = 0_ G & h + b2 = 0_ G & b2 + h = 0_ G holds
b1 = b2
proof end;
involutiveness
for b1, b2 being Element of G st b2 + b1 = 0_ G & b1 + b2 = 0_ G holds
( b1 + b2 = 0_ G & b2 + b1 = 0_ G )
;
end;

:: deftheorem Def5 defines - GROUP_1A:def 4 :
for G being addGroup
for h, b3 being Element of G holds
( b3 = - h iff ( h + b3 = 0_ G & b3 + h = 0_ G ) );

theorem :: GROUP_1A:5
for G being addGroup
for g, h being Element of G st h + g = 0_ G & g + h = 0_ G holds
g = - h by Def5;

theorem Th6: :: GROUP_1A:6
for G being addGroup
for f, g, h being Element of G st ( h + g = h + f or g + h = f + h ) holds
g = f
proof end;

theorem Th7: :: GROUP_1A:7
for G being addGroup
for g, h being Element of G st ( h + g = h or g + h = h ) holds
g = 0_ G
proof end;

theorem Th8: :: GROUP_1A:8
for G being addGroup holds - (0_ G) = 0_ G
proof end;

theorem TH9: :: GROUP_1A:9
for G being addGroup
for g, h being Element of G st - h = - g holds
h = g
proof end;

theorem :: GROUP_1A:10
for G being addGroup
for h being Element of G st - h = 0_ G holds
h = 0_ G
proof end;

theorem Th11: :: GROUP_1A:11
for G being addGroup
for g, h being Element of G st h + g = 0_ G holds
( h = - g & g = - h )
proof end;

theorem Th12: :: GROUP_1A:12
for G being addGroup
for f, g, h being Element of G holds
( h + f = g iff f = (- h) + g )
proof end;

theorem Th13: :: GROUP_1A:13
for G being addGroup
for f, g, h being Element of G holds
( f + h = g iff f = g + (- h) )
proof end;

theorem :: GROUP_1A:14
for G being addGroup
for g, h being Element of G ex f being Element of G st g + f = h
proof end;

theorem :: GROUP_1A:15
for G being addGroup
for g, h being Element of G ex f being Element of G st f + g = h
proof end;

theorem Th16: :: GROUP_1A:16
for G being addGroup
for g, h being Element of G holds - (h + g) = (- g) + (- h)
proof end;

theorem Th17: :: GROUP_1A:17
for G being addGroup
for g, h being Element of G holds
( g + h = h + g iff - (g + h) = (- g) + (- h) )
proof end;

theorem Th18: :: GROUP_1A:18
for G being addGroup
for g, h being Element of G holds
( g + h = h + g iff (- g) + (- h) = (- h) + (- g) )
proof end;

theorem Th19: :: GROUP_1A:19
for G being addGroup
for g, h being Element of G holds
( g + h = h + g iff g + (- h) = (- h) + g )
proof end;

definition
let G be addGroup;
func add_inverse G -> UnOp of G means :Def6: :: GROUP_1A:def 5
for h being Element of G holds it . h = - h;
existence
ex b1 being UnOp of G st
for h being Element of G holds b1 . h = - h
proof end;
uniqueness
for b1, b2 being UnOp of G st ( for h being Element of G holds b1 . h = - h ) & ( for h being Element of G holds b2 . h = - h ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines add_inverse GROUP_1A:def 5 :
for G being addGroup
for b2 being UnOp of G holds
( b2 = add_inverse G iff for h being Element of G holds b2 . h = - h );

registration
let G be non empty add-associative addMagma ;
cluster the addF of G -> associative ;
coherence
the addF of G is associative
proof end;
end;

theorem Th20: :: GROUP_1A:20
for G being non empty add-unital addMagma holds 0_ G is_a_unity_wrt the addF of G
proof end;

theorem Th21: :: GROUP_1A:21
for G being non empty add-unital addMagma holds the_unity_wrt the addF of G = 0_ G
proof end;

registration
let G be non empty add-unital addMagma ;
cluster the addF of G -> having_a_unity ;
coherence
the addF of G is having_a_unity
proof end;
end;

theorem Th22: :: GROUP_1A:22
for G being addGroup holds add_inverse G is_an_inverseOp_wrt the addF of G
proof end;

registration
let G be addGroup;
cluster the addF of G -> having_an_inverseOp ;
coherence
the addF of G is having_an_inverseOp
proof end;
end;

theorem :: GROUP_1A:23
for G being addGroup holds the_inverseOp_wrt the addF of G = add_inverse G
proof end;

definition
let G be non empty addMagma ;
func mult G -> Function of [:NAT, the carrier of G:], the carrier of G means :Def7: :: 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 ) );
existence
ex b1 being Function of [:NAT, the carrier of G:], the carrier of G st
for h being Element of G holds
( b1 . (0,h) = 0_ G & ( for n being Nat holds b1 . ((n + 1),h) = (b1 . (n,h)) + h ) )
proof end;
uniqueness
for b1, b2 being Function of [:NAT, the carrier of G:], the carrier of G st ( for h being Element of G holds
( b1 . (0,h) = 0_ G & ( for n being Nat holds b1 . ((n + 1),h) = (b1 . (n,h)) + h ) ) ) & ( for h being Element of G holds
( b2 . (0,h) = 0_ G & ( for n being Nat holds b2 . ((n + 1),h) = (b2 . (n,h)) + h ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines mult GROUP_1A:def 6 :
for G being non empty addMagma
for b2 being Function of [:NAT, the carrier of G:], the carrier of G holds
( b2 = mult G iff for h being Element of G holds
( b2 . (0,h) = 0_ G & ( for n being Nat holds b2 . ((n + 1),h) = (b2 . (n,h)) + h ) ) );

definition
let G be addGroup;
let i be Integer;
let h be Element of G;
func i * h -> Element of G equals :Def8: :: GROUP_1A:def 7
(mult G) . (|.i.|,h) if 0 <= i
otherwise - ((mult G) . (|.i.|,h));
correctness
coherence
( ( 0 <= i implies (mult G) . (|.i.|,h) is Element of G ) & ( not 0 <= i implies - ((mult G) . (|.i.|,h)) is Element of G ) )
;
consistency
for b1 being Element of G holds verum
;
;
end;

:: deftheorem Def8 defines * GROUP_1A:def 7 :
for G being addGroup
for i being Integer
for h being Element of G holds
( ( 0 <= i implies i * h = (mult G) . (|.i.|,h) ) & ( not 0 <= i implies i * h = - ((mult G) . (|.i.|,h)) ) );

definition
let G be addGroup;
let n be Nat;
let h be Element of G;
redefine func n * h equals :: GROUP_1A:def 8
(mult G) . (n,h);
compatibility
for b1 being Element of G holds
( b1 = n * h iff b1 = (mult G) . (n,h) )
proof end;
end;

:: deftheorem defines * GROUP_1A:def 8 :
for G being addGroup
for n being Nat
for h being Element of G holds n * h = (mult G) . (n,h);

Lm3: for G being addGroup
for h being Element of G holds 0 * h = 0_ G

by Def7;

Lm4: for n being Nat
for G being addGroup holds n * (0_ G) = 0_ G

proof end;

theorem ThA24: :: GROUP_1A:24
for G being addGroup
for h being Element of G holds 0 * h = 0_ G by Def7;

theorem Th25: :: GROUP_1A:25
for G being addGroup
for h being Element of G holds 1 * h = h
proof end;

theorem Th26: :: GROUP_1A:26
for G being addGroup
for h being Element of G holds 2 * h = h + h
proof end;

theorem :: GROUP_1A:27
for G being addGroup
for h being Element of G holds 3 * h = (h + h) + h
proof end;

theorem :: GROUP_1A:28
for G being addGroup
for h being Element of G holds
( 2 * h = 0_ G iff - h = h )
proof end;

Lm5: for m, n being Nat
for G being addGroup
for h being Element of G holds (n + m) * h = (n * h) + (m * h)

proof end;

Lm6: for n being Nat
for G being addGroup
for h being Element of G holds
( (n + 1) * h = (n * h) + h & (n + 1) * h = h + (n * h) )

proof end;

Lm9: for n being Nat
for G being addGroup
for g, h being Element of G st g + h = h + g holds
g + (n * h) = (n * h) + g

proof end;

Lm10: for m, n being Nat
for G being addGroup
for g, h being Element of G st g + h = h + g holds
(n * g) + (m * h) = (m * h) + (n * g)

proof end;

Lm11: for n being Nat
for G being addGroup
for g, h being Element of G st g + h = h + g holds
n * (g + h) = (n * g) + (n * h)

proof end;

theorem Th29: :: GROUP_1A:29
for i being Integer
for G being addGroup
for h being Element of G st i <= 0 holds
i * h = - (|.i.| * h)
proof end;

theorem :: GROUP_1A:30
for i being Integer
for G being addGroup holds i * (0_ G) = 0_ G
proof end;

theorem Th31: :: GROUP_1A:31
for G being addGroup
for h being Element of G holds (- 1) * h = - h
proof end;

Lm12: for i being Integer
for G being addGroup
for h being Element of G holds (- i) * h = - (i * h)

proof end;

Lm13: for j being Integer holds
( j >= 1 or j = 0 or j < 0 )

proof end;

Lm14: for j being Integer
for G being addGroup
for h being Element of G holds (j - 1) * h = (j * h) + ((- 1) * h)

proof end;

Lm15: for j being Integer holds
( j >= 0 or j = - 1 or j < - 1 )

proof end;

Lm16: for j being Integer
for G being addGroup
for h being Element of G holds (j + 1) * h = (j * h) + (1 * h)

proof end;

theorem Th32: :: GROUP_1A:32
for i, j being Integer
for G being addGroup
for h being Element of G holds (i + j) * h = (i * h) + (j * h)
proof end;

theorem Th33: :: GROUP_1A:33
for i being Integer
for G being addGroup
for h being Element of G holds
( (i + 1) * h = (i * h) + h & (i + 1) * h = h + (i * h) )
proof end;

theorem :: GROUP_1A:34
for i being Integer
for G being addGroup
for h being Element of G holds - (i * h) = - (i * h) ;

theorem ThA37: :: GROUP_1A:35
for i being Integer
for G being addGroup
for g, h being Element of G st g + h = h + g holds
i * (g + h) = (i * g) + (i * h)
proof end;

theorem Th38: :: GROUP_1A:36
for i, j being Integer
for G being addGroup
for g, h being Element of G st g + h = h + g holds
(i * g) + (j * h) = (j * h) + (i * g)
proof end;

theorem :: GROUP_1A:37
for i being Integer
for G being addGroup
for g, h being Element of G st g + h = h + g holds
g + (i * h) = (i * h) + g
proof end;

definition
let G be addGroup;
let h be Element of G;
attr h is being_of_order_0 means :: GROUP_1A:def 9
for n being Nat st n * h = 0_ G holds
n = 0 ;
end;

:: deftheorem defines being_of_order_0 GROUP_1A:def 9 :
for G being addGroup
for h being Element of G holds
( h is being_of_order_0 iff for n being Nat st n * h = 0_ G holds
n = 0 );

registration
let G be addGroup;
cluster 0_ G -> non being_of_order_0 ;
coherence
not 0_ G is being_of_order_0
proof end;
end;

definition
let G be addGroup;
let h be Element of G;
func ord h -> Element of NAT means :Def11: :: GROUP_1A:def 10
it = 0 if h is being_of_order_0
otherwise ( it * h = 0_ G & it <> 0 & ( for m being Nat st m * h = 0_ G & m <> 0 holds
it <= m ) );
existence
( ( h is being_of_order_0 implies ex b1 being Element of NAT st b1 = 0 ) & ( not h is being_of_order_0 implies ex b1 being Element of NAT st
( b1 * h = 0_ G & b1 <> 0 & ( for m being Nat st m * h = 0_ G & m <> 0 holds
b1 <= m ) ) ) )
proof end;
uniqueness
for b1, b2 being Element of NAT holds
( ( h is being_of_order_0 & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( not h is being_of_order_0 & b1 * h = 0_ G & b1 <> 0 & ( for m being Nat st m * h = 0_ G & m <> 0 holds
b1 <= m ) & b2 * h = 0_ G & b2 <> 0 & ( for m being Nat st m * h = 0_ G & m <> 0 holds
b2 <= m ) implies b1 = b2 ) )
proof end;
correctness
consistency
for b1 being Element of NAT holds verum
;
;
end;

:: deftheorem Def11 defines ord GROUP_1A:def 10 :
for G being addGroup
for h being Element of G
for b3 being Element of NAT holds
( ( h is being_of_order_0 implies ( b3 = ord h iff b3 = 0 ) ) & ( not h is being_of_order_0 implies ( b3 = ord h iff ( b3 * h = 0_ G & b3 <> 0 & ( for m being Nat st m * h = 0_ G & m <> 0 holds
b3 <= m ) ) ) ) );

theorem :: GROUP_1A:38
for G being addGroup
for h being Element of G holds (ord h) * h = 0_ G
proof end;

theorem :: GROUP_1A:39
for G being addGroup holds ord (0_ G) = 1
proof end;

theorem :: GROUP_1A:40
for G being addGroup
for h being Element of G st ord h = 1 holds
h = 0_ G
proof end;

registration
cluster non empty strict Abelian add-associative add-unital addGroup-like for addMagma ;
existence
ex b1 being addGroup st
( b1 is strict & b1 is Abelian )
proof end;
end;

theorem :: GROUP_1A:41
addMagma(# REAL,addreal #) is Abelian addGroup
proof end;

theorem Th44: :: GROUP_1A:42
for A being Abelian addGroup
for a, b being Element of A holds - (a + b) = (- a) + (- b) by Th16;

theorem :: GROUP_1A:43
for i being Integer
for A being Abelian addGroup
for a, b being Element of A holds i * (a + b) = (i * a) + (i * b) by ThA37;

theorem :: GROUP_1A:44
for A being Abelian addGroup holds
( addLoopStr(# the carrier of A, the addF of A,(0_ A) #) is Abelian & addLoopStr(# the carrier of A, the addF of A,(0_ A) #) is add-associative & addLoopStr(# the carrier of A, the addF of A,(0_ A) #) is right_zeroed & addLoopStr(# the carrier of A, the addF of A,(0_ A) #) is right_complementable )
proof end;

theorem Th49: :: GROUP_1A:45
for L being non empty add-unital addMagma
for x being Element of L holds (mult L) . (1,x) = x
proof end;

theorem :: GROUP_1A:46
for L being non empty add-unital addMagma
for x being Element of L holds (mult L) . (2,x) = x + x
proof end;

theorem :: GROUP_1A:47
for L being non empty Abelian add-associative add-unital addMagma
for x, y being Element of L
for n being Nat holds (mult L) . (n,(x + y)) = ((mult L) . (n,x)) + ((mult L) . (n,y))
proof end;

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;

:: deftheorem defines zero-preserving GROUP_1A:def 11 :
for G, H being addMagma
for IT being Function of G,H holds
( IT is zero-preserving iff IT . (0_ G) = 0_ H );

Lm1: for x being object
for G being addGroup
for A being Subset of G st x in A holds
x is Element of G

;

definition
let G be addGroup;
let A be Subset of G;
func - A -> Subset of G equals :: GROUP_1A:def 12
{ (- g) where g is Element of G : g in A } ;
coherence
{ (- g) where g is Element of G : g in A } is Subset of G
proof end;
involutiveness
for b1, b2 being Subset of G st b1 = { (- g) where g is Element of G : g in b2 } holds
b2 = { (- g) where g is Element of G : g in b1 }
proof end;
end;

:: deftheorem defines - GROUP_1A:def 12 :
for G being addGroup
for A being Subset of G holds - A = { (- g) where g is Element of G : g in A } ;

theorem Th2: :: GROUP_1A:48
for x being object
for G being addGroup
for A being Subset of G holds
( x in - A iff ex g being Element of G st
( x = - g & g in A ) ) ;

theorem ThB3: :: GROUP_1A:49
for G being addGroup
for g being Element of G holds - {g} = {(- g)}
proof end;

theorem :: GROUP_1A:50
for G being addGroup
for g, h being Element of G holds - {g,h} = {(- g),(- h)}
proof end;

theorem :: GROUP_1A:51
for G being addGroup holds - ({} the carrier of G) = {}
proof end;

theorem :: GROUP_1A:52
for G being addGroup holds - ([#] the carrier of G) = the carrier of G
proof end;

theorem ThX7: :: GROUP_1A:53
for G being addGroup
for A being Subset of G holds
( A <> {} iff - A <> {} )
proof end;

registration
let G be addGroup;
let A be empty Subset of G;
cluster - A -> empty ;
coherence
- A is empty
by ThX7;
end;

registration
let G be addGroup;
let A be non empty Subset of G;
cluster - A -> non empty ;
coherence
not - A is empty
by ThX7;
end;

definition
let G be non empty Abelian addMagma ;
let A, B be Subset of G;
:: original: +
redefine func A + B -> Element of bool the carrier of G;
commutativity
for A, B being Subset of G holds A + B = B + A
proof end;
end;

theorem ThX8: :: GROUP_1A:54
for x being object
for G being non empty addMagma
for A, B being Subset of G holds
( x in A + B iff ex g, h being Element of G st
( x = g + h & g in A & h in B ) ) ;

theorem Th9: :: GROUP_1A:55
for G being non empty addMagma
for A, B being Subset of G holds
( ( A <> {} & B <> {} ) iff A + B <> {} )
proof end;

theorem Th10: :: GROUP_1A:56
for G being non empty addMagma
for A, B, C being Subset of G st G is add-associative holds
(A + B) + C = A + (B + C)
proof end;

theorem :: GROUP_1A:57
for G being addGroup
for A, B being Subset of G holds - (A + B) = (- B) + (- A)
proof end;

theorem :: GROUP_1A:58
for G being non empty addMagma
for A, B, C being Subset of G holds A + (B \/ C) = (A + B) \/ (A + C)
proof end;

theorem :: GROUP_1A:59
for G being non empty addMagma
for A, B, C being Subset of G holds (A \/ B) + C = (A + C) \/ (B + C)
proof end;

theorem :: GROUP_1A:60
for G being non empty addMagma
for A, B, C being Subset of G holds A + (B /\ C) c= (A + B) /\ (A + C)
proof end;

theorem :: GROUP_1A:61
for G being non empty addMagma
for A, B, C being Subset of G holds (A /\ B) + C c= (A + C) /\ (B + C)
proof end;

theorem ThA16: :: GROUP_1A:62
for G being non empty addMagma
for A being Subset of G holds
( ({} the carrier of G) + A = {} & A + ({} the carrier of G) = {} )
proof end;

theorem ThX17: :: GROUP_1A:63
for G being addGroup
for A being Subset of G st A <> {} holds
( ([#] the carrier of G) + A = the carrier of G & A + ([#] the carrier of G) = the carrier of G )
proof end;

theorem Th18: :: GROUP_1A:64
for G being non empty addMagma
for g, h being Element of G holds {g} + {h} = {(g + h)}
proof end;

theorem :: GROUP_1A:65
for G being non empty addMagma
for g, g1, g2 being Element of G holds {g} + {g1,g2} = {(g + g1),(g + g2)}
proof end;

theorem :: GROUP_1A:66
for G being non empty addMagma
for g, g1, g2 being Element of G holds {g1,g2} + {g} = {(g1 + g),(g2 + g)}
proof end;

theorem :: GROUP_1A:67
for G being non empty addMagma
for g, g1, g2, h being Element of G holds {g,h} + {g1,g2} = {(g + g1),(g + g2),(h + g1),(h + g2)}
proof end;

theorem Th22: :: GROUP_1A:68
for G being addGroup
for A being Subset of G st ( 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 ) holds
A + A = A
proof end;

theorem Th23: :: GROUP_1A:69
for G being addGroup
for A being Subset of G st ( for g being Element of G st g in A holds
- g in A ) holds
- A = A
proof end;

theorem :: GROUP_1A:70
for G being non empty addMagma
for A, B being Subset of G st ( for a, b being Element of G st a in A & b in B holds
a + b = b + a ) holds
A + B = B + A
proof end;

Lm2: for A being Abelian addGroup
for a, b being Element of A holds a + b = b + a

;

theorem Th25: :: GROUP_1A:71
for G being non empty addMagma
for A, B being Subset of G st G is Abelian addGroup holds
A + B = B + A
proof end;

theorem :: GROUP_1A:72
for G being Abelian addGroup
for A, B being Subset of G holds - (A + B) = (- A) + (- B)
proof end;

definition
let G be non empty addMagma ;
let g be Element of G;
let A be Subset of G;
func g + A -> Subset of G equals :: GROUP_1A:def 13
{g} + A;
correctness
coherence
{g} + A is Subset of G
;
;
func A + g -> Subset of G equals :: GROUP_1A:def 14
A + {g};
correctness
coherence
A + {g} is Subset of G
;
;
end;

:: deftheorem defines + GROUP_1A:def 13 :
for G being non empty addMagma
for g being Element of G
for A being Subset of G holds g + A = {g} + A;

:: deftheorem defines + GROUP_1A:def 14 :
for G being non empty addMagma
for g being Element of G
for A being Subset of G holds A + g = A + {g};

theorem Th27: :: GROUP_1A:73
for x being object
for G being non empty addMagma
for A being Subset of G
for g being Element of G holds
( x in g + A iff ex h being Element of G st
( x = g + h & h in A ) )
proof end;

theorem Th28: :: GROUP_1A:74
for x being object
for G being non empty addMagma
for A being Subset of G
for g being Element of G holds
( x in A + g iff ex h being Element of G st
( x = h + g & h in A ) )
proof end;

theorem ThB29: :: GROUP_1A:75
for G being non empty addMagma
for A, B being Subset of G
for g being Element of G st G is add-associative holds
(g + A) + B = g + (A + B) by Th10;

theorem ThA30: :: GROUP_1A:76
for G being non empty addMagma
for A, B being Subset of G
for g being Element of G st G is add-associative holds
(A + g) + B = A + (g + B) by Th10;

theorem ThB31: :: GROUP_1A:77
for G being non empty addMagma
for A, B being Subset of G
for g being Element of G st G is add-associative holds
(A + B) + g = A + (B + g) by Th10;

theorem Th32: :: GROUP_1A:78
for G being non empty addMagma
for A being Subset of G
for g, h being Element of G st G is add-associative holds
(g + h) + A = g + (h + A)
proof end;

theorem ThA33: :: GROUP_1A:79
for G being non empty addMagma
for A being Subset of G
for g, h being Element of G st G is add-associative holds
(g + A) + h = g + (A + h) by Th10;

theorem ThB34: :: GROUP_1A:80
for G being non empty addMagma
for A being Subset of G
for g, h being Element of G st G is add-associative holds
(A + g) + h = A + (g + h)
proof end;

theorem :: GROUP_1A:81
for G being non empty addMagma
for a being Element of G holds
( ({} the carrier of G) + a = {} & a + ({} the carrier of G) = {} ) by ThA16;

theorem :: GROUP_1A:82
for G being addGroup
for a being Element of G holds
( ([#] the carrier of G) + a = the carrier of G & a + ([#] the carrier of G) = the carrier of G ) by ThX17;

theorem Th37: :: GROUP_1A:83
for G being non empty addGroup-like addMagma
for A being Subset of G holds
( (0_ G) + A = A & A + (0_ G) = A )
proof end;

theorem :: GROUP_1A:84
for G being non empty addGroup-like addMagma
for g being Element of G
for A being Subset of G st G is Abelian addGroup holds
g + A = A + g by Th25;

definition
let G be non empty addGroup-like addMagma ;
mode Subgroup of G -> non empty addGroup-like addMagma means :DefA5: :: 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 );
existence
ex b1 being non empty addGroup-like addMagma st
( the carrier of b1 c= the carrier of G & the addF of b1 = the addF of G || the carrier of b1 )
proof end;
end;

:: deftheorem DefA5 defines Subgroup GROUP_1A:def 15 :
for G, b2 being non empty addGroup-like addMagma holds
( b2 is Subgroup of G iff ( the carrier of b2 c= the carrier of G & the addF of b2 = the addF of G || the carrier of b2 ) );

theorem Th39: :: GROUP_1A:85
for G being non empty addGroup-like addMagma
for H being Subgroup of G st G is finite holds
H is finite
proof end;

theorem Th40: :: GROUP_1A:86
for x being object
for G being non empty addGroup-like addMagma
for H being Subgroup of G st x in H holds
x in G
proof end;

theorem Th41: :: GROUP_1A:87
for G being non empty addGroup-like addMagma
for H being Subgroup of G
for h being Element of H holds h in G by Th40, STRUCT_0:def 5;

theorem Th42: :: GROUP_1A:88
for G being non empty addGroup-like addMagma
for H being Subgroup of G
for h being Element of H holds h is Element of G by Th41, STRUCT_0:def 5;

theorem Th43: :: GROUP_1A:89
for G being non empty addGroup-like addMagma
for g1, g2 being Element of G
for H being Subgroup of G
for h1, h2 being Element of H st h1 = g1 & h2 = g2 holds
h1 + h2 = g1 + g2
proof end;

registration
let G be addGroup;
cluster -> add-associative for Subgroup of G;
coherence
for b1 being Subgroup of G holds b1 is add-associative
proof end;
end;

theorem Th44: :: GROUP_1A:90
for G being addGroup
for H being Subgroup of G holds 0_ H = 0_ G
proof end;

theorem :: GROUP_1A:91
for G being addGroup
for H1, H2 being Subgroup of G holds 0_ H1 = 0_ H2
proof end;

theorem Th46: :: GROUP_1A:92
for G being addGroup
for H being Subgroup of G holds 0_ G in H
proof end;

theorem :: GROUP_1A:93
for G being addGroup
for H1, H2 being Subgroup of G holds 0_ H1 in H2
proof end;

theorem Th48: :: GROUP_1A:94
for G being addGroup
for g being Element of G
for H being Subgroup of G
for h being Element of H st h = g holds
- h = - g
proof end;

theorem :: GROUP_1A:95
for G being addGroup
for H being Subgroup of G holds add_inverse H = (add_inverse G) | the carrier of H
proof end;

theorem Th50: :: GROUP_1A:96
for G being addGroup
for g1, g2 being Element of G
for H being Subgroup of G st g1 in H & g2 in H holds
g1 + g2 in H
proof end;

theorem Th51: :: GROUP_1A:97
for G being addGroup
for g being Element of G
for H being Subgroup of G st g in H holds
- g in H
proof end;

registration
let G be addGroup;
cluster non empty strict add-associative add-unital addGroup-like for Subgroup of G;
existence
ex b1 being Subgroup of G st b1 is strict
proof end;
end;

theorem Th52: :: GROUP_1A:98
for G being addGroup
for A being Subset of G st A <> {} & ( 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 ) holds
ex H being strict Subgroup of G st the carrier of H = A
proof end;

theorem Th53: :: GROUP_1A:99
for G being addGroup
for H being Subgroup of G st G is Abelian addGroup holds
H is Abelian
proof end;

registration
let G be Abelian addGroup;
cluster -> Abelian for Subgroup of G;
coherence
for b1 being Subgroup of G holds b1 is Abelian
by Th53;
end;

theorem ThA54: :: GROUP_1A:100
for G being addGroup holds G is Subgroup of G
proof end;

theorem Th55: :: GROUP_1A:101
for G1, G2 being addGroup st G1 is Subgroup of G2 & G2 is Subgroup of G1 holds
addMagma(# the carrier of G1, the addF of G1 #) = addMagma(# the carrier of G2, the addF of G2 #)
proof end;

theorem Th56: :: GROUP_1A:102
for G1, G2, G3 being addGroup st G1 is Subgroup of G2 & G2 is Subgroup of G3 holds
G1 is Subgroup of G3
proof end;

theorem Th57: :: GROUP_1A:103
for G being addGroup
for H1, H2 being Subgroup of G st the carrier of H1 c= the carrier of H2 holds
H1 is Subgroup of H2
proof end;

theorem Th58: :: GROUP_1A:104
for G being addGroup
for H1, H2 being Subgroup of G st ( for g being Element of G st g in H1 holds
g in H2 ) holds
H1 is Subgroup of H2
proof end;

theorem Th59: :: GROUP_1A:105
for G being addGroup
for H1, H2 being Subgroup of G st the carrier of H1 = the carrier of H2 holds
addMagma(# the carrier of H1, the addF of H1 #) = addMagma(# the carrier of H2, the addF of H2 #)
proof end;

theorem Th60: :: GROUP_1A:106
for G being addGroup
for H1, H2 being Subgroup of G st ( for g being Element of G holds
( g in H1 iff g in H2 ) ) holds
addMagma(# the carrier of H1, the addF of H1 #) = addMagma(# the carrier of H2, the addF of H2 #)
proof end;

definition
let G be addGroup;
let H1, H2 be strict Subgroup of G;
:: original: =
redefine pred H1 = H2 means :: GROUP_1A:def 16
for g being Element of G holds
( g in H1 iff g in H2 );
compatibility
( H1 = H2 iff for g being Element of G holds
( g in H1 iff g in H2 ) )
by Th60;
end;

:: deftheorem defines = GROUP_1A:def 16 :
for G being addGroup
for H1, H2 being strict Subgroup of G holds
( H1 = H2 iff for g being Element of G holds
( g in H1 iff g in H2 ) );

theorem Th61: :: GROUP_1A:107
for G being addGroup
for H being Subgroup of G st the carrier of G c= the carrier of H holds
addMagma(# the carrier of H, the addF of H #) = addMagma(# the carrier of G, the addF of G #)
proof end;

theorem Th62: :: GROUP_1A:108
for G being addGroup
for H being Subgroup of G st ( for g being Element of G holds g in H ) holds
addMagma(# the carrier of H, the addF of H #) = addMagma(# the carrier of G, the addF of G #)
proof end;

definition
let G be addGroup;
func (0). G -> strict Subgroup of G means :Def7: :: GROUP_1A:def 17
the carrier of it = {(0_ G)};
existence
ex b1 being strict Subgroup of G st the carrier of b1 = {(0_ G)}
proof end;
uniqueness
for b1, b2 being strict Subgroup of G st the carrier of b1 = {(0_ G)} & the carrier of b2 = {(0_ G)} holds
b1 = b2
by Th59;
end;

:: deftheorem Def7 defines (0). GROUP_1A:def 17 :
for G being addGroup
for b2 being strict Subgroup of G holds
( b2 = (0). G iff the carrier of b2 = {(0_ G)} );

definition
let G be addGroup;
func (Omega). G -> strict Subgroup of G equals :: GROUP_1A:def 18
addMagma(# the carrier of G, the addF of G #);
coherence
addMagma(# the carrier of G, the addF of G #) is strict Subgroup of G
proof end;
projectivity
for b1 being strict Subgroup of G
for b2 being addGroup st b1 = addMagma(# the carrier of b2, the addF of b2 #) holds
b1 = addMagma(# the carrier of b1, the addF of b1 #)
;
end;

:: deftheorem defines (Omega). GROUP_1A:def 18 :
for G being addGroup holds (Omega). G = addMagma(# the carrier of G, the addF of G #);

theorem Th63: :: GROUP_1A:109
for G being addGroup
for H being Subgroup of G holds (0). H = (0). G
proof end;

theorem :: GROUP_1A:110
for G being addGroup
for H1, H2 being Subgroup of G holds (0). H1 = (0). H2
proof end;

theorem Th65: :: GROUP_1A:111
for G being addGroup
for H being Subgroup of G holds (0). G is Subgroup of H
proof end;

theorem :: GROUP_1A:112
for G being strict addGroup
for 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 Th68: :: GROUP_1A:114
for G being addGroup holds (0). G is finite
proof end;

registration
let G be addGroup;
cluster (0). G -> finite strict ;
coherence
(0). G is finite
by Th68;
cluster non empty finite strict add-associative add-unital addGroup-like for Subgroup of G;
existence
ex b1 being Subgroup of G st
( b1 is strict & b1 is finite )
proof end;
end;

registration
cluster non empty finite strict add-associative add-unital addGroup-like for addMagma ;
existence
ex b1 being addGroup st
( b1 is strict & b1 is finite )
proof end;
end;

registration
let G be finite addGroup;
cluster -> finite for Subgroup of G;
coherence
for b1 being Subgroup of G holds b1 is finite
by Th39;
end;

theorem Th69: :: GROUP_1A:115
for G being addGroup holds card ((0). G) = 1
proof end;

theorem Th70: :: GROUP_1A:116
for G being addGroup
for H being finite strict Subgroup of G st card H = 1 holds
H = (0). G
proof end;

theorem :: GROUP_1A:117
for G being addGroup
for H being Subgroup of G holds card H c= card G by DefA5, CARD_1:11;

theorem :: GROUP_1A:118
for G being finite addGroup
for H being Subgroup of G holds card H <= card G by DefA5, NAT_1:43;

theorem :: GROUP_1A:119
for G being finite addGroup
for H being Subgroup of G st card G = card H holds
addMagma(# the carrier of H, the addF of H #) = addMagma(# the carrier of G, the addF of G #)
proof end;

definition
let G be addGroup;
let H be Subgroup of G;
func carr H -> Subset of G equals :: GROUP_1A:def 19
the carrier of H;
coherence
the carrier of H is Subset of G
by DefA5;
end;

:: deftheorem defines carr GROUP_1A:def 19 :
for G being addGroup
for H being Subgroup of G holds carr H = the carrier of H;

theorem Th74: :: GROUP_1A:120
for G being addGroup
for g1, g2 being Element of G
for H being Subgroup of G st g1 in carr H & g2 in carr H holds
g1 + g2 in carr H
proof end;

theorem Th75: :: GROUP_1A:121
for G being addGroup
for g being Element of G
for H being Subgroup of G st g in carr H holds
- g in carr H
proof end;

theorem :: GROUP_1A:122
for G being addGroup
for H being Subgroup of G holds (carr H) + (carr H) = carr H
proof end;

theorem :: GROUP_1A:123
for G being addGroup
for H being Subgroup of G holds - (carr H) = carr H
proof end;

theorem Th78: :: GROUP_1A:124
for G being addGroup
for H1, H2 being Subgroup of G holds
( ( (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 being Subgroup of G st the carrier of H = (carr H1) + (carr H2) implies (carr H1) + (carr H2) = (carr H2) + (carr H1) ) )
proof end;

theorem :: GROUP_1A:125
for G being addGroup
for H1, H2 being Subgroup of G st G is Abelian addGroup holds
ex H being strict Subgroup of G st the carrier of H = (carr H1) + (carr H2)
proof end;

definition
let G be addGroup;
let H1, H2 be Subgroup of G;
func H1 /\ H2 -> strict Subgroup of G means :Def10: :: GROUP_1A:def 20
the carrier of it = (carr H1) /\ (carr H2);
existence
ex b1 being strict Subgroup of G st the carrier of b1 = (carr H1) /\ (carr H2)
proof end;
uniqueness
for b1, b2 being strict Subgroup of G st the carrier of b1 = (carr H1) /\ (carr H2) & the carrier of b2 = (carr H1) /\ (carr H2) holds
b1 = b2
by Th59;
end;

:: deftheorem Def10 defines /\ GROUP_1A:def 20 :
for G being addGroup
for H1, H2 being Subgroup of G
for b4 being strict Subgroup of G holds
( b4 = H1 /\ H2 iff the carrier of b4 = (carr H1) /\ (carr H2) );

theorem Th80: :: GROUP_1A:126
for G being addGroup
for H1, H2 being Subgroup of G holds
( ( 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 st the carrier of H = the carrier of H1 /\ the carrier of H2 holds
H = H1 /\ H2 ) )
proof end;

theorem :: GROUP_1A:127
for G being addGroup
for H1, H2 being Subgroup of G holds carr (H1 /\ H2) = (carr H1) /\ (carr H2) by Def10;

theorem Th82: :: GROUP_1A:128
for x being object
for G being addGroup
for H1, H2 being Subgroup of G holds
( x in H1 /\ H2 iff ( x in H1 & x in H2 ) )
proof end;

theorem :: GROUP_1A:129
for G being addGroup
for H being strict Subgroup of G holds H /\ H = H
proof end;

definition
let G be addGroup;
let H1, H2 be Subgroup of G;
:: original: /\
redefine func H1 /\ H2 -> strict Subgroup of G;
commutativity
for H1, H2 being Subgroup of G holds H1 /\ H2 = H2 /\ H1
proof end;
end;

theorem :: GROUP_1A:130
for G being addGroup
for H1, H2, H3 being Subgroup of G holds (H1 /\ H2) /\ H3 = H1 /\ (H2 /\ H3)
proof end;

Lm3: for G being addGroup
for H2, H1 being Subgroup of G holds
( H1 is Subgroup of H2 iff addMagma(# the carrier of (H1 /\ H2), the addF of (H1 /\ H2) #) = addMagma(# the carrier of H1, the addF of H1 #) )

proof end;

theorem :: GROUP_1A:131
for G being addGroup
for H being Subgroup of G holds
( ((0). G) /\ H = (0). G & H /\ ((0). G) = (0). G )
proof end;

theorem :: GROUP_1A:132
for G being strict addGroup
for H being strict Subgroup of G holds
( H /\ ((Omega). G) = H & ((Omega). G) /\ H = H ) by Lm3;

theorem :: GROUP_1A:133
for G being strict addGroup holds ((Omega). G) /\ ((Omega). G) = G by Lm3;

Lm4: for G being addGroup
for H1, H2 being Subgroup of G holds H1 /\ H2 is Subgroup of H1

proof end;

theorem :: GROUP_1A:134
for G being addGroup
for H1, H2 being Subgroup of G holds
( H1 /\ H2 is Subgroup of H1 & H1 /\ H2 is Subgroup of H2 ) by Lm4;

theorem :: GROUP_1A:135
for G being addGroup
for H2, H1 being Subgroup of G holds
( H1 is Subgroup of H2 iff addMagma(# the carrier of (H1 /\ H2), the addF of (H1 /\ H2) #) = addMagma(# the carrier of H1, the addF of H1 #) ) by Lm3;

theorem :: GROUP_1A:136
for G being addGroup
for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 holds
H1 /\ H3 is Subgroup of H2
proof end;

theorem :: GROUP_1A:137
for G being addGroup
for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 & H1 is Subgroup of H3 holds
H1 is Subgroup of H2 /\ H3
proof end;

theorem :: GROUP_1A:138
for G being addGroup
for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 holds
H1 /\ H3 is Subgroup of H2 /\ H3
proof end;

theorem :: GROUP_1A:139
for G being addGroup
for H1, H2 being Subgroup of G st ( H1 is finite or H2 is finite ) holds
H1 /\ H2 is finite
proof end;

definition
let G be addGroup;
let H be Subgroup of G;
let A be Subset of G;
func A + H -> Subset of G equals :: GROUP_1A:def 21
A + (carr H);
correctness
coherence
A + (carr H) is Subset of G
;
;
func H + A -> Subset of G equals :: GROUP_1A:def 22
(carr H) + A;
correctness
coherence
(carr H) + A is Subset of G
;
;
end;

:: deftheorem defines + GROUP_1A:def 21 :
for G being addGroup
for H being Subgroup of G
for A being Subset of G holds A + H = A + (carr H);

:: deftheorem defines + GROUP_1A:def 22 :
for G being addGroup
for H being Subgroup of G
for A being Subset of G holds H + A = (carr H) + A;

theorem Th94: :: GROUP_1A:140
for x being object
for G being addGroup
for A being Subset of G
for H being Subgroup of G holds
( x in A + H iff ex g1, g2 being Element of G st
( x = g1 + g2 & g1 in A & g2 in H ) )
proof end;

theorem ThB95: :: GROUP_1A:141
for x being object
for G being addGroup
for A being Subset of G
for H being Subgroup of G holds
( x in H + A iff ex g1, g2 being Element of G st
( x = g1 + g2 & g1 in H & g2 in A ) )
proof end;

theorem Th96: :: GROUP_1A:142
for G being addGroup
for A, B being Subset of G
for H being Subgroup of G holds (A + B) + H = A + (B + H) by Th10;

theorem Th97: :: GROUP_1A:143
for G being addGroup
for A, B being Subset of G
for H being Subgroup of G holds (A + H) + B = A + (H + B) by Th10;

theorem Th98: :: GROUP_1A:144
for G being addGroup
for A, B being Subset of G
for H being Subgroup of G holds (H + A) + B = H + (A + B) by Th10;

theorem :: GROUP_1A:145
for G being addGroup
for A being Subset of G
for H1, H2 being Subgroup of G holds (A + H1) + H2 = A + (H1 + (carr H2)) by Th10;

theorem :: GROUP_1A:146
for G being addGroup
for A being Subset of G
for H1, H2 being Subgroup of G holds (H1 + A) + H2 = H1 + (A + H2) by Th10;

theorem :: GROUP_1A:147
for G being addGroup
for A being Subset of G
for H1, H2 being Subgroup of G holds (H1 + (carr H2)) + A = H1 + (H2 + A) by Th10;

theorem :: GROUP_1A:148
for G being addGroup
for A being Subset of G
for H being Subgroup of G st G is Abelian addGroup holds
A + H = H + A by Th25;

definition
let G be addGroup;
let H be Subgroup of G;
let a be Element of G;
func a + H -> Subset of G equals :: GROUP_1A:def 23
a + (carr H);
correctness
coherence
a + (carr H) is Subset of G
;
;
func H + a -> Subset of G equals :: GROUP_1A:def 24
(carr H) + a;
correctness
coherence
(carr H) + a is Subset of G
;
;
end;

:: deftheorem defines + GROUP_1A:def 23 :
for G being addGroup
for H being Subgroup of G
for a being Element of G holds a + H = a + (carr H);

:: deftheorem defines + GROUP_1A:def 24 :
for G being addGroup
for H being Subgroup of G
for a being Element of G holds H + a = (carr H) + a;

theorem Th103: :: GROUP_1A:149
for x being object
for G being addGroup
for a being Element of G
for H being Subgroup of G holds
( x in a + H iff ex g being Element of G st
( x = a + g & g in H ) )
proof end;

theorem Th104: :: GROUP_1A:150
for x being object
for G being addGroup
for a being Element of G
for H being Subgroup of G holds
( x in H + a iff ex g being Element of G st
( x = g + a & g in H ) )
proof end;

theorem ThB105: :: GROUP_1A:151
for G being addGroup
for a, b being Element of G
for H being Subgroup of G holds (a + b) + H = a + (b + H) by Th32;

theorem ThB106: :: GROUP_1A:152
for G being addGroup
for a, b being Element of G
for H being Subgroup of G holds (a + H) + b = a + (H + b) by Th10;

theorem ThA107: :: GROUP_1A:153
for G being addGroup
for a, b being Element of G
for H being Subgroup of G holds (H + a) + b = H + (a + b) by ThB34;

theorem Th108: :: GROUP_1A:154
for G being addGroup
for a being Element of G
for H being Subgroup of G holds
( a in a + H & a in H + a )
proof end;

theorem ThB109: :: GROUP_1A:155
for G being addGroup
for H being Subgroup of G holds
( (0_ G) + H = carr H & H + (0_ G) = carr H ) by Th37;

theorem Th110: :: GROUP_1A:156
for G being addGroup
for a being Element of G holds
( ((0). G) + a = {a} & a + ((0). G) = {a} )
proof end;

theorem Th111: :: GROUP_1A:157
for G being addGroup
for a being Element of G holds
( a + ((Omega). G) = the carrier of G & ((Omega). G) + a = the carrier of G )
proof end;

theorem Th112: :: GROUP_1A:158
for G being addGroup
for a being Element of G
for H being Subgroup of G st G is Abelian addGroup holds
a + H = H + a by Th25;

theorem Th113: :: GROUP_1A:159
for G being addGroup
for a being Element of G
for H being Subgroup of G holds
( a in H iff a + H = carr H )
proof end;

theorem Th114: :: GROUP_1A:160
for G being addGroup
for a, b being Element of G
for H being Subgroup of G holds
( a + H = b + H iff (- b) + a in H )
proof end;

theorem Th115: :: GROUP_1A:161
for G being addGroup
for a, b being Element of G
for H being Subgroup of G holds
( a + H = b + H iff a + H meets b + H )
proof end;

theorem Th116: :: GROUP_1A:162
for G being addGroup
for a, b being Element of G
for H being Subgroup of G holds (a + b) + H c= (a + H) + (b + H)
proof end;

theorem :: GROUP_1A:163
for G being addGroup
for a being Element of G
for H being Subgroup of G holds
( carr H c= (a + H) + ((- a) + H) & carr H c= ((- a) + H) + (a + H) )
proof end;

theorem :: GROUP_1A:164
for G being addGroup
for a being Element of G
for H being Subgroup of G holds (2 * a) + H c= (a + H) + (a + H)
proof end;

theorem Th119: :: GROUP_1A:165
for G being addGroup
for a being Element of G
for H being Subgroup of G holds
( a in H iff H + a = carr H )
proof end;

theorem Th120: :: GROUP_1A:166
for G being addGroup
for a, b being Element of G
for H being Subgroup of G holds
( H + a = H + b iff b + (- a) in H )
proof end;

theorem Th121: :: GROUP_1A:167
for G being addGroup
for a, b being Element of G
for H being Subgroup of G holds
( H + a = H + b iff H + a meets H + b )
proof end;

theorem Th122: :: GROUP_1A:168
for G being addGroup
for a, b being Element of G
for H being Subgroup of G holds (H + a) + b c= (H + a) + (H + b)
proof end;

theorem :: GROUP_1A:169
for G being addGroup
for a being Element of G
for H being Subgroup of G holds
( carr H c= (H + a) + (H + (- a)) & carr H c= (H + (- a)) + (H + a) )
proof end;

theorem :: GROUP_1A:170
for G being addGroup
for a being Element of G
for H being Subgroup of G holds H + (2 * a) c= (H + a) + (H + a)
proof end;

theorem :: GROUP_1A:171
for G being addGroup
for a being Element of G
for H1, H2 being Subgroup of G holds a + (H1 /\ H2) = (a + H1) /\ (a + H2)
proof end;

theorem :: GROUP_1A:172
for G being addGroup
for a being Element of G
for H1, H2 being Subgroup of G holds (H1 /\ H2) + a = (H1 + a) /\ (H2 + a)
proof end;

theorem Th127: :: GROUP_1A:173
for G being addGroup
for a being Element of G
for H2 being Subgroup of G ex H1 being strict Subgroup of G st the carrier of H1 = (a + H2) + (- a)
proof end;

theorem Th128: :: GROUP_1A:174
for G being addGroup
for a, b being Element of G
for H being Subgroup of G holds a + H,b + H are_equipotent
proof end;

theorem Th129: :: GROUP_1A:175
for G being addGroup
for a, b being Element of G
for H being Subgroup of G holds a + H,H + b are_equipotent
proof end;

theorem Th130: :: GROUP_1A:176
for G being addGroup
for a, b being Element of G
for H being Subgroup of G holds H + a,H + b are_equipotent
proof end;

theorem Th131: :: GROUP_1A:177
for G being addGroup
for a being Element of G
for H being Subgroup of G holds
( carr H,a + H are_equipotent & carr H,H + a are_equipotent )
proof end;

theorem :: GROUP_1A:178
for G being addGroup
for a being Element of G
for H being Subgroup of G holds
( card H = card (a + H) & card H = card (H + a) ) by Th131, CARD_1:5;

theorem Th133: :: GROUP_1A:179
for G being addGroup
for a being Element of G
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 )
proof end;

definition
let G be addGroup;
let H be Subgroup of G;
func Left_Cosets H -> Subset-Family of G means :Def15: :: GROUP_1A:def 25
for A being Subset of G holds
( A in it iff ex a being Element of G st A = a + H );
existence
ex b1 being Subset-Family of G st
for A being Subset of G holds
( A in b1 iff ex a being Element of G st A = a + H )
proof end;
uniqueness
for b1, b2 being Subset-Family of G st ( for A being Subset of G holds
( A in b1 iff ex a being Element of G st A = a + H ) ) & ( for A being Subset of G holds
( A in b2 iff ex a being Element of G st A = a + H ) ) holds
b1 = b2
proof end;
func Right_Cosets H -> Subset-Family of G means :Def16: :: GROUP_1A:def 26
for A being Subset of G holds
( A in it iff ex a being Element of G st A = H + a );
existence
ex b1 being Subset-Family of G st
for A being Subset of G holds
( A in b1 iff ex a being Element of G st A = H + a )
proof end;
uniqueness
for b1, b2 being Subset-Family of G st ( for A being Subset of G holds
( A in b1 iff ex a being Element of G st A = H + a ) ) & ( for A being Subset of G holds
( A in b2 iff ex a being Element of G st A = H + a ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines Left_Cosets GROUP_1A:def 25 :
for G being addGroup
for H being Subgroup of G
for b3 being Subset-Family of G holds
( b3 = Left_Cosets H iff for A being Subset of G holds
( A in b3 iff ex a being Element of G st A = a + H ) );

:: deftheorem Def16 defines Right_Cosets GROUP_1A:def 26 :
for G being addGroup
for H being Subgroup of G
for b3 being Subset-Family of G holds
( b3 = Right_Cosets H iff for A being Subset of G holds
( A in b3 iff ex a being Element of G st A = H + a ) );

theorem :: GROUP_1A:180
for G being addGroup
for H being Subgroup of G st G is finite holds
( Right_Cosets H is finite & Left_Cosets H is finite ) ;

theorem Th135: :: GROUP_1A:181
for G being addGroup
for H being Subgroup of G holds
( carr H in Left_Cosets H & carr H in Right_Cosets H )
proof end;

theorem Th136: :: GROUP_1A:182
for G being addGroup
for H being Subgroup of G holds Left_Cosets H, Right_Cosets H are_equipotent
proof end;

theorem Th137: :: GROUP_1A:183
for G being addGroup
for H being Subgroup of G holds
( union (Left_Cosets H) = the carrier of G & union (Right_Cosets H) = the carrier of G )
proof end;

theorem Th138: :: GROUP_1A:184
for G being addGroup holds Left_Cosets ((0). G) = { {a} where a is Element of G : verum }
proof end;

theorem :: GROUP_1A:185
for G being addGroup holds Right_Cosets ((0). G) = { {a} where a is Element of G : verum }
proof end;

theorem :: GROUP_1A:186
for G being addGroup
for H being strict Subgroup of G st Left_Cosets H = { {a} where a is Element of G : verum } holds
H = (0). G
proof end;

theorem :: GROUP_1A:187
for G being addGroup
for H being strict Subgroup of G st Right_Cosets H = { {a} where a is Element of G : verum } holds
H = (0). G
proof end;

theorem Th142: :: GROUP_1A:188
for G being addGroup holds
( Left_Cosets ((Omega). G) = { the carrier of G} & Right_Cosets ((Omega). G) = { the carrier of G} )
proof end;

theorem Th143: :: GROUP_1A:189
for G being strict addGroup
for H being strict Subgroup of G st Left_Cosets H = { the carrier of G} holds
H = G
proof end;

theorem :: GROUP_1A:190
for G being strict addGroup
for H being strict Subgroup of G st Right_Cosets H = { the carrier of G} holds
H = G
proof end;

definition
let G be addGroup;
let H be Subgroup of G;
func Index H -> Cardinal equals :: GROUP_1A:def 27
card (Left_Cosets H);
correctness
coherence
card (Left_Cosets H) is Cardinal
;
;
end;

:: deftheorem defines Index GROUP_1A:def 27 :
for G being addGroup
for H being Subgroup of G holds Index H = card (Left_Cosets H);

theorem Th145: :: GROUP_1A:191
for G being addGroup
for H being Subgroup of G holds
( Index H = card (Left_Cosets H) & Index H = card (Right_Cosets H) ) by Th136, CARD_1:5;

definition
let G be addGroup;
let H be Subgroup of G;
assume A1: Left_Cosets H is finite ;
func index H -> Element of NAT means :Def18: :: GROUP_1A:def 28
ex B being finite set st
( B = Left_Cosets H & it = card B );
existence
ex b1 being Element of NAT ex B being finite set st
( B = Left_Cosets H & b1 = card B )
proof end;
uniqueness
for b1, b2 being Element of NAT st ex B being finite set st
( B = Left_Cosets H & b1 = card B ) & ex B being finite set st
( B = Left_Cosets H & b2 = card B ) holds
b1 = b2
;
end;

:: deftheorem Def18 defines index GROUP_1A:def 28 :
for G being addGroup
for H being Subgroup of G st Left_Cosets H is finite holds
for b3 being Element of NAT holds
( b3 = index H iff ex B being finite set st
( B = Left_Cosets H & b3 = card B ) );

theorem Th146: :: GROUP_1A:192
for G being addGroup
for H being Subgroup of G st Left_Cosets H is finite holds
( 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 ) )
proof end;

:: WP: Lagrange theorem for addGroups
theorem Th147: :: GROUP_1A:193
for G being finite addGroup
for H being Subgroup of G holds card G = (card H) * (index H)
proof end;

theorem :: GROUP_1A:194
for G being finite addGroup
for H being Subgroup of G holds card H divides card G
proof end;

theorem :: GROUP_1A:195
for G being finite addGroup
for I, H being Subgroup of G
for J being Subgroup of H st I = J holds
index I = (index J) * (index H)
proof end;

theorem :: GROUP_1A:196
for G being addGroup holds index ((Omega). G) = 1
proof end;

theorem :: GROUP_1A:197
for G being strict addGroup
for H being strict Subgroup of G st Left_Cosets H is finite & index H = 1 holds
H = G
proof end;

theorem :: GROUP_1A:198
for G being addGroup holds Index ((0). G) = card G
proof end;

theorem :: GROUP_1A:199
for G being finite addGroup holds index ((0). G) = card G
proof end;

theorem Th154: :: GROUP_1A:200
for G being finite addGroup
for H being strict Subgroup of G st index H = card G holds
H = (0). G
proof end;

theorem :: GROUP_1A:201
for G being addGroup
for H being strict Subgroup of G st Left_Cosets H is finite & Index H = card G holds
( G is finite & H = (0). G )
proof end;

theorem Th1: :: GROUP_1A:202
for G being addGroup
for a, b being Element of G holds
( (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 )
proof end;

Lm1: for A being Abelian addGroup
for a, b being Element of A holds a + b = b + a

;

theorem :: GROUP_1A:203
for G being addGroup holds
( G is Abelian addGroup iff the addF of G is commutative )
proof end;

theorem :: GROUP_1A:204
for G being addGroup holds (0). G is Abelian
proof end;

theorem Th4: :: GROUP_1A:205
for G being addGroup
for A, B, C, D being Subset of G st A c= B & C c= D holds
A + C c= B + D
proof end;

theorem :: GROUP_1A:206
for G being addGroup
for a being Element of G
for A, B being Subset of G st A c= B holds
( a + A c= a + B & A + a c= B + a ) by Th4;

theorem ThB6: :: GROUP_1A:207
for G being addGroup
for a being Element of G
for H1, H2 being Subgroup of G st H1 is Subgroup of H2 holds
( a + H1 c= a + H2 & H1 + a c= H2 + a )
proof end;

theorem :: GROUP_1A:208
for G being addGroup
for a being Element of G
for H being Subgroup of G holds a + H = {a} + H ;

theorem :: GROUP_1A:209
for G being addGroup
for a being Element of G
for H being Subgroup of G holds H + a = H + {a} ;

theorem Th9: :: GROUP_1A:210
for G being addGroup
for a being Element of G
for A being Subset of G
for H being Subgroup of G holds (A + a) + H = A + (a + H)
proof end;

theorem :: GROUP_1A:211
for G being addGroup
for a being Element of G
for A being Subset of G
for H being Subgroup of G holds (a + H) + A = a + (H + A)
proof end;

theorem :: GROUP_1A:212
for G being addGroup
for a being Element of G
for A being Subset of G
for H being Subgroup of G holds (A + H) + a = A + (H + a)
proof end;

theorem :: GROUP_1A:213
for G being addGroup
for a being Element of G
for A being Subset of G
for H being Subgroup of G holds (H + a) + A = H + (a + A)
proof end;

theorem :: GROUP_1A:214
for G being addGroup
for a being Element of G
for H1, H2 being Subgroup of G holds (H1 + a) + H2 = H1 + (a + H2) by Th9;

definition
let G be addGroup;
func Subgroups G -> set means :Def1: :: GROUP_1A:def 29
for x being object holds
( x in it iff x is strict Subgroup of G );
existence
ex b1 being set st
for x being object holds
( x in b1 iff x is strict Subgroup of G )
proof end;
uniqueness
for b1, b2 being set st ( for x being object holds
( x in b1 iff x is strict Subgroup of G ) ) & ( for x being object holds
( x in b2 iff x is strict Subgroup of G ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Subgroups GROUP_1A:def 29 :
for G being addGroup
for b2 being set holds
( b2 = Subgroups G iff for x being object holds
( x in b2 iff x is strict Subgroup of G ) );

registration
let G be addGroup;
cluster Subgroups G -> non empty ;
coherence
not Subgroups G is empty
proof end;
end;

theorem :: GROUP_1A:215
for G being strict addGroup holds G in Subgroups G
proof end;

theorem Th15: :: GROUP_1A:216
for G being addGroup st G is finite holds
Subgroups G is finite
proof end;

definition
let G be addGroup;
let a, b be Element of G;
func a * b -> Element of G equals :: GROUP_1A:def 30
((- b) + a) + b;
correctness
coherence
((- b) + a) + b is Element of G
;
;
end;

:: deftheorem defines * GROUP_1A:def 30 :
for G being addGroup
for a, b being Element of G holds a * b = ((- b) + a) + b;

theorem ThB16: :: GROUP_1A:217
for G being addGroup
for a, b, g being Element of G st a * g = b * g holds
a = b
proof end;

theorem Th17: :: GROUP_1A:218
for G being addGroup
for a being Element of G holds (0_ G) * a = 0_ G
proof end;

theorem ThB18: :: GROUP_1A:219
for G being addGroup
for a, b being Element of G st a * b = 0_ G holds
a = 0_ G
proof end;

theorem Th19: :: GROUP_1A:220
for G being addGroup
for a being Element of G holds a * (0_ G) = a
proof end;

theorem Th20: :: GROUP_1A:221
for G being addGroup
for a being Element of G holds a * a = a
proof end;

theorem :: GROUP_1A:222
for G being addGroup
for a being Element of G holds
( a * (- a) = a & (- a) * a = - a ) by Th1;

theorem Th22: :: GROUP_1A:223
for G being addGroup
for a, b being Element of G holds
( a * b = a iff a + b = b + a )
proof end;

theorem Th23: :: GROUP_1A:224
for G being addGroup
for a, b, g being Element of G holds (a + b) * g = (a * g) + (b * g)
proof end;

theorem Th24: :: GROUP_1A:225
for G being addGroup
for a, g, h being Element of G holds (a * g) * h = a * (g + h)
proof end;

theorem ThB25: :: GROUP_1A:226
for G being addGroup
for a, b being Element of G holds
( (a * b) * (- b) = a & (a * (- b)) * b = a )
proof end;

theorem Th26: :: GROUP_1A:227
for G being addGroup
for a, b being Element of G holds (- a) * b = - (a * b)
proof end;

Lm2: now :: thesis: for G being addGroup
for a, b being Element of G holds (0 * a) * b = 0 * (a * b)
let G be addGroup; :: thesis: for a, b being Element of G holds (0 * a) * b = 0 * (a * b)
let a, b be Element of G; :: thesis: (0 * a) * b = 0 * (a * b)
thus (0 * a) * b = (0_ G) * b by ThA24
.= 0_ G by Th17
.= 0 * (a * b) by ThA24 ; :: thesis: verum
end;

Lm3: now :: thesis: for n being Nat st ( for G being addGroup
for a, b being Element of G holds (n * a) * b = n * (a * b) ) holds
for G being addGroup
for a, b being Element of G holds ((n + 1) * a) * b = (n + 1) * (a * b)
let n be Nat; :: thesis: ( ( for G being addGroup
for a, b being Element of G holds (n * a) * b = n * (a * b) ) implies for G being addGroup
for a, b being Element of G holds ((n + 1) * a) * b = (n + 1) * (a * b) )

assume A1: for G being addGroup
for a, b being Element of G holds (n * a) * b = n * (a * b) ; :: thesis: for G being addGroup
for a, b being Element of G holds ((n + 1) * a) * b = (n + 1) * (a * b)

let G be addGroup; :: thesis: for a, b being Element of G holds ((n + 1) * a) * b = (n + 1) * (a * b)
let a, b be Element of G; :: thesis: ((n + 1) * a) * b = (n + 1) * (a * b)
thus ((n + 1) * a) * b = ((n * a) + a) * b by Th33
.= ((n * a) * b) + (a * b) by Th23
.= (n * (a * b)) + (a * b) by A1
.= (n + 1) * (a * b) by Th33 ; :: thesis: verum
end;

Lm4: for n being Nat
for G being addGroup
for a, b being Element of G holds (n * a) * b = n * (a * b)

proof end;

theorem :: GROUP_1A:228
for G being addGroup
for a, b being Element of G
for n being Nat holds (n * a) * b = n * (a * b) by Lm4;

theorem :: GROUP_1A:229
for G being addGroup
for a, b being Element of G
for i being Integer holds (i * a) * b = i * (a * b)
proof end;

theorem Th29: :: GROUP_1A:230
for G being addGroup
for a, b being Element of G st G is Abelian addGroup holds
a * b = a
proof end;

theorem ThB30: :: GROUP_1A:231
for G being addGroup st ( for a, b being Element of G holds a * b = a ) holds
G is Abelian
proof end;

definition
let G be addGroup;
let A, B be Subset of G;
func A * B -> Subset of G equals :: GROUP_1A:def 31
{ (g * h) where g, h is Element of G : ( g in A & h in B ) } ;
coherence
{ (g * h) where g, h is Element of G : ( g in A & h in B ) } is Subset of G
proof end;
end;

:: deftheorem defines * GROUP_1A:def 31 :
for G being addGroup
for A, B being Subset of G holds A * B = { (g * h) where g, h is Element of G : ( g in A & h in B ) } ;

theorem Th31: :: GROUP_1A:232
for x being set
for G being addGroup
for A, B being Subset of G holds
( x in A * B iff ex g, h being Element of G st
( x = g * h & g in A & h in B ) ) ;

theorem ThB32: :: GROUP_1A:233
for G being addGroup
for A, B being Subset of G holds
( A * B <> {} iff ( A <> {} & B <> {} ) )
proof end;

theorem ThB33: :: GROUP_1A:234
for G being addGroup
for A, B being Subset of G holds A * B c= ((- B) + A) + B
proof end;

theorem Th34: :: GROUP_1A:235
for G being addGroup
for A, B, C being Subset of G holds (A + B) * C c= (A * C) + (B * C)
proof end;

theorem Th35: :: GROUP_1A:236
for G being addGroup
for A, B, C being Subset of G holds (A * B) * C = A * (B + C)
proof end;

theorem :: GROUP_1A:237
for G being addGroup
for A, B being Subset of G holds (- A) * B = - (A * B)
proof end;

theorem ThB37: :: GROUP_1A:238
for G being addGroup
for a, b being Element of G holds {a} * {b} = {(a * b)}
proof end;

theorem :: GROUP_1A:239
for G being addGroup
for a, b, c being Element of G holds {a} * {b,c} = {(a * b),(a * c)}
proof end;

theorem :: GROUP_1A:240
for G being addGroup
for a, b, c being Element of G holds {a,b} * {c} = {(a * c),(b * c)}
proof end;

theorem :: GROUP_1A:241
for G being addGroup
for a, b, c, d being Element of G holds {a,b} * {c,d} = {(a * c),(a * d),(b * c),(b * d)}
proof end;

definition
let G be addGroup;
let A be Subset of G;
let g be Element of G;
func A * g -> Subset of G equals :: GROUP_1A:def 32
A * {g};
correctness
coherence
A * {g} is Subset of G
;
;
func g * A -> Subset of G equals :: GROUP_1A:def 33
{g} * A;
correctness
coherence
{g} * A is Subset of G
;
;
end;

:: deftheorem defines * GROUP_1A:def 32 :
for G being addGroup
for A being Subset of G
for g being Element of G holds A * g = A * {g};

:: deftheorem defines * GROUP_1A:def 33 :
for G being addGroup
for A being Subset of G
for g being Element of G holds g * A = {g} * A;

theorem Th41: :: GROUP_1A:242
for x being set
for G being addGroup
for g being Element of G
for A being Subset of G holds
( x in A * g iff ex h being Element of G st
( x = h * g & h in A ) )
proof end;

theorem ThB42: :: GROUP_1A:243
for x being set
for G being addGroup
for g being Element of G
for A being Subset of G holds
( x in g * A iff ex h being Element of G st
( x = g * h & h in A ) )
proof end;

theorem :: GROUP_1A:244
for G being addGroup
for g being Element of G
for A being Subset of G holds g * A c= ((- A) + g) + A
proof end;

theorem :: GROUP_1A:245
for G being addGroup
for g being Element of G
for A, B being Subset of G holds (A * B) * g = A * (B + g) by Th35;

theorem :: GROUP_1A:246
for G being addGroup
for g being Element of G
for A, B being Subset of G holds (A * g) * B = A * (g + B) by Th35;

theorem :: GROUP_1A:247
for G being addGroup
for g being Element of G
for A, B being Subset of G holds (g * A) * B = g * (A + B) by Th35;

theorem Th47: :: GROUP_1A:248
for G being addGroup
for a, b being Element of G
for A being Subset of G holds (A * a) * b = A * (a + b)
proof end;

theorem :: GROUP_1A:249
for G being addGroup
for a, b being Element of G
for A being Subset of G holds (a * A) * b = a * (A + b) by Th35;

theorem :: GROUP_1A:250
for G being addGroup
for a, b being Element of G
for A being Subset of G holds (a * b) * A = a * (b + A)
proof end;

theorem Th50: :: GROUP_1A:251
for G being addGroup
for g being Element of G
for A being Subset of G holds A * g = ((- g) + A) + g
proof end;

theorem :: GROUP_1A:252
for G being addGroup
for a being Element of G
for A, B being Subset of G holds (A + B) * a c= (A * a) + (B * a) by Th34;

theorem ThB52: :: GROUP_1A:253
for G being addGroup
for A being Subset of G holds A * (0_ G) = A
proof end;

theorem :: GROUP_1A:254
for G being addGroup
for A being Subset of G st A <> {} holds
(0_ G) * A = {(0_ G)}
proof end;

theorem Th54: :: GROUP_1A:255
for G being addGroup
for a being Element of G
for A being Subset of G holds
( (A * a) * (- a) = A & (A * (- a)) * a = A )
proof end;

theorem Th55: :: GROUP_1A:256
for G being addGroup holds
( G is Abelian addGroup iff for A, B being Subset of G st B <> {} holds
A * B = A )
proof end;

theorem :: GROUP_1A:257
for G being addGroup holds
( G is Abelian addGroup iff for A being Subset of G
for g being Element of G holds A * g = A )
proof end;

theorem :: GROUP_1A:258
for G being addGroup holds
( G is Abelian addGroup iff for A being Subset of G
for g being Element of G st A <> {} holds
g * A = {g} )
proof end;

definition
let G be addGroup;
let H be Subgroup of G;
let a be Element of G;
func H * a -> strict Subgroup of G means :Def6A: :: GROUP_1A:def 34
the carrier of it = (carr H) * a;
existence
ex b1 being strict Subgroup of G st the carrier of b1 = (carr H) * a
proof end;
correctness
uniqueness
for b1, b2 being strict Subgroup of G st the carrier of b1 = (carr H) * a & the carrier of b2 = (carr H) * a holds
b1 = b2
;
by Th59;
end;

:: deftheorem Def6A defines * GROUP_1A:def 34 :
for G being addGroup
for H being Subgroup of G
for a being Element of G
for b4 being strict Subgroup of G holds
( b4 = H * a iff the carrier of b4 = (carr H) * a );

theorem Th58: :: GROUP_1A:259
for x being set
for G being addGroup
for a being Element of G
for H being Subgroup of G holds
( x in H * a iff ex g being Element of G st
( x = g * a & g in H ) )
proof end;

theorem ThB59: :: GROUP_1A:260
for G being addGroup
for a being Element of G
for H being Subgroup of G holds the carrier of (H * a) = ((- a) + H) + a
proof end;

theorem Th60: :: GROUP_1A:261
for G being addGroup
for a, b being Element of G
for H being Subgroup of G holds (H * a) * b = H * (a + b)
proof end;

theorem Th61: :: GROUP_1A:262
for G being addGroup
for H being strict Subgroup of G holds H * (0_ G) = H
proof end;

theorem ThB62: :: GROUP_1A:263
for G being addGroup
for a being Element of G
for H being strict Subgroup of G holds
( (H * a) * (- a) = H & (H * (- a)) * a = H )
proof end;

theorem Th63: :: GROUP_1A:264
for G being addGroup
for a being Element of G
for H1, H2 being Subgroup of G holds (H1 /\ H2) * a = (H1 * a) /\ (H2 * a)
proof end;

theorem Th64: :: GROUP_1A:265
for G being addGroup
for a being Element of G
for H being Subgroup of G holds card H = card (H * a)
proof end;

theorem Th65: :: GROUP_1A:266
for G being addGroup
for a being Element of G
for H being Subgroup of G holds
( H is finite iff H * a is finite )
proof end;

registration
let G be addGroup;
let a be Element of G;
let H be finite Subgroup of G;
cluster H * a -> finite strict ;
coherence
H * a is finite
by Th65;
end;

theorem :: GROUP_1A:267
for G being addGroup
for a being Element of G
for H being finite Subgroup of G holds card H = card (H * a) by Th64;

theorem Th67: :: GROUP_1A:268
for G being addGroup
for a being Element of G holds ((0). G) * a = (0). G
proof end;

theorem :: GROUP_1A:269
for G being addGroup
for a being Element of G
for H being strict Subgroup of G st H * a = (0). G holds
H = (0). G
proof end;

theorem Th69: :: GROUP_1A:270
for G being addGroup
for a being Element of G holds ((Omega). G) * a = (Omega). G
proof end;

theorem :: GROUP_1A:271
for G being addGroup
for a being Element of G
for H being strict Subgroup of G st H * a = G holds
H = G
proof end;

theorem Th71: :: GROUP_1A:272
for G being addGroup
for a being Element of G
for H being Subgroup of G holds Index H = Index (H * a)
proof end;

theorem :: GROUP_1A:273
for G being addGroup
for a being Element of G
for H being Subgroup of G st Left_Cosets H is finite holds
index H = index (H * a)
proof end;

theorem Th73: :: GROUP_1A:274
for G being addGroup st G is Abelian addGroup holds
for H being strict Subgroup of G
for a being Element of G holds H * a = H
proof end;

definition
let G be addGroup;
let a, b be Element of G;
pred a,b are_conjugated means :Def7: :: GROUP_1A:def 35
ex g being Element of G st a = b * g;
end;

:: deftheorem Def7 defines are_conjugated GROUP_1A:def 35 :
for G being addGroup
for a, b being Element of G holds
( a,b are_conjugated iff ex g being Element of G st a = b * g );

notation
let G be addGroup;
let a, b be Element of G;
antonym a,b are_not_conjugated for a,b are_conjugated ;
end;

theorem Th74: :: GROUP_1A:275
for G being addGroup
for a, b being Element of G holds
( a,b are_conjugated iff ex g being Element of G st b = a * g )
proof end;

Th75: for G being addGroup
for a being Element of G holds a,a are_conjugated

proof end;

Th76: for G being addGroup
for a, b being Element of G st a,b are_conjugated holds
b,a are_conjugated

proof end;

definition
let G be addGroup;
let a, b be Element of G;
:: original: are_conjugated
redefine pred a,b are_conjugated ;
reflexivity
for a being Element of G holds (G,b1,b1)
by Th75;
symmetry
for a, b being Element of G st (G,b1,b2) holds
(G,b2,b1)
by Th76;
end;

theorem Th77: :: GROUP_1A:276
for G being addGroup
for a, b, c being Element of G st a,b are_conjugated & b,c are_conjugated holds
a,c are_conjugated
proof end;

theorem ThB78: :: GROUP_1A:277
for G being addGroup
for a being Element of G st ( a, 0_ G are_conjugated or 0_ G,a are_conjugated ) holds
a = 0_ G
proof end;

theorem Th79: :: GROUP_1A:278
for G being addGroup
for a being Element of G holds a * (carr ((Omega). G)) = { b where b is Element of G : a,b are_conjugated }
proof end;

definition
let G be addGroup;
let a be Element of G;
func con_class a -> Subset of G equals :: GROUP_1A:def 36
a * (carr ((Omega). G));
correctness
coherence
a * (carr ((Omega). G)) is Subset of G
;
;
end;

:: deftheorem defines con_class GROUP_1A:def 36 :
for G being addGroup
for a being Element of G holds con_class a = a * (carr ((Omega). G));

theorem Th80: :: GROUP_1A:279
for x being set
for G being addGroup
for a being Element of G holds
( x in con_class a iff ex b being Element of G st
( b = x & a,b are_conjugated ) )
proof end;

theorem Th81: :: GROUP_1A:280
for G being addGroup
for a, b being Element of G holds
( a in con_class b iff a,b are_conjugated )
proof end;

theorem :: GROUP_1A:281
for G being addGroup
for a, g being Element of G holds a * g in con_class a by Th80, Th74;

theorem :: GROUP_1A:282
for G being addGroup
for a being Element of G holds a in con_class a by Th81;

theorem :: GROUP_1A:283
for G being addGroup
for a, b being Element of G st a in con_class b holds
b in con_class a
proof end;

theorem :: GROUP_1A:284
for G being addGroup
for a, b being Element of G holds
( con_class a = con_class b iff con_class a meets con_class b )
proof end;

theorem :: GROUP_1A:285
for G being addGroup
for a being Element of G holds
( con_class a = {(0_ G)} iff a = 0_ G )
proof end;

theorem :: GROUP_1A:286
for G being addGroup
for a being Element of G
for A being Subset of G holds (con_class a) + A = A + (con_class a)
proof end;

definition
let G be addGroup;
let A, B be Subset of G;
pred A,B are_conjugated means :: GROUP_1A:def 37
ex g being Element of G st A = B * g;
end;

:: deftheorem defines are_conjugated GROUP_1A:def 37 :
for G being addGroup
for A, B being Subset of G holds
( A,B are_conjugated iff ex g being Element of G st A = B * g );

notation
let G be addGroup;
let A, B be Subset of G;
antonym A,B are_not_conjugated for A,B are_conjugated ;
end;

theorem Th88: :: GROUP_1A:287
for G being addGroup
for A, B being Subset of G holds
( A,B are_conjugated iff ex g being Element of G st B = A * g )
proof end;

theorem Th89: :: GROUP_1A:288
for G being addGroup
for A being Subset of G holds A,A are_conjugated
proof end;

theorem Th90: :: GROUP_1A:289
for G being addGroup
for A, B being Subset of G st A,B are_conjugated holds
B,A are_conjugated
proof end;

definition
let G be addGroup;
let A, B be Subset of G;
:: original: are_conjugated
redefine pred A,B are_conjugated ;
reflexivity
for A being Subset of G holds (G,b1,b1)
by Th89;
symmetry
for A, B being Subset of G st (G,b1,b2) holds
(G,b2,b1)
by Th90;
end;

theorem Th91: :: GROUP_1A:290
for G being addGroup
for A, B, C being Subset of G st A,B are_conjugated & B,C are_conjugated holds
A,C are_conjugated
proof end;

theorem Th92: :: GROUP_1A:291
for G being addGroup
for a, b being Element of G holds
( {a},{b} are_conjugated iff a,b are_conjugated )
proof end;

theorem Th93: :: GROUP_1A:292
for G being addGroup
for A being Subset of G
for H1 being Subgroup of G st A, carr H1 are_conjugated holds
ex H2 being strict Subgroup of G st the carrier of H2 = A
proof end;

definition
let G be addGroup;
let A be Subset of G;
func con_class A -> Subset-Family of G equals :: GROUP_1A:def 38
{ B where B is Subset of G : A,B are_conjugated } ;
coherence
{ B where B is Subset of G : A,B are_conjugated } is Subset-Family of G
proof end;
end;

:: deftheorem defines con_class GROUP_1A:def 38 :
for G being addGroup
for A being Subset of G holds con_class A = { B where B is Subset of G : A,B are_conjugated } ;

theorem :: GROUP_1A:293
for x being set
for G being addGroup
for A being Subset of G holds
( x in con_class A iff ex B being Subset of G st
( x = B & A,B are_conjugated ) ) ;

theorem Th95: :: GROUP_1A:294
for G being addGroup
for A, B being Subset of G holds
( A in con_class B iff A,B are_conjugated )
proof end;

theorem :: GROUP_1A:295
for G being addGroup
for g being Element of G
for A being Subset of G holds A * g in con_class A
proof end;

theorem :: GROUP_1A:296
for G being addGroup
for A being Subset of G holds A in con_class A ;

theorem :: GROUP_1A:297
for G being addGroup
for A, B being Subset of G st A in con_class B holds
B in con_class A
proof end;

theorem :: GROUP_1A:298
for G being addGroup
for A, B being Subset of G holds
( con_class A = con_class B iff con_class A meets con_class B )
proof end;

theorem Th100: :: GROUP_1A:299
for G being addGroup
for a being Element of G holds con_class {a} = { {b} where b is Element of G : b in con_class a }
proof end;

theorem :: GROUP_1A:300
for G being addGroup
for A being Subset of G st G is finite holds
con_class A is finite ;

definition
let G be addGroup;
let H1, H2 be Subgroup of G;
pred H1,H2 are_conjugated means :: GROUP_1A:def 39
ex g being Element of G st addMagma(# the carrier of H1, the addF of H1 #) = H2 * g;
end;

:: deftheorem defines are_conjugated GROUP_1A:def 39 :
for G being addGroup
for H1, H2 being Subgroup of G holds
( H1,H2 are_conjugated iff ex g being Element of G st addMagma(# the carrier of H1, the addF of H1 #) = H2 * g );

notation
let G be addGroup;
let H1, H2 be Subgroup of G;
antonym H1,H2 are_not_conjugated for H1,H2 are_conjugated ;
end;

theorem Th102: :: GROUP_1A:301
for G being addGroup
for H1, H2 being strict Subgroup of G holds
( H1,H2 are_conjugated iff ex g being Element of G st H2 = H1 * g )
proof end;

theorem ThB103: :: GROUP_1A:302
for G being addGroup
for H1 being strict Subgroup of G holds H1,H1 are_conjugated
proof end;

theorem ThB104: :: GROUP_1A:303
for G being addGroup
for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated holds
H2,H1 are_conjugated
proof end;

definition
let G be addGroup;
let H1, H2 be strict Subgroup of G;
:: original: are_conjugated
redefine pred H1,H2 are_conjugated ;
reflexivity
for H1 being strict Subgroup of G holds (G,b1,b1)
by ThB103;
symmetry
for H1, H2 being strict Subgroup of G st (G,b1,b2) holds
(G,b2,b1)
by ThB104;
end;

theorem Th105: :: GROUP_1A:304
for G being addGroup
for H3 being Subgroup of G
for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated & H2,H3 are_conjugated holds
H1,H3 are_conjugated
proof end;

definition
let G be addGroup;
let H be Subgroup of G;
func con_class H -> Subset of (Subgroups G) means :Def12: :: 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 ) );
existence
ex b1 being Subset of (Subgroups G) st
for x being object holds
( x in b1 iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) )
proof end;
uniqueness
for b1, b2 being Subset of (Subgroups G) st ( for x being object holds
( x in b1 iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) ) ) & ( for x being object holds
( x in b2 iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines con_class GROUP_1A:def 40 :
for G being addGroup
for H being Subgroup of G
for b3 being Subset of (Subgroups G) holds
( b3 = con_class H iff for x being object holds
( x in b3 iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) ) );

theorem Th106: :: GROUP_1A:305
for x being set
for G being addGroup
for H being Subgroup of G st x in con_class H holds
x is strict Subgroup of G
proof end;

theorem Th107: :: GROUP_1A:306
for G being addGroup
for H1, H2 being strict Subgroup of G holds
( H1 in con_class H2 iff H1,H2 are_conjugated )
proof end;

theorem Th108: :: GROUP_1A:307
for G being addGroup
for g being Element of G
for H being strict Subgroup of G holds H * g in con_class H
proof end;

theorem Th109: :: GROUP_1A:308
for G being addGroup
for H being strict Subgroup of G holds H in con_class H
proof end;

theorem :: GROUP_1A:309
for G being addGroup
for H1, H2 being strict Subgroup of G st H1 in con_class H2 holds
H2 in con_class H1
proof end;

theorem :: GROUP_1A:310
for G being addGroup
for H1, H2 being strict Subgroup of G holds
( con_class H1 = con_class H2 iff con_class H1 meets con_class H2 )
proof end;

theorem :: GROUP_1A:311
for G being addGroup
for H being Subgroup of G st G is finite holds
con_class H is finite by Th15, FINSET_1:1;

theorem ThB113: :: GROUP_1A:312
for G being addGroup
for H2 being Subgroup of G
for H1 being strict Subgroup of G holds
( H1,H2 are_conjugated iff carr H1, carr H2 are_conjugated )
proof end;

definition
let G be addGroup;
let IT be Subgroup of G;
attr IT is normal means :Def13: :: GROUP_1A:def 41
for a being Element of G holds IT * a = addMagma(# the carrier of IT, the addF of IT #);
end;

:: deftheorem Def13 defines normal GROUP_1A:def 41 :
for G being addGroup
for IT being Subgroup of G holds
( IT is normal iff for a being Element of G holds IT * a = addMagma(# the carrier of IT, the addF of IT #) );

registration
let G be addGroup;
cluster non empty strict add-associative add-unital addGroup-like normal for Subgroup of G;
existence
ex b1 being Subgroup of G st
( b1 is strict & b1 is normal )
proof end;
end;

theorem Th114: :: GROUP_1A:313
for G being addGroup holds
( (0). G is normal & (Omega). G is normal ) by Th67, Th69;

theorem :: GROUP_1A:314
for G being addGroup
for N1, N2 being strict normal Subgroup of G holds N1 /\ N2 is normal
proof end;

theorem :: GROUP_1A:315
for G being addGroup
for H being strict Subgroup of G st G is Abelian addGroup holds
H is normal by Th73;

theorem Th117: :: GROUP_1A:316
for G being addGroup
for H being Subgroup of G holds
( H is normal Subgroup of G iff for a being Element of G holds a + H = H + a )
proof end;

theorem Th118: :: GROUP_1A:317
for G being addGroup
for H being Subgroup of G holds
( H is normal Subgroup of G iff for a being Element of G holds a + H c= H + a )
proof end;

theorem ThB119: :: GROUP_1A:318
for G being addGroup
for H being Subgroup of G holds
( H is normal Subgroup of G iff for a being Element of G holds H + a c= a + H )
proof end;

theorem :: GROUP_1A:319
for G being addGroup
for H being Subgroup of G holds
( H is normal Subgroup of G iff for A being Subset of G holds A + H = H + A )
proof end;

theorem :: GROUP_1A:320
for G being addGroup
for H being strict Subgroup of G holds
( H is normal Subgroup of G iff for a being Element of G holds H is Subgroup of H * a )
proof end;

theorem :: GROUP_1A:321
for G being addGroup
for H being strict Subgroup of G holds
( H is normal Subgroup of G iff for a being Element of G holds H * a is Subgroup of H )
proof end;

theorem :: GROUP_1A:322
for G being addGroup
for H being strict Subgroup of G holds
( H is normal Subgroup of G iff con_class H = {H} )
proof end;

theorem :: GROUP_1A:323
for G being addGroup
for H being strict Subgroup of G holds
( H is normal Subgroup of G iff for a being Element of G st a in H holds
con_class a c= carr H )
proof end;

Lm5: for G being addGroup
for N2 being normal Subgroup of G
for N1 being strict normal Subgroup of G holds (carr N1) + (carr N2) c= (carr N2) + (carr N1)

proof end;

theorem :: GROUP_1A:324
for G being addGroup
for N1, N2 being strict normal Subgroup of G holds (carr N1) + (carr N2) = (carr N2) + (carr N1) by Lm5;

theorem :: GROUP_1A:325
for G being addGroup
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)
proof end;

theorem :: GROUP_1A:326
for G being addGroup
for N being normal Subgroup of G holds Left_Cosets N = Right_Cosets N
proof end;

theorem :: GROUP_1A:327
for G being addGroup
for H being Subgroup of G st Left_Cosets H is finite & index H = 2 holds
H is normal Subgroup of G
proof end;

definition
let G be addGroup;
let A be Subset of G;
func Normalizer A -> strict Subgroup of G means :Def14: :: GROUP_1A:def 42
the carrier of it = { h where h is Element of G : A * h = A } ;
existence
ex b1 being strict Subgroup of G st the carrier of b1 = { h where h is Element of G : A * h = A }
proof end;
uniqueness
for b1, b2 being strict Subgroup of G st the carrier of b1 = { h where h is Element of G : A * h = A } & the carrier of b2 = { h where h is Element of G : A * h = A } holds
b1 = b2
by Th59;
end;

:: deftheorem Def14 defines Normalizer GROUP_1A:def 42 :
for G being addGroup
for A being Subset of G
for b3 being strict Subgroup of G holds
( b3 = Normalizer A iff the carrier of b3 = { h where h is Element of G : A * h = A } );

theorem Th129: :: GROUP_1A:328
for x being set
for G being addGroup
for A being Subset of G holds
( x in Normalizer A iff ex h being Element of G st
( x = h & A * h = A ) )
proof end;

theorem Th130: :: GROUP_1A:329
for G being addGroup
for A being Subset of G holds card (con_class A) = Index (Normalizer A)
proof end;

theorem :: GROUP_1A:330
for G being addGroup
for A being Subset of G st ( con_class A is finite or Left_Cosets (Normalizer A) is finite ) holds
ex C being finite set st
( C = con_class A & card C = index (Normalizer A) )
proof end;

theorem Th132: :: GROUP_1A:331
for G being addGroup
for a being Element of G holds card (con_class a) = Index (Normalizer {a})
proof end;

theorem :: GROUP_1A:332
for G being addGroup
for a being Element of G st ( con_class a is finite or Left_Cosets (Normalizer {a}) is finite ) holds
ex C being finite set st
( C = con_class a & card C = index (Normalizer {a}) )
proof end;

definition
let G be addGroup;
let H be Subgroup of G;
func Normalizer H -> strict Subgroup of G equals :: GROUP_1A:def 43
Normalizer (carr H);
correctness
coherence
Normalizer (carr H) is strict Subgroup of G
;
;
end;

:: deftheorem defines Normalizer GROUP_1A:def 43 :
for G being addGroup
for H being Subgroup of G holds Normalizer H = Normalizer (carr H);

theorem Th134: :: GROUP_1A:333
for x being set
for G being addGroup
for H being strict Subgroup of G holds
( x in Normalizer H iff ex h being Element of G st
( x = h & H * h = H ) )
proof end;

theorem Th135: :: GROUP_1A:334
for G being addGroup
for H being strict Subgroup of G holds card (con_class H) = Index (Normalizer H)
proof end;

theorem :: GROUP_1A:335
for G being addGroup
for H being strict Subgroup of G st ( con_class H is finite or Left_Cosets (Normalizer H) is finite ) holds
ex C being finite set st
( C = con_class H & card C = index (Normalizer H) )
proof end;

theorem Th137: :: GROUP_1A:336
for G being strict addGroup
for H being strict Subgroup of G holds
( H is normal Subgroup of G iff Normalizer H = G )
proof end;

theorem :: GROUP_1A:337
for G being strict addGroup holds Normalizer ((0). G) = G
proof end;

theorem :: GROUP_1A:338
for G being strict addGroup holds Normalizer ((Omega). G) = G
proof end;

theorem Th4: :: GROUP_1A:339
for H being non empty addMagma
for P, Q, P1, Q1 being Subset of H st P c= P1 & Q c= Q1 holds
P + Q c= P1 + Q1
proof end;

theorem Th5: :: GROUP_1A:340
for H being non empty addMagma
for P, Q being Subset of H
for h being Element of H st P c= Q holds
P + h c= Q + h
proof end;

theorem :: GROUP_1A:341
for H being non empty addMagma
for P, Q being Subset of H
for h being Element of H st P c= Q holds
h + P c= h + Q
proof end;

theorem Th7: :: GROUP_1A:342
for G being addGroup
for A being Subset of G
for a being Element of G holds
( a in - A iff - a in A )
proof end;

Lm1: for G being addGroup
for A, B being Subset of G st A c= B holds
- A c= - B

proof end;

theorem ThB8: :: GROUP_1A:343
for G being addGroup
for A, B being Subset of G holds
( A c= B iff - A c= - B )
proof end;

theorem Th9: :: GROUP_1A:344
for G being addGroup
for A being Subset of G holds (add_inverse G) .: A = - A
proof end;

theorem Th10: :: GROUP_1A:345
for G being addGroup
for A being Subset of G holds (add_inverse G) " A = - A
proof end;

theorem Th11: :: GROUP_1A:346
for G being addGroup holds add_inverse G is one-to-one
proof end;

theorem Th12: :: GROUP_1A:347
for G being addGroup holds rng (add_inverse G) = the carrier of G
proof end;

registration
let G be addGroup;
cluster add_inverse G -> one-to-one onto ;
coherence
( add_inverse G is one-to-one & add_inverse G is onto )
by Th11, Th12;
end;

theorem Th13: :: GROUP_1A:348
for G being addGroup holds (add_inverse G) " = add_inverse G
proof end;

theorem Th14: :: GROUP_1A:349
for H being non empty addMagma
for P, Q being Subset of H holds the addF of H .: [:P,Q:] = P + Q
proof end;

definition
let G be non empty addMagma ;
let a be Element of G;
func a + -> Function of G,G means :Def1: :: GROUP_1A:def 44
for x being Element of G holds it . x = a + x;
existence
ex b1 being Function of G,G st
for x being Element of G holds b1 . x = a + x
proof end;
uniqueness
for b1, b2 being Function of G,G st ( for x being Element of G holds b1 . x = a + x ) & ( for x being Element of G holds b2 . x = a + x ) holds
b1 = b2
proof end;
func + a -> Function of G,G means :Def2: :: GROUP_1A:def 45
for x being Element of G holds it . x = x + a;
existence
ex b1 being Function of G,G st
for x being Element of G holds b1 . x = x + a
proof end;
uniqueness
for b1, b2 being Function of G,G st ( for x being Element of G holds b1 . x = x + a ) & ( for x being Element of G holds b2 . x = x + a ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines + GROUP_1A:def 44 :
for G being non empty addMagma
for a being Element of G
for b3 being Function of G,G holds
( b3 = a + iff for x being Element of G holds b3 . x = a + x );

:: deftheorem Def2 defines + GROUP_1A:def 45 :
for G being non empty addMagma
for a being Element of G
for b3 being Function of G,G holds
( b3 = + a iff for x being Element of G holds b3 . x = x + a );

registration
let G be addGroup;
let a be Element of G;
cluster a + -> one-to-one onto ;
coherence
( a + is one-to-one & a + is onto )
proof end;
cluster + a -> one-to-one onto ;
coherence
( + a is one-to-one & + a is onto )
proof end;
end;

theorem Th15: :: GROUP_1A:350
for H being non empty addMagma
for P being Subset of H
for h being Element of H holds (h +) .: P = h + P
proof end;

theorem Th16: :: GROUP_1A:351
for H being non empty addMagma
for P being Subset of H
for h being Element of H holds (+ h) .: P = P + h
proof end;

theorem Th17: :: GROUP_1A:352
for G being addGroup
for a being Element of G holds (a +) /" = (- a) +
proof end;

theorem Th18: :: GROUP_1A:353
for G being addGroup
for a being Element of G holds (+ a) /" = + (- a)
proof end;

:: On the topological groups
definition
attr c1 is strict ;
struct TopaddGrStr -> addMagma , TopStruct ;
aggr TopaddGrStr(# carrier, addF, topology #) -> TopaddGrStr ;
end;

registration
let A be non empty set ;
let R be BinOp of A;
let T be Subset-Family of A;
cluster TopaddGrStr(# A,R,T #) -> non empty ;
coherence
not TopaddGrStr(# A,R,T #) is empty
;
end;

registration
let x be set ;
let R be BinOp of {x};
let T be Subset-Family of {x};
cluster TopaddGrStr(# {x},R,T #) -> trivial ;
coherence
TopaddGrStr(# {x},R,T #) is trivial
;
end;

registration
cluster 1 -element -> 1 -element Abelian add-associative addGroup-like for addMagma ;
coherence
for b1 being 1 -element addMagma holds
( b1 is addGroup-like & b1 is add-associative & b1 is Abelian )
proof end;
end;

registration
cluster non empty strict for TopaddGrStr ;
existence
ex b1 being TopaddGrStr st
( b1 is strict & not b1 is empty )
proof end;
end;

registration
cluster 1 -element TopSpace-like strict for TopaddGrStr ;
existence
ex b1 being TopaddGrStr st
( b1 is strict & b1 is TopSpace-like & b1 is 1 -element )
proof end;
end;

definition
let G be non empty add-associative addGroup-like TopaddGrStr ;
attr G is UnContinuous means :Def7: :: GROUP_1A:def 46
add_inverse G is continuous ;
end;

:: deftheorem Def7 defines UnContinuous GROUP_1A:def 46 :
for G being non empty add-associative addGroup-like TopaddGrStr holds
( G is UnContinuous iff add_inverse G is continuous );

definition
let G be TopSpace-like TopaddGrStr ;
attr G is BinContinuous means :Def8: :: GROUP_1A:def 47
for f being Function of [:G,G:],G st f = the addF of G holds
f is continuous ;
end;

:: deftheorem Def8 defines BinContinuous GROUP_1A:def 47 :
for G being TopSpace-like TopaddGrStr holds
( G is BinContinuous iff for f being Function of [:G,G:],G st f = the addF of G holds
f is continuous );

registration
cluster non empty trivial finite 1 -element Abelian add-associative TopSpace-like compact homogeneous add-unital addGroup-like strict UnContinuous BinContinuous for TopaddGrStr ;
existence
ex b1 being 1 -element add-associative TopSpace-like addGroup-like TopaddGrStr st
( b1 is strict & b1 is Abelian & b1 is UnContinuous & b1 is BinContinuous )
proof end;
end;

definition
mode TopaddGroup is non empty add-associative TopSpace-like addGroup-like TopaddGrStr ;
end;

definition
mode TopologicaladdGroup is UnContinuous BinContinuous TopaddGroup;
end;

theorem Th36: :: GROUP_1A:354
for T being non empty TopSpace-like BinContinuous TopaddGrStr
for a, b being Element of T
for W being a_neighborhood of a + b ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A + B c= W
proof end;

theorem ThW37: :: GROUP_1A:355
for T being non empty TopSpace-like TopaddGrStr st ( for a, b being Element of T
for W being a_neighborhood of a + b ex A being a_neighborhood of a ex B being a_neighborhood of b st A + B c= W ) holds
T is BinContinuous
proof end;

theorem Th38: :: GROUP_1A:356
for T being UnContinuous TopaddGroup
for a being Element of T
for W being a_neighborhood of - a ex A being open a_neighborhood of a st - A c= W
proof end;

theorem Th39: :: GROUP_1A:357
for T being TopaddGroup st ( for a being Element of T
for W being a_neighborhood of - a ex A being a_neighborhood of a st - A c= W ) holds
T is UnContinuous
proof end;

theorem Th40: :: GROUP_1A:358
for T being TopologicaladdGroup
for a, b being Element of T
for W being a_neighborhood of a + (- b) ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A + (- B) c= W
proof end;

theorem :: GROUP_1A:359
for T being TopaddGroup st ( for a, b being Element of T
for W being a_neighborhood of a + (- b) ex A being a_neighborhood of a ex B being a_neighborhood of b st A + (- B) c= W ) holds
T is TopologicaladdGroup
proof end;

registration
let G be non empty TopSpace-like BinContinuous TopaddGrStr ;
let a be Element of G;
cluster a + -> continuous ;
coherence
a + is continuous
proof end;
cluster + a -> continuous ;
coherence
+ a is continuous
proof end;
end;

theorem Th42: :: GROUP_1A:360
for G being BinContinuous TopaddGroup
for a being Element of G holds a + is Homeomorphism of G
proof end;

theorem Th43: :: GROUP_1A:361
for G being BinContinuous TopaddGroup
for a being Element of G holds + a is Homeomorphism of G
proof end;

definition
let G be BinContinuous TopaddGroup;
let a be Element of G;
:: original: +
redefine func a + -> Homeomorphism of G;
coherence
a + is Homeomorphism of G
by Th42;
:: original: +
redefine func + a -> Homeomorphism of G;
coherence
+ a is Homeomorphism of G
by Th43;
end;

theorem Th44: :: GROUP_1A:362
for G being UnContinuous TopaddGroup holds add_inverse G is Homeomorphism of G
proof end;

definition
let G be UnContinuous TopaddGroup;
:: original: add_inverse
redefine func add_inverse G -> Homeomorphism of G;
coherence
add_inverse G is Homeomorphism of G
by Th44;
end;

registration
cluster non empty add-associative TopSpace-like addGroup-like BinContinuous -> homogeneous for TopaddGrStr ;
coherence
for b1 being TopaddGroup st b1 is BinContinuous holds
b1 is homogeneous
proof end;
end;

theorem Th45: :: GROUP_1A:363
for G being BinContinuous TopaddGroup
for F being closed Subset of G
for a being Element of G holds F + a is closed
proof end;

theorem Th46: :: GROUP_1A:364
for G being BinContinuous TopaddGroup
for F being closed Subset of G
for a being Element of G holds a + F is closed
proof end;

registration
let G be BinContinuous TopaddGroup;
let F be closed Subset of G;
let a be Element of G;
cluster F + a -> closed ;
coherence
F + a is closed
by Th45;
cluster a + F -> closed ;
coherence
a + F is closed
by Th46;
end;

theorem Th47: :: GROUP_1A:365
for G being UnContinuous TopaddGroup
for F being closed Subset of G holds - F is closed
proof end;

registration
let G be UnContinuous TopaddGroup;
let F be closed Subset of G;
cluster - F -> closed ;
coherence
- F is closed
by Th47;
end;

theorem Th48: :: GROUP_1A:366
for G being BinContinuous TopaddGroup
for O being open Subset of G
for a being Element of G holds O + a is open
proof end;

theorem Th49: :: GROUP_1A:367
for G being BinContinuous TopaddGroup
for O being open Subset of G
for a being Element of G holds a + O is open
proof end;

registration
let G be BinContinuous TopaddGroup;
let A be open Subset of G;
let a be Element of G;
cluster A + a -> open ;
coherence
A + a is open
by Th48;
cluster a + A -> open ;
coherence
a + A is open
by Th49;
end;

theorem Th50: :: GROUP_1A:368
for G being UnContinuous TopaddGroup
for O being open Subset of G holds - O is open
proof end;

registration
let G be UnContinuous TopaddGroup;
let A be open Subset of G;
cluster - A -> open ;
coherence
- A is open
by Th50;
end;

theorem Th51: :: GROUP_1A:369
for G being BinContinuous TopaddGroup
for A, O being Subset of G st O is open holds
O + A is open
proof end;

theorem Th52: :: GROUP_1A:370
for G being BinContinuous TopaddGroup
for A, O being Subset of G st O is open holds
A + O is open
proof end;

registration
let G be BinContinuous TopaddGroup;
let A be open Subset of G;
let B be Subset of G;
cluster A + B -> open ;
coherence
A + B is open
by Th51;
cluster B + A -> open ;
coherence
B + A is open
by Th52;
end;

theorem Th53: :: GROUP_1A:371
for G being UnContinuous TopaddGroup
for a being Point of G
for A being a_neighborhood of a holds - A is a_neighborhood of - a
proof end;

theorem Th54: :: GROUP_1A:372
for G being TopologicaladdGroup
for a being Point of G
for A being a_neighborhood of a + (- a) ex B being open a_neighborhood of a st B + (- B) c= A
proof end;

theorem Th55: :: GROUP_1A:373
for G being UnContinuous TopaddGroup
for A being dense Subset of G holds - A is dense
proof end;

registration
let G be UnContinuous TopaddGroup;
let A be dense Subset of G;
cluster - A -> dense ;
coherence
- A is dense
by Th55;
end;

theorem Th56: :: GROUP_1A:374
for G being BinContinuous TopaddGroup
for A being dense Subset of G
for a being Point of G holds a + A is dense
proof end;

theorem Th57: :: GROUP_1A:375
for G being BinContinuous TopaddGroup
for A being dense Subset of G
for a being Point of G holds A + a is dense
proof end;

registration
let G be BinContinuous TopaddGroup;
let A be dense Subset of G;
let a be Point of G;
cluster A + a -> dense ;
coherence
A + a is dense
by Th57;
cluster a + A -> dense ;
coherence
a + A is dense
by Th56;
end;

theorem :: GROUP_1A:376
for G being TopologicaladdGroup
for B being Basis of 0_ G
for 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
proof end;

Th59: for G being TopologicaladdGroup holds G is regular
proof end;

registration
cluster non empty add-associative TopSpace-like addGroup-like UnContinuous BinContinuous -> regular for TopaddGrStr ;
coherence
for b1 being TopologicaladdGroup holds b1 is regular
by Th59;
end;