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

scheme :: GROUP_1A:sch 1
SeqEx2Dbis{ F₁() -> non empty set , F₂() -> non empty set , P₁[ set , set , set ] } :

ex f being Function of [:NAT,F₁():],F₂() st
for x being Nat
for y being Element of F₁() holds P₁[x,y,f . (x,y)]

provided

A1: for x being Nat
for y being Element of F₁() ex z being Element of F₂() st P₁[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 b₁ being addMagma st b₁ is addGroup-like holds
b₁ is add-unital ;

end;

registration

cluster non empty strict add-associative addGroup-like for addMagma ;

existence
ex b₁ being addMagma st
( b₁ is strict & b₁ is addGroup-like & b₁ is add-associative & not b₁ 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 b₁ being Element of G st
for h being Element of G holds
( h + b₁ = h & b₁ + h = h ) by A1;
uniqueness
for b₁, b₂ being Element of G st ( for h being Element of G holds
( h + b₁ = h & b₁ + h = h ) ) & ( for h being Element of G holds
( h + b₂ = h & b₂ + h = h ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines 0_ GROUP_1A:def 3 :
for G being addMagma st G is add-unital holds
for b₂ being Element of G holds
( b₂ = 0_ G iff for h being Element of G holds
( h + b₂ = h & b₂ + 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 b₁ being Element of G st
( h + b₁ = 0_ G & b₁ + h = 0_ G )

proof end;

uniqueness
for b₁, b₂ being Element of G st h + b₁ = 0_ G & b₁ + h = 0_ G & h + b₂ = 0_ G & b₂ + h = 0_ G holds
b₁ = b₂

proof end;

involutiveness
for b₁, b₂ being Element of G st b₂ + b₁ = 0_ G & b₁ + b₂ = 0_ G holds
( b₁ + b₂ = 0_ G & b₂ + b₁ = 0_ G ) ;

end;

:: deftheorem Def5 defines - GROUP_1A:def 4 :
for G being addGroup
for h, b₃ being Element of G holds
( b₃ = - h iff ( h + b₃ = 0_ G & b₃ + 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 b₁ being UnOp of G st
for h being Element of G holds b₁ . h = - h

proof end;

uniqueness
for b₁, b₂ being UnOp of G st ( for h being Element of G holds b₁ . h = - h ) & ( for h being Element of G holds b₂ . h = - h ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines add_inverse GROUP_1A:def 5 :
for G being addGroup
for b₂ being UnOp of G holds
( b₂ = add_inverse G iff for h being Element of G holds b₂ . 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 b₁ being Function of [:NAT, the carrier of G:], the carrier of G st
for h being Element of G holds
( b₁ . (0,h) = 0_ G & ( for n being Nat holds b₁ . ((n + 1),h) = (b₁ . (n,h)) + h ) )

proof end;

uniqueness
for b₁, b₂ being Function of [:NAT, the carrier of G:], the carrier of G st ( for h being Element of G holds
( b₁ . (0,h) = 0_ G & ( for n being Nat holds b₁ . ((n + 1),h) = (b₁ . (n,h)) + h ) ) ) & ( for h being Element of G holds
( b₂ . (0,h) = 0_ G & ( for n being Nat holds b₂ . ((n + 1),h) = (b₂ . (n,h)) + h ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines mult GROUP_1A:def 6 :
for G being non empty addMagma
for b₂ being Function of [:NAT, the carrier of G:], the carrier of G holds
( b₂ = mult G iff for h being Element of G holds
( b₂ . (0,h) = 0_ G & ( for n being Nat holds b₂ . ((n + 1),h) = (b₂ . (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 b₁ 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 b₁ being Element of G holds
( b₁ = n * h iff b₁ = (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 b₁ being Element of NAT st b₁ = 0 ) & ( not h is being_of_order_0 implies ex b₁ being Element of NAT st
( b₁ * h = 0_ G & b₁ <> 0 & ( for m being Nat st m * h = 0_ G & m <> 0 holds
b₁ <= m ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT holds
( ( h is being_of_order_0 & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) & ( not h is being_of_order_0 & b₁ * h = 0_ G & b₁ <> 0 & ( for m being Nat st m * h = 0_ G & m <> 0 holds
b₁ <= m ) & b₂ * h = 0_ G & b₂ <> 0 & ( for m being Nat st m * h = 0_ G & m <> 0 holds
b₂ <= m ) implies b₁ = b₂ ) )

proof end;

correctness
consistency
for b₁ 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 b₃ being Element of NAT holds
( ( h is being_of_order_0 implies ( b₃ = ord h iff b₃ = 0 ) ) & ( not h is being_of_order_0 implies ( b₃ = ord h iff ( b₃ * h = 0_ G & b₃ <> 0 & ( for m being Nat st m * h = 0_ G & m <> 0 holds
b₃ <= 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 b₁ being addGroup st
( b₁ is strict & b₁ 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 b₁, b₂ being Subset of G st b₁ = { (- g) where g is Element of G : g in b₂ } holds
b₂ = { (- g) where g is Element of G : g in b₁ }

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 b₁ being non empty addGroup-like addMagma st
( the carrier of b₁ c= the carrier of G & the addF of b₁ = the addF of G || the carrier of b₁ )

proof end;

end;

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

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 b₁ being Subgroup of G holds b₁ 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 b₁ being Subgroup of G st b₁ 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 b₁ being Subgroup of G holds b₁ 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 b₁ being strict Subgroup of G st the carrier of b₁ = {(0_ G)}

proof end;

uniqueness
for b₁, b₂ being strict Subgroup of G st the carrier of b₁ = {(0_ G)} & the carrier of b₂ = {(0_ G)} holds
b₁ = b₂ by Th59;

end;

:: deftheorem Def7 defines (0). GROUP_1A:def 17 :
for G being addGroup
for b₂ being strict Subgroup of G holds
( b₂ = (0). G iff the carrier of b₂ = {(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 b₁ being strict Subgroup of G
for b₂ being addGroup st b₁ = addMagma(# the carrier of b₂, the addF of b₂ #) holds
b₁ = addMagma(# the carrier of b₁, the addF of b₁ #) ;

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 b₁ being Subgroup of G st
( b₁ is strict & b₁ is finite )

proof end;

end;

registration

cluster non empty finite strict add-associative add-unital addGroup-like for addMagma ;

existence
ex b₁ being addGroup st
( b₁ is strict & b₁ is finite )

proof end;

end;

registration

let G be finite addGroup;

cluster -> finite for Subgroup of G;

coherence
for b₁ being Subgroup of G holds b₁ 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 b₁ being strict Subgroup of G st the carrier of b₁ = (carr H1) /\ (carr H2)

proof end;

uniqueness
for b₁, b₂ being strict Subgroup of G st the carrier of b₁ = (carr H1) /\ (carr H2) & the carrier of b₂ = (carr H1) /\ (carr H2) holds
b₁ = b₂ by Th59;

end;

:: deftheorem Def10 defines /\ GROUP_1A:def 20 :
for G being addGroup
for H1, H2 being Subgroup of G
for b₄ being strict Subgroup of G holds
( b₄ = H1 /\ H2 iff the carrier of b₄ = (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 b₁ being Subset-Family of G st
for A being Subset of G holds
( A in b₁ iff ex a being Element of G st A = a + H )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of G st ( for A being Subset of G holds
( A in b₁ iff ex a being Element of G st A = a + H ) ) & ( for A being Subset of G holds
( A in b₂ iff ex a being Element of G st A = a + H ) ) holds
b₁ = b₂

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 b₁ being Subset-Family of G st
for A being Subset of G holds
( A in b₁ iff ex a being Element of G st A = H + a )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of G st ( for A being Subset of G holds
( A in b₁ iff ex a being Element of G st A = H + a ) ) & ( for A being Subset of G holds
( A in b₂ iff ex a being Element of G st A = H + a ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def15 defines Left_Cosets GROUP_1A:def 25 :
for G being addGroup
for H being Subgroup of G
for b₃ being Subset-Family of G holds
( b₃ = Left_Cosets H iff for A being Subset of G holds
( A in b₃ 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 b₃ being Subset-Family of G holds
( b₃ = Right_Cosets H iff for A being Subset of G holds
( A in b₃ 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 b₁ being Element of NAT ex B being finite set st
( B = Left_Cosets H & b₁ = card B )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st ex B being finite set st
( B = Left_Cosets H & b₁ = card B ) & ex B being finite set st
( B = Left_Cosets H & b₂ = card B ) holds
b₁ = b₂ ;

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 b₃ being Element of NAT holds
( b₃ = index H iff ex B being finite set st
( B = Left_Cosets H & b₃ = 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;

:: 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 b₁ being set st
for x being object holds
( x in b₁ iff x is strict Subgroup of G )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff x is strict Subgroup of G ) ) & ( for x being object holds
( x in b₂ iff x is strict Subgroup of G ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Subgroups GROUP_1A:def 29 :
for G being addGroup
for b₂ being set holds
( b₂ = Subgroups G iff for x being object holds
( x in b₂ 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 b₁ being strict Subgroup of G st the carrier of b₁ = (carr H) * a

proof end;

correctness
uniqueness
for b₁, b₂ being strict Subgroup of G st the carrier of b₁ = (carr H) * a & the carrier of b₂ = (carr H) * a holds
b₁ = b₂;
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 b₄ being strict Subgroup of G holds
( b₄ = H * a iff the carrier of b₄ = (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,b₁,b₁) by Th75;
symmetry
for a, b being Element of G st (G,b₁,b₂) holds
(G,b₂,b₁) 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,b₁,b₁) by Th89;
symmetry
for A, B being Subset of G st (G,b₁,b₂) holds
(G,b₂,b₁) 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,b₁,b₁) by ThB103;
symmetry
for H1, H2 being strict Subgroup of G st (G,b₁,b₂) holds
(G,b₂,b₁) 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 b₁ being Subset of (Subgroups G) st
for x being object holds
( x in b₁ iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) )

proof end;

uniqueness
for b₁, b₂ being Subset of (Subgroups G) st ( for x being object holds
( x in b₁ iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) ) ) & ( for x being object holds
( x in b₂ iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines con_class GROUP_1A:def 40 :
for G being addGroup
for H being Subgroup of G
for b₃ being Subset of (Subgroups G) holds
( b₃ = con_class H iff for x being object holds
( x in b₃ 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 b₁ being Subgroup of G st
( b₁ is strict & b₁ 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 b₁ being strict Subgroup of G st the carrier of b₁ = { h where h is Element of G : A * h = A }

proof end;

uniqueness
for b₁, b₂ being strict Subgroup of G st the carrier of b₁ = { h where h is Element of G : A * h = A } & the carrier of b₂ = { h where h is Element of G : A * h = A } holds
b₁ = b₂ by Th59;

end;

:: deftheorem Def14 defines Normalizer GROUP_1A:def 42 :
for G being addGroup
for A being Subset of G
for b₃ being strict Subgroup of G holds
( b₃ = Normalizer A iff the carrier of b₃ = { 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 b₁ being Function of G,G st
for x being Element of G holds b₁ . x = a + x

proof end;

uniqueness
for b₁, b₂ being Function of G,G st ( for x being Element of G holds b₁ . x = a + x ) & ( for x being Element of G holds b₂ . x = a + x ) holds
b₁ = b₂

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 b₁ being Function of G,G st
for x being Element of G holds b₁ . x = x + a

proof end;

uniqueness
for b₁, b₂ being Function of G,G st ( for x being Element of G holds b₁ . x = x + a ) & ( for x being Element of G holds b₂ . x = x + a ) holds
b₁ = b₂

proof end;

end;

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

:: deftheorem Def2 defines + GROUP_1A:def 45 :
for G being non empty addMagma
for a being Element of G
for b₃ being Function of G,G holds
( b₃ = + a iff for x being Element of G holds b₃ . 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 c₁ 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 b₁ being 1 -element addMagma holds
( b₁ is addGroup-like & b₁ is add-associative & b₁ is Abelian )

proof end;

end;

registration

cluster non empty strict for TopaddGrStr ;

existence
ex b₁ being TopaddGrStr st
( b₁ is strict & not b₁ is empty )

proof end;

end;

registration

cluster 1 -element TopSpace-like strict for TopaddGrStr ;

existence
ex b₁ being TopaddGrStr st
( b₁ is strict & b₁ is TopSpace-like & b₁ 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 b₁ being 1 -element add-associative TopSpace-like addGroup-like TopaddGrStr st
( b₁ is strict & b₁ is Abelian & b₁ is UnContinuous & b₁ 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 b₁ being TopaddGroup st b₁ is BinContinuous holds
b₁ 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 b₁ being TopologicaladdGroup holds b₁ is regular by Th59;

end;