environ
vocabularies HIDDEN, NUMBERS, NAT_1, INT_1, XBOOLE_0, ALGSTR_0, SUBSET_1, BINOP_2, RELAT_1, REAL_1, ARYTM_3, CARD_1, ARYTM_1, BINOP_1, STRUCT_0, FUNCT_1, SETWISEO, FINSEQOP, ZFMISC_1, NEWTON, COMPLEX1, XXREAL_0, FINSET_1, TARSKI, RLVECT_1, SUPINF_2, GROUP_1, ORDINAL1;
notations HIDDEN, TARSKI, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, RELAT_1, FUNCT_1, XREAL_0, FUNCT_2, BINOP_2, BINOP_1, STRUCT_0, ALGSTR_0, RLVECT_1, INT_1, NAT_1, FINSEQOP, SETWISEO, INT_2;
definitions FUNCT_2, BINOP_1, FINSEQOP, RLVECT_1, SETWISEO, ALGSTR_0;
theorems ABSVALUE, BINOP_1, CARD_1, FINSEQOP, INT_1, NAT_1, ZFMISC_1, BINOP_2, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, NAT_D, XREAL_0;
schemes FUNCT_2, INT_1, NAT_1, CLASSES1;
registrations ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XREAL_0, NAT_1, INT_1, STRUCT_0, ALGSTR_0, CARD_1;
constructors HIDDEN, BINOP_1, SETWISEO, XXREAL_0, REAL_1, NAT_1, NAT_D, BINOP_2, FINSEQOP, RLVECT_1;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities BINOP_1, STRUCT_0, ALGSTR_0;
expansions BINOP_1, FINSEQOP;
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 #)
by XREAL_0:def 1;
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 #)
by XREAL_0:def 1;
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
f,
g,
h being
Element of
G st (
h * g = h * f or
g * h = f * h ) holds
g = f
theorem Th12:
for
G being
Group for
f,
g,
h being
Element of
G holds
(
h * f = g iff
f = (h ") * g )
theorem Th13:
for
G being
Group for
f,
g,
h 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 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 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 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
by Def7;
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 m, n 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 m, n 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 m, n 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) "