:: by Roland Coghetto

::

:: Received April 30, 2015

:: Copyright (c) 2015-2018 Association of Mizar Users

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 ) ) )

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 ) )

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

reconsider e = 0 as Element of addMagma(# REAL,addreal #) by XREAL_0:def 1;
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 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

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

definition

let IT be addMagma ;

end;
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 );

ex e being Element of IT st

for h being Element of IT holds

( h + e = h & e + h = h );

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

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

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

registration

existence

ex b_{1} being addMagma st

( b_{1} is strict & b_{1} is addGroup-like & b_{1} is add-associative & not b_{1} is empty )

end;
ex b

( b

proof end;

theorem :: GROUP_1A:1

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 )

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

definition

let G be addMagma ;

assume A1: G is add-unital ;

ex b_{1} being Element of G st

for h being Element of G holds

( h + b_{1} = h & b_{1} + h = h )
by A1;

uniqueness

for b_{1}, b_{2} being Element of G st ( for h being Element of G holds

( h + b_{1} = h & b_{1} + h = h ) ) & ( for h being Element of G holds

( h + b_{2} = h & b_{2} + h = h ) ) holds

b_{1} = b_{2}

end;
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 for h being Element of G holds

( h + it = h & it + h = h );

ex b

for h being Element of G holds

( h + b

uniqueness

for b

( h + b

( h + b

b

proof end;

:: deftheorem Def4 defines 0_ GROUP_1A:def 3 :

for G being addMagma st G is add-unital holds

for b_{2} being Element of G holds

( b_{2} = 0_ G iff for h being Element of G holds

( h + b_{2} = h & b_{2} + h = h ) );

for G being addMagma st G is add-unital holds

for b

( b

( h + b

theorem :: GROUP_1A:4

definition

let G be addGroup;

let h be Element of G;

existence

ex b_{1} being Element of G st

( h + b_{1} = 0_ G & b_{1} + h = 0_ G )

for b_{1}, b_{2} being Element of G st h + b_{1} = 0_ G & b_{1} + h = 0_ G & h + b_{2} = 0_ G & b_{2} + h = 0_ G holds

b_{1} = b_{2}

for b_{1}, b_{2} being Element of G st b_{2} + b_{1} = 0_ G & b_{1} + b_{2} = 0_ G holds

( b_{1} + b_{2} = 0_ G & b_{2} + b_{1} = 0_ G )
;

end;
let h be Element of G;

existence

ex b

( h + b

proof end;

uniqueness for b

b

proof end;

involutiveness for b

( b

:: deftheorem Def5 defines - GROUP_1A:def 4 :

for G being addGroup

for h, b_{3} being Element of G holds

( b_{3} = - h iff ( h + b_{3} = 0_ G & b_{3} + h = 0_ G ) );

for G being addGroup

for h, b

( b

theorem :: GROUP_1A:5

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

for f, g, h being Element of G st ( h + g = h + f or g + h = f + h ) holds

g = f

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) )

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) )

for g, h being Element of G holds

( g + h = h + g iff (- g) + (- h) = (- h) + (- g) )

proof end;

definition

let G be addGroup;

ex b_{1} being UnOp of G st

for h being Element of G holds b_{1} . h = - h

for b_{1}, b_{2} being UnOp of G st ( for h being Element of G holds b_{1} . h = - h ) & ( for h being Element of G holds b_{2} . h = - h ) holds

b_{1} = b_{2}

end;
func add_inverse G -> UnOp of G means :Def6: :: GROUP_1A:def 5

for h being Element of G holds it . h = - h;

existence for h being Element of G holds it . h = - h;

ex b

for h being Element of G holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines add_inverse GROUP_1A:def 5 :

for G being addGroup

for b_{2} being UnOp of G holds

( b_{2} = add_inverse G iff for h being Element of G holds b_{2} . h = - h );

for G being addGroup

for b

( b

registration
end;

registration
end;

definition

let G be non empty addMagma ;

ex b_{1} being Function of [:NAT, the carrier of G:], the carrier of G st

for h being Element of G holds

( b_{1} . (0,h) = 0_ G & ( for n being Nat holds b_{1} . ((n + 1),h) = (b_{1} . (n,h)) + h ) )

for b_{1}, b_{2} being Function of [:NAT, the carrier of G:], the carrier of G st ( for h being Element of G holds

( b_{1} . (0,h) = 0_ G & ( for n being Nat holds b_{1} . ((n + 1),h) = (b_{1} . (n,h)) + h ) ) ) & ( for h being Element of G holds

( b_{2} . (0,h) = 0_ G & ( for n being Nat holds b_{2} . ((n + 1),h) = (b_{2} . (n,h)) + h ) ) ) holds

b_{1} = b_{2}

end;
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 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 ) );

ex b

for h being Element of G holds

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def7 defines mult GROUP_1A:def 6 :

for G being non empty addMagma

for b_{2} being Function of [:NAT, the carrier of G:], the carrier of G holds

( b_{2} = mult G iff for h being Element of G holds

( b_{2} . (0,h) = 0_ G & ( for n being Nat holds b_{2} . ((n + 1),h) = (b_{2} . (n,h)) + h ) ) );

for G being non empty addMagma

for b

( b

( b

definition

let G be addGroup;

let i be Integer;

let h be Element of G;

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_{1} being Element of G holds verum;

;

end;
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 (mult G) . (|.i.|,h) if 0 <= i

otherwise - ((mult G) . (|.i.|,h));

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

;

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

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;

compatibility

for b_{1} being Element of G holds

( b_{1} = n * h iff b_{1} = (mult G) . (n,h) )

end;
let n be Nat;

let h be Element of G;

compatibility

for b

( b

proof 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);

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;

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)

for G being addGroup

for h being Element of G st i <= 0 holds

i * h = - (|.i.| * 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)

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) )

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

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)

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)

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

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;

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

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

definition

let G be addGroup;

let h be Element of G;

( ( h is being_of_order_0 implies ex b_{1} being Element of NAT st b_{1} = 0 ) & ( not h is being_of_order_0 implies ex b_{1} being Element of NAT st

( b_{1} * h = 0_ G & b_{1} <> 0 & ( for m being Nat st m * h = 0_ G & m <> 0 holds

b_{1} <= m ) ) ) )

for b_{1}, b_{2} being Element of NAT holds

( ( h is being_of_order_0 & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) & ( not h is being_of_order_0 & b_{1} * h = 0_ G & b_{1} <> 0 & ( for m being Nat st m * h = 0_ G & m <> 0 holds

b_{1} <= m ) & b_{2} * h = 0_ G & b_{2} <> 0 & ( for m being Nat st m * h = 0_ G & m <> 0 holds

b_{2} <= m ) implies b_{1} = b_{2} ) )

consistency

for b_{1} being Element of NAT holds verum;

;

end;
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 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 ) );

( ( h is being_of_order_0 implies ex b

( b

b

proof end;

uniqueness for b

( ( h is being_of_order_0 & b

b

b

proof end;

correctness consistency

for b

;

:: deftheorem Def11 defines ord GROUP_1A:def 10 :

for G being addGroup

for h being Element of G

for b_{3} being Element of NAT holds

( ( h is being_of_order_0 implies ( b_{3} = ord h iff b_{3} = 0 ) ) & ( not h is being_of_order_0 implies ( b_{3} = ord h iff ( b_{3} * h = 0_ G & b_{3} <> 0 & ( for m being Nat st m * h = 0_ G & m <> 0 holds

b_{3} <= m ) ) ) ) );

for G being addGroup

for h being Element of G

for b

( ( h is being_of_order_0 implies ( b

b

registration
end;

theorem :: GROUP_1A:43

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 )

( 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 :: 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))

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;

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

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;

coherence

{ (- g) where g is Element of G : g in A } is Subset of G

for b_{1}, b_{2} being Subset of G st b_{1} = { (- g) where g is Element of G : g in b_{2} } holds

b_{2} = { (- g) where g is Element of G : g in b_{1} }

end;
let A be Subset of G;

coherence

{ (- g) where g is Element of G : g in A } is Subset of G

proof end;

involutiveness for b

b

proof 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 } ;

for G being addGroup

for A being Subset of G holds - A = { (- g) where g is Element of G : g in A } ;

registration
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

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

theorem Th9: :: GROUP_1A:55

for G being non empty addMagma

for A, B being Subset of G holds

( ( A <> {} & B <> {} ) iff A + B <> {} )

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)

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

for G being non empty addMagma

for A, B, C being Subset of G holds A + (B \/ C) = (A + B) \/ (A + C)

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)

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)

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)

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) = {} )

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 )

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 :: 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)}

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)}

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)}

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

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

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

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

for A, B being Subset of G st G is Abelian addGroup holds

A + B = B + A

proof end;

definition

let G be non empty addMagma ;

let g be Element of G;

let A be Subset of G;

correctness

coherence

{g} + A is Subset of G;

;

correctness

coherence

A + {g} is Subset of G;

;

end;
let g be Element of G;

let A be Subset of G;

correctness

coherence

{g} + A is Subset of G;

;

correctness

coherence

A + {g} is Subset of G;

;

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

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

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 ) )

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 ) )

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 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)

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 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)

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

theorem :: GROUP_1A:82

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 )

for A being Subset of G holds

( (0_ G) + A = A & A + (0_ G) = A )

proof end;

theorem :: GROUP_1A:84

definition

let G be non empty addGroup-like addMagma ;

ex b_{1} being non empty addGroup-like addMagma st

( the carrier of b_{1} c= the carrier of G & the addF of b_{1} = the addF of G || the carrier of b_{1} )

end;
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 ( the carrier of it c= the carrier of G & the addF of it = the addF of G || the carrier of it );

ex b

( the carrier of b

proof end;

:: deftheorem DefA5 defines Subgroup GROUP_1A:def 15 :

for G, b_{2} being non empty addGroup-like addMagma holds

( b_{2} is Subgroup of G iff ( the carrier of b_{2} c= the carrier of G & the addF of b_{2} = the addF of G || the carrier of b_{2} ) );

for G, b

( 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

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

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;

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;

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

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;

coherence

for b_{1} being Subgroup of G holds b_{1} is add-associative

end;
coherence

for b

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

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

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

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;

registration
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

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;

registration
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 #)

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

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

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

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 #)

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 #)

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;

( H1 = H2 iff for g being Element of G holds

( g in H1 iff g in H2 ) ) by Th60;

end;
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 redefine pred H1 = H2 means :: GROUP_1A:def 16

for g being Element of G holds

( g in H1 iff g in H2 );

( H1 = H2 iff for g being Element of G holds

( g in H1 iff g in H2 ) ) by Th60;

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

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 #)

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 #)

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;

existence

ex b_{1} being strict Subgroup of G st the carrier of b_{1} = {(0_ G)}

for b_{1}, b_{2} being strict Subgroup of G st the carrier of b_{1} = {(0_ G)} & the carrier of b_{2} = {(0_ G)} holds

b_{1} = b_{2}
by Th59;

end;
existence

ex b

proof end;

uniqueness for b

b

:: deftheorem Def7 defines (0). GROUP_1A:def 17 :

for G being addGroup

for b_{2} being strict Subgroup of G holds

( b_{2} = (0). G iff the carrier of b_{2} = {(0_ G)} );

for G being addGroup

for b

( b

definition

let G be addGroup;

addMagma(# the carrier of G, the addF of G #) is strict Subgroup of G

for b_{1} being strict Subgroup of G

for b_{2} being addGroup st b_{1} = addMagma(# the carrier of b_{2}, the addF of b_{2} #) holds

b_{1} = addMagma(# the carrier of b_{1}, the addF of b_{1} #)
;

end;
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 #);

addMagma(# the carrier of G, the addF of G #) is strict Subgroup of G

proof end;

projectivity for b

for b

b

:: deftheorem defines (Omega). GROUP_1A:def 18 :

for G being addGroup holds (Omega). G = addMagma(# the carrier of G, the addF of G #);

for G being addGroup holds (Omega). G = addMagma(# the carrier of G, the addF of G #);

theorem :: GROUP_1A:112

registration

let G be addGroup;

coherence

(0). G is finite by Th68;

existence

ex b_{1} being Subgroup of G st

( b_{1} is strict & b_{1} is finite )

end;
coherence

(0). G is finite by Th68;

existence

ex b

( b

proof end;

registration
end;

registration
end;

theorem :: GROUP_1A:117

theorem :: GROUP_1A:118

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 #)

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

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

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

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 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) ) )

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)

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;

ex b_{1} being strict Subgroup of G st the carrier of b_{1} = (carr H1) /\ (carr H2)

for b_{1}, b_{2} being strict Subgroup of G st the carrier of b_{1} = (carr H1) /\ (carr H2) & the carrier of b_{2} = (carr H1) /\ (carr H2) holds

b_{1} = b_{2}
by Th59;

end;
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 the carrier of it = (carr H1) /\ (carr H2);

ex b

proof end;

uniqueness for b

b

:: deftheorem Def10 defines /\ GROUP_1A:def 20 :

for G being addGroup

for H1, H2 being Subgroup of G

for b_{4} being strict Subgroup of G holds

( b_{4} = H1 /\ H2 iff the carrier of b_{4} = (carr H1) /\ (carr H2) );

for G being addGroup

for H1, H2 being Subgroup of G

for b

( b

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 ) )

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

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 ) )

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;

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

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

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 )

for H being Subgroup of G holds

( ((0). G) /\ H = (0). G & H /\ ((0). G) = (0). G )

proof end;

theorem :: GROUP_1A:132

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

theorem :: GROUP_1A:135

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

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

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

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

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;

correctness

coherence

A + (carr H) is Subset of G;

;

correctness

coherence

(carr H) + A is Subset of G;

;

end;
let H be Subgroup of G;

let A be Subset of G;

correctness

coherence

A + (carr H) is Subset of G;

;

correctness

coherence

(carr H) + A is Subset of G;

;

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

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;

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 ) )

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 ) )

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 :: GROUP_1A:145

theorem :: GROUP_1A:146

theorem :: GROUP_1A:147

theorem :: GROUP_1A:148

definition

let G be addGroup;

let H be Subgroup of G;

let a be Element of G;

correctness

coherence

a + (carr H) is Subset of G;

;

correctness

coherence

(carr H) + a is Subset of G;

;

end;
let H be Subgroup of G;

let a be Element of G;

correctness

coherence

a + (carr H) is Subset of G;

;

correctness

coherence

(carr H) + a is Subset of G;

;

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

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;

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 ) )

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 ) )

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 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 )

for a being Element of G

for H being Subgroup of G holds

( a in a + H & a in H + 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 )

for a being Element of G holds

( a + ((Omega). G) = the carrier of G & ((Omega). G) + a = the carrier of G )

proof end;

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 )

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 )

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 )

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)

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) )

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)

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 )

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 )

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 )

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)

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) )

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)

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)

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)

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)

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

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

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

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 )

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

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 )

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;

ex b_{1} being Subset-Family of G st

for A being Subset of G holds

( A in b_{1} iff ex a being Element of G st A = a + H )

for b_{1}, b_{2} being Subset-Family of G st ( for A being Subset of G holds

( A in b_{1} iff ex a being Element of G st A = a + H ) ) & ( for A being Subset of G holds

( A in b_{2} iff ex a being Element of G st A = a + H ) ) holds

b_{1} = b_{2}

ex b_{1} being Subset-Family of G st

for A being Subset of G holds

( A in b_{1} iff ex a being Element of G st A = H + a )

for b_{1}, b_{2} being Subset-Family of G st ( for A being Subset of G holds

( A in b_{1} iff ex a being Element of G st A = H + a ) ) & ( for A being Subset of G holds

( A in b_{2} iff ex a being Element of G st A = H + a ) ) holds

b_{1} = b_{2}

end;
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 for A being Subset of G holds

( A in it iff ex a being Element of G st A = a + H );

ex b

for A being Subset of G holds

( A in b

proof end;

uniqueness for b

( A in b

( A in 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 for A being Subset of G holds

( A in it iff ex a being Element of G st A = H + a );

ex b

for A being Subset of G holds

( A in b

proof end;

uniqueness for b

( A in b

( A in b

b

proof end;

:: deftheorem Def15 defines Left_Cosets GROUP_1A:def 25 :

for G being addGroup

for H being Subgroup of G

for b_{3} being Subset-Family of G holds

( b_{3} = Left_Cosets H iff for A being Subset of G holds

( A in b_{3} iff ex a being Element of G st A = a + H ) );

for G being addGroup

for H being Subgroup of G

for b

( b

( A in b

:: deftheorem Def16 defines Right_Cosets GROUP_1A:def 26 :

for G being addGroup

for H being Subgroup of G

for b_{3} being Subset-Family of G holds

( b_{3} = Right_Cosets H iff for A being Subset of G holds

( A in b_{3} iff ex a being Element of G st A = H + a ) );

for G being addGroup

for H being Subgroup of G

for b

( b

( A in b

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

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 )

for H being Subgroup of G holds

( carr H in Left_Cosets H & carr H in Right_Cosets H )

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 )

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

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

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} )

( 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

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

for H being strict Subgroup of G st Right_Cosets H = { the carrier of G} holds

H = G

proof end;

definition
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);

for G being addGroup

for H being Subgroup of G holds Index H = card (Left_Cosets H);

definition

let G be addGroup;

let H be Subgroup of G;

assume A1: Left_Cosets H is finite ;

ex b_{1} being Element of NAT ex B being finite set st

( B = Left_Cosets H & b_{1} = card B )

for b_{1}, b_{2} being Element of NAT st ex B being finite set st

( B = Left_Cosets H & b_{1} = card B ) & ex B being finite set st

( B = Left_Cosets H & b_{2} = card B ) holds

b_{1} = b_{2}
;

end;
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 finite set st

( B = Left_Cosets H & it = card B );

ex b

( B = Left_Cosets H & b

proof end;

uniqueness for b

( B = Left_Cosets H & b

( B = Left_Cosets H & b

b

:: 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_{3} being Element of NAT holds

( b_{3} = index H iff ex B being finite set st

( B = Left_Cosets H & b_{3} = card B ) );

for G being addGroup

for H being Subgroup of G st Left_Cosets H is finite holds

for b

( b

( B = Left_Cosets H & 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 ) )

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

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

for H being strict Subgroup of G st Left_Cosets H is finite & index H = 1 holds

H = 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 )

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 )

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

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 )

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

theorem :: GROUP_1A:209

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)

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)

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)

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)

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

definition

let G be addGroup;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff x is strict Subgroup of G )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff x is strict Subgroup of G ) ) & ( for x being object holds

( x in b_{2} iff x is strict Subgroup of G ) ) holds

b_{1} = b_{2}

end;
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 for x being object holds

( x in it iff x is strict Subgroup of G );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def1 defines Subgroups GROUP_1A:def 29 :

for G being addGroup

for b_{2} being set holds

( b_{2} = Subgroups G iff for x being object holds

( x in b_{2} iff x is strict Subgroup of G ) );

for G being addGroup

for b

( b

( x in b

registration
end;

definition
end;

:: deftheorem defines * GROUP_1A:def 30 :

for G being addGroup

for a, b being Element of G holds a * b = ((- b) + a) + b;

for G being addGroup

for a, b being Element of G holds a * b = ((- b) + a) + b;

theorem :: GROUP_1A:222

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 )

for a, b being Element of G holds

( (a * b) * (- b) = a & (a * (- b)) * b = a )

proof end;

Lm2: now :: thesis: for G being addGroup

for a, b being Element of G holds (0 * a) * b = 0 * (a * b)

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

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)

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

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

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)

for a, b being Element of G

for i being Integer holds (i * a) * b = i * (a * b)

proof end;

definition

let G be addGroup;

let A, B be Subset of G;

{ (g * h) where g, h is Element of G : ( g in A & h in B ) } is Subset of G

end;
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 ) } ;

{ (g * h) where g, h is Element of G : ( g in A & h in B ) } is Subset of G

proof 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 ) } ;

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 :: 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)}

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;

correctness

coherence

A * {g} is Subset of G;

;

correctness

coherence

{g} * A is Subset of G;

;

end;
let A be Subset of G;

let g be Element of G;

correctness

coherence

A * {g} is Subset of G;

;

correctness

coherence

{g} * A is Subset of G;

;

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

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;

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 ) )

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 ) )

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

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

theorem :: GROUP_1A:246

theorem :: GROUP_1A:247

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)

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

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)

for a, b being Element of G

for A being Subset of G holds (a * b) * A = a * (b + A)

proof end;

theorem :: GROUP_1A:252

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 )

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 )

( 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 )

( 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} )

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

ex b_{1} being strict Subgroup of G st the carrier of b_{1} = (carr H) * a

uniqueness

for b_{1}, b_{2} being strict Subgroup of G st the carrier of b_{1} = (carr H) * a & the carrier of b_{2} = (carr H) * a holds

b_{1} = b_{2};

by Th59;

end;
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 the carrier of it = (carr H) * a;

ex b

proof end;

correctness uniqueness

for b

b

by Th59;

:: 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_{4} being strict Subgroup of G holds

( b_{4} = H * a iff the carrier of b_{4} = (carr H) * a );

for G being addGroup

for H being Subgroup of G

for a being Element of G

for b

( b

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 ) )

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

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)

for a, b being Element of G

for H being Subgroup of G holds (H * a) * b = H * (a + b)

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 )

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)

for a being Element of G

for H1, H2 being Subgroup of G holds (H1 /\ H2) * a = (H1 * a) /\ (H2 * 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 )

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;

coherence

H * a is finite by Th65;

end;
let a be Element of G;

let H be finite Subgroup of G;

coherence

H * a is finite by Th65;

theorem :: GROUP_1A:267

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

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

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)

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)

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

for H being strict Subgroup of G

for a being Element of G holds H * a = H

proof 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 );

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
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 )

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_{1},b_{1})
by Th75;

symmetry

for a, b being Element of G st (G,b_{1},b_{2}) holds

(G,b_{2},b_{1})
by Th76;

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

symmetry

for a, b being Element of G st (G,b

(G,b

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

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

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 }

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;

correctness

coherence

a * (carr ((Omega). G)) is Subset of G;

;

end;
let a be Element of G;

correctness

coherence

a * (carr ((Omega). G)) is Subset of G;

;

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

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 ) )

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 :: GROUP_1A:281

theorem :: GROUP_1A:282

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 )

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

for a being Element of G

for A being Subset of G holds (con_class a) + A = A + (con_class a)

proof 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 );

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
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 )

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;

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_{1},b_{1})
by Th89;

symmetry

for A, B being Subset of G st (G,b_{1},b_{2}) holds

(G,b_{2},b_{1})
by Th90;

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

symmetry

for A, B being Subset of G st (G,b

(G,b

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

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 )

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

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;

{ B where B is Subset of G : A,B are_conjugated } is Subset-Family of G

end;
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 } ;

{ B where B is Subset of G : A,B are_conjugated } is Subset-Family of G

proof 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 } ;

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

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 )

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 }

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

definition

let G be addGroup;

let H1, H2 be Subgroup of G;

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

ex g being Element of G st addMagma(# the carrier of H1, the addF of H1 #) = H2 * g;

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

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;
let H1, H2 be Subgroup of G;

antonym H1,H2 are_not_conjugated for H1,H2 are_conjugated ;

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 )

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

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_{1},b_{1})
by ThB103;

symmetry

for H1, H2 being strict Subgroup of G st (G,b_{1},b_{2}) holds

(G,b_{2},b_{1})
by ThB104;

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

symmetry

for H1, H2 being strict Subgroup of G st (G,b

(G,b

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

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;

ex b_{1} being Subset of (Subgroups G) st

for x being object holds

( x in b_{1} iff ex H1 being strict Subgroup of G st

( x = H1 & H,H1 are_conjugated ) )

for b_{1}, b_{2} being Subset of (Subgroups G) st ( for x being object holds

( x in b_{1} iff ex H1 being strict Subgroup of G st

( x = H1 & H,H1 are_conjugated ) ) ) & ( for x being object holds

( x in b_{2} iff ex H1 being strict Subgroup of G st

( x = H1 & H,H1 are_conjugated ) ) ) holds

b_{1} = b_{2}

end;
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 for x being object holds

( x in it iff ex H1 being strict Subgroup of G st

( x = H1 & H,H1 are_conjugated ) );

ex b

for x being object holds

( x in b

( x = H1 & H,H1 are_conjugated ) )

proof end;

uniqueness for b

( x in b

( x = H1 & H,H1 are_conjugated ) ) ) & ( for x being object holds

( x in b

( x = H1 & H,H1 are_conjugated ) ) ) holds

b

proof end;

:: deftheorem Def12 defines con_class GROUP_1A:def 40 :

for G being addGroup

for H being Subgroup of G

for b_{3} being Subset of (Subgroups G) holds

( b_{3} = con_class H iff for x being object holds

( x in b_{3} iff ex H1 being strict Subgroup of G st

( x = H1 & H,H1 are_conjugated ) ) );

for G being addGroup

for H being Subgroup of G

for b

( b

( x in b

( 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

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 )

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

for g being Element of G

for H being strict Subgroup of G holds H * g 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

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 )

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

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 )

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;

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

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;

existence

ex b_{1} being Subgroup of G st

( b_{1} is strict & b_{1} is normal )

end;
existence

ex b

( b

proof end;

theorem :: GROUP_1A:315

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 )

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 )

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 )

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 )

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 )

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 )

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} )

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 )

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

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)

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

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;

ex b_{1} being strict Subgroup of G st the carrier of b_{1} = { h where h is Element of G : A * h = A }

for b_{1}, b_{2} being strict Subgroup of G st the carrier of b_{1} = { h where h is Element of G : A * h = A } & the carrier of b_{2} = { h where h is Element of G : A * h = A } holds

b_{1} = b_{2}
by Th59;

end;
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 the carrier of it = { h where h is Element of G : A * h = A } ;

ex b

proof end;

uniqueness for b

b

:: deftheorem Def14 defines Normalizer GROUP_1A:def 42 :

for G being addGroup

for A being Subset of G

for b_{3} being strict Subgroup of G holds

( b_{3} = Normalizer A iff the carrier of b_{3} = { h where h is Element of G : A * h = A } );

for G being addGroup

for A being Subset of G

for b

( b

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 ) )

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

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 :: 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}) )

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;

correctness

coherence

Normalizer (carr H) is strict Subgroup of G;

;

end;
let H be Subgroup of G;

correctness

coherence

Normalizer (carr H) is strict Subgroup of G;

;

:: deftheorem defines Normalizer GROUP_1A:def 43 :

for G being addGroup

for H being Subgroup of G holds Normalizer H = Normalizer (carr H);

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 ) )

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)

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) )

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 )

for H being strict Subgroup of G holds

( H is normal Subgroup of G iff Normalizer H = 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

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

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

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 )

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;

registration
end;

definition

let G be non empty addMagma ;

let a be Element of G;

ex b_{1} being Function of G,G st

for x being Element of G holds b_{1} . x = a + x

for b_{1}, b_{2} being Function of G,G st ( for x being Element of G holds b_{1} . x = a + x ) & ( for x being Element of G holds b_{2} . x = a + x ) holds

b_{1} = b_{2}

ex b_{1} being Function of G,G st

for x being Element of G holds b_{1} . x = x + a

for b_{1}, b_{2} being Function of G,G st ( for x being Element of G holds b_{1} . x = x + a ) & ( for x being Element of G holds b_{2} . x = x + a ) holds

b_{1} = b_{2}

end;
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 for x being Element of G holds it . x = a + x;

ex b

for x being Element of G holds b

proof end;

uniqueness for 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 for x being Element of G holds it . x = x + a;

ex b

for x being Element of G holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines + GROUP_1A:def 44 :

for G being non empty addMagma

for a being Element of G

for b_{3} being Function of G,G holds

( b_{3} = a + iff for x being Element of G holds b_{3} . x = a + x );

for G being non empty addMagma

for a being Element of G

for b

( b

:: deftheorem Def2 defines + GROUP_1A:def 45 :

for G being non empty addMagma

for a being Element of G

for b_{3} being Function of G,G holds

( b_{3} = + a iff for x being Element of G holds b_{3} . x = x + a );

for G being non empty addMagma

for a being Element of G

for b

( b

registration

let G be addGroup;

let a be Element of G;

coherence

( a + is one-to-one & a + is onto )

( + a is one-to-one & + a is onto )

end;
let a be Element of G;

coherence

( a + is one-to-one & a + is onto )

proof end;

coherence ( + a is one-to-one & + a is onto )

proof 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

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

for P being Subset of H

for h being Element of H holds (+ h) .: P = P + h

proof end;

:: On the topological groups

definition

attr c_{1} is strict ;

struct TopaddGrStr -> addMagma , TopStruct ;

aggr TopaddGrStr(# carrier, addF, topology #) -> TopaddGrStr ;

end;
struct TopaddGrStr -> addMagma , TopStruct ;

aggr TopaddGrStr(# carrier, addF, topology #) -> TopaddGrStr ;

registration

let A be non empty set ;

let R be BinOp of A;

let T be Subset-Family of A;

coherence

not TopaddGrStr(# A,R,T #) is empty ;

end;
let R be BinOp of A;

let T be Subset-Family of A;

coherence

not TopaddGrStr(# A,R,T #) is empty ;

registration

let x be set ;

let R be BinOp of {x};

let T be Subset-Family of {x};

coherence

TopaddGrStr(# {x},R,T #) is trivial ;

end;
let R be BinOp of {x};

let T be Subset-Family of {x};

coherence

TopaddGrStr(# {x},R,T #) is trivial ;

registration

coherence

for b_{1} being 1 -element addMagma holds

( b_{1} is addGroup-like & b_{1} is add-associative & b_{1} is Abelian )

end;
for b

( b

proof end;

registration
end;

registration

existence

ex b_{1} being TopaddGrStr st

( b_{1} is strict & b_{1} is TopSpace-like & b_{1} is 1 -element )

end;
ex b

( b

proof 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 );

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 ;

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

for f being Function of [:G,G:],G st f = the addF of G holds

f is continuous ;

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

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

ex b_{1} being 1 -element add-associative TopSpace-like addGroup-like TopaddGrStr st

( b_{1} is strict & b_{1} is Abelian & b_{1} is UnContinuous & b_{1} is BinContinuous )
end;

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

( b

proof end;

definition
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

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

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

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

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

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

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;

coherence

a + is continuous

+ a is continuous

end;
let a be Element of G;

coherence

a + is continuous

proof end;

coherence + a is continuous

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

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

redefine func add_inverse G -> Homeomorphism of G;

coherence

add_inverse G is Homeomorphism of G by Th44;

registration

for b_{1} being TopaddGroup st b_{1} is BinContinuous holds

b_{1} is homogeneous
end;

cluster non empty add-associative TopSpace-like addGroup-like BinContinuous -> homogeneous for TopaddGroup;

coherence for b

b

proof 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

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

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;

coherence

F + a is closed by Th45;

coherence

a + F is closed by Th46;

end;
let F be closed Subset of G;

let a be Element of G;

coherence

F + a is closed by Th45;

coherence

a + F is closed by Th46;

registration
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

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

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;

coherence

A + a is open by Th48;

coherence

a + A is open by Th49;

end;
let A be open Subset of G;

let a be Element of G;

coherence

A + a is open by Th48;

coherence

a + A is open by Th49;

registration
end;

registration

let G be BinContinuous TopaddGroup;

let A be open Subset of G;

let B be Subset of G;

coherence

A + B is open by Th51;

coherence

B + A is open by Th52;

end;
let A be open Subset of G;

let B be Subset of G;

coherence

A + B is open by Th51;

coherence

B + A is open by Th52;

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

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

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;

registration
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

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

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;

coherence

A + a is dense by Th57;

coherence

a + A is dense by Th56;

end;
let A be dense Subset of G;

let a be Point of G;

coherence

A + a is dense by Th57;

coherence

a + A is dense by Th56;

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

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

for b_{1} being TopologicaladdGroup holds b_{1} is regular
by Th59;

end;

cluster non empty add-associative TopSpace-like addGroup-like UnContinuous BinContinuous -> regular for TopologicaladdGroup;

coherence for b