begin
Lm1:
now ( ( for h, g, f being Element of multMagma(# REAL,addreal #) holds (h * g) * f = h * (g * f) ) & ex e being Element of multMagma(# REAL,addreal #) st
for h being Element of multMagma(# REAL,addreal #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# REAL,addreal #) st
( h * g = e & g * h = e ) ) )
set G =
multMagma(#
REAL,
addreal #);
thus
for
h,
g,
f being
Element of
multMagma(#
REAL,
addreal #) holds
(h * g) * f = h * (g * f)
ex e being Element of multMagma(# REAL,addreal #) st
for h being Element of multMagma(# REAL,addreal #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# REAL,addreal #) st
( h * g = e & g * h = e ) )
reconsider e =
0 as
Element of
multMagma(#
REAL,
addreal #) ;
take e =
e;
for h being Element of multMagma(# REAL,addreal #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# REAL,addreal #) st
( h * g = e & g * h = e ) )let h be
Element of
multMagma(#
REAL,
addreal #);
( h * e = h & e * h = h & ex g being Element of multMagma(# 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
;
( e * h = h & ex g being Element of multMagma(# REAL,addreal #) st
( h * g = e & g * h = e ) )thus e * h =
0 + A
by BINOP_2:def 9
.=
h
;
ex g being Element of multMagma(# REAL,addreal #) st
( h * g = e & g * h = e )reconsider g =
- A as
Element of
multMagma(#
REAL,
addreal #) ;
take g =
g;
( h * g = e & g * h = e )thus h * g =
A + (- A)
by BINOP_2:def 9
.=
e
;
g * h = ethus g * h =
(- A) + A
by BINOP_2:def 9
.=
e
;
verum
end;
theorem Th6:
for
G being
Group for
h,
g,
f being
Element of
G st (
h * g = h * f or
g * h = f * h ) holds
g = f
theorem Th13:
for
G being
Group for
h,
f,
g being
Element of
G holds
(
h * f = g iff
f = (h ") * g )
theorem Th14:
for
G being
Group for
f,
h,
g being
Element of
G holds
(
f * h = g iff
f = g * (h ") )
definition
let G be non
empty multMagma ;
existence
ex b1 being Function of [: the carrier of G,NAT:], the carrier of G st
for h being Element of G holds
( b1 . (h,0) = 1_ G & ( for n being Element of NAT holds b1 . (h,(n + 1)) = (b1 . (h,n)) * h ) )
uniqueness
for b1, b2 being Function of [: the carrier of G,NAT:], the carrier of G st ( for h being Element of G holds
( b1 . (h,0) = 1_ G & ( for n being Element of NAT holds b1 . (h,(n + 1)) = (b1 . (h,n)) * h ) ) ) & ( for h being Element of G holds
( b2 . (h,0) = 1_ G & ( for n being Element of NAT holds b2 . (h,(n + 1)) = (b2 . (h,n)) * h ) ) ) holds
b1 = b2
end;
Lm2:
for n being Nat
for G being Group
for h being Element of G holds h |^ (n + 1) = (h |^ n) * h
Lm3:
for G being Group
for h being Element of G holds h |^ 0 = 1_ G
by Def7;
Lm4:
for n being Nat
for G being Group holds (1_ G) |^ n = 1_ G
Lm5:
for n, m being Nat
for G being Group
for h being Element of G holds h |^ (n + m) = (h |^ n) * (h |^ m)
Lm6:
for n being Nat
for G being Group
for h being Element of G holds
( h |^ (n + 1) = (h |^ n) * h & h |^ (n + 1) = h * (h |^ n) )
Lm7:
for n, m being Nat
for G being Group
for h being Element of G holds h |^ (n * m) = (h |^ n) |^ m
Lm8:
for n being Nat
for G being Group
for h being Element of G holds (h ") |^ n = (h |^ n) "
Lm9:
for n being Nat
for G being Group
for g, h being Element of G st g * h = h * g holds
g * (h |^ n) = (h |^ n) * g
Lm10:
for n, m being Nat
for G being Group
for g, h being Element of G st g * h = h * g holds
(g |^ n) * (h |^ m) = (h |^ m) * (g |^ n)
Lm11:
for n being Nat
for G being Group
for g, h being Element of G st g * h = h * g holds
(g * h) |^ n = (g |^ n) * (h |^ n)
Lm12:
for i being Integer
for G being Group
for h being Element of G holds h |^ (- i) = (h |^ i) "
Lm13:
for j being Integer holds
( j >= 1 or j = 0 or j < 0 )
Lm14:
for j being Integer
for G being Group
for h being Element of G holds h |^ (j - 1) = (h |^ j) * (h |^ (- 1))
Lm15:
for j being Integer holds
( j >= 0 or j = - 1 or j < - 1 )
Lm16:
for j being Integer
for G being Group
for h being Element of G holds h |^ (j + 1) = (h |^ j) * (h |^ 1)
Lm17:
for i being Integer
for G being Group
for h being Element of G holds (h ") |^ i = (h |^ i) "
begin