:: Groups
:: by Wojciech A. Trybulec
::
:: Received July 3, 1990
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
now
set G =
multMagma(#
REAL ,
addreal #);
thus
for
h,
g,
f being
Element of
multMagma(#
REAL ,
addreal #) holds
(h * g) * f = h * (g * f)
:: thesis: 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;
:: thesis: 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 #);
:: thesis: ( 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
;
:: thesis: ( 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
;
:: thesis: 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;
:: thesis: ( h * g = e & g * h = e )thus h * g =
A + (- A)
by BINOP_2:def 9
.=
e
;
:: thesis: g * h = ethus g * h =
(- A) + A
by BINOP_2:def 9
.=
e
;
:: thesis: verum
end;
:: deftheorem GROUP_1:def 1 :
canceled;
:: deftheorem Def2 defines unital GROUP_1:def 2 :
:: deftheorem Def3 defines Group-like GROUP_1:def 3 :
:: deftheorem Def4 defines associative GROUP_1:def 4 :
theorem :: GROUP_1:1
canceled;
theorem :: GROUP_1:2
canceled;
theorem :: GROUP_1:3
canceled;
theorem :: GROUP_1:4
canceled;
theorem :: GROUP_1:5
theorem :: GROUP_1:6
theorem Th7: :: GROUP_1:7
:: deftheorem Def5 defines 1_ GROUP_1:def 5 :
theorem :: GROUP_1:8
canceled;
theorem :: GROUP_1:9
canceled;
theorem :: GROUP_1:10
:: deftheorem Def6 defines " GROUP_1:def 6 :
theorem :: GROUP_1:11
canceled;
theorem :: GROUP_1:12
theorem :: GROUP_1:13
canceled;
theorem Th14: :: GROUP_1:14
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 :: GROUP_1:15
theorem Th16: :: GROUP_1:16
theorem Th17: :: GROUP_1:17
theorem :: GROUP_1:18
theorem Th19: :: GROUP_1:19
theorem Th20: :: GROUP_1:20
theorem Th21: :: GROUP_1:21
for
G being
Group for
h,
f,
g being
Element of
G holds
(
h * f = g iff
f = (h " ) * g )
theorem Th22: :: GROUP_1:22
for
G being
Group for
f,
h,
g being
Element of
G holds
(
f * h = g iff
f = g * (h " ) )
theorem :: GROUP_1:23
theorem :: GROUP_1:24
theorem Th25: :: GROUP_1:25
theorem Th26: :: GROUP_1:26
theorem Th27: :: GROUP_1:27
theorem Th28: :: GROUP_1:28
:: deftheorem Def7 defines inverse_op GROUP_1:def 7 :
theorem :: GROUP_1:29
canceled;
theorem :: GROUP_1:30
canceled;
theorem Th31: :: GROUP_1:31
theorem Th32: :: GROUP_1:32
theorem Th33: :: GROUP_1:33
theorem Th34: :: GROUP_1:34
theorem Th35: :: GROUP_1:35
theorem Th36: :: GROUP_1:36
theorem :: GROUP_1:37
definition
let G be non
empty multMagma ;
func power G -> Function of
[:the carrier of G,NAT :],the
carrier of
G means :
Def8:
:: GROUP_1:def 8
for
h being
Element of
G holds
(
it . h,
0 = 1_ G & ( for
n being
Element of
NAT holds
it . h,
(n + 1) = (it . h,n) * h ) );
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;
:: deftheorem Def8 defines power GROUP_1:def 8 :
:: deftheorem Def9 defines |^ GROUP_1:def 9 :
:: deftheorem defines |^ GROUP_1:def 10 :
Lm2:
for G being Group
for h being Element of G
for n being Nat holds h |^ (n + 1) = (h |^ n) * h
Lm3:
for G being Group
for h being Element of G holds h |^ 0 = 1_ G
by Def8;
theorem :: GROUP_1:38
canceled;
theorem :: GROUP_1:39
canceled;
theorem :: GROUP_1:40
canceled;
theorem :: GROUP_1:41
canceled;
theorem Th42: :: GROUP_1:42
theorem :: GROUP_1:43
theorem Th44: :: GROUP_1:44
theorem Th45: :: GROUP_1:45
theorem :: GROUP_1:46
theorem :: GROUP_1:47
theorem Th48: :: GROUP_1:48
theorem Th49: :: GROUP_1:49
theorem Th50: :: GROUP_1:50
theorem Th51: :: GROUP_1:51
theorem Th52: :: GROUP_1:52
theorem Th53: :: GROUP_1:53
theorem Th54: :: GROUP_1:54
theorem :: GROUP_1:55
theorem :: GROUP_1:56
theorem :: GROUP_1:57
canceled;
theorem :: GROUP_1:58
canceled;
theorem :: GROUP_1:59
theorem Th60: :: GROUP_1:60
theorem :: GROUP_1:61
theorem Th62: :: GROUP_1:62
Lm4:
for i being Integer
for G being Group
for h being Element of G holds h |^ (- i) = (h |^ i) "
Lm5:
for j being Integer holds
( j >= 1 or j = 0 or j < 0 )
Lm6:
for j being Integer
for G being Group
for h being Element of G holds h |^ (j - 1) = (h |^ j) * (h |^ (- 1))
Lm7:
for j being Integer holds
( j >= 0 or j = - 1 or j < - 1 )
Lm8:
for j being Integer
for G being Group
for h being Element of G holds h |^ (j + 1) = (h |^ j) * (h |^ 1)
theorem Th63: :: GROUP_1:63
theorem :: GROUP_1:64
theorem :: GROUP_1:65
theorem :: GROUP_1:66
Lm9:
for i being Integer
for G being Group
for h being Element of G holds (h " ) |^ i = (h |^ i) "
theorem Th67: :: GROUP_1:67
theorem :: GROUP_1:68
theorem :: GROUP_1:69
theorem :: GROUP_1:70
theorem :: GROUP_1:71
theorem :: GROUP_1:72
theorem Th73: :: GROUP_1:73
theorem Th74: :: GROUP_1:74
theorem :: GROUP_1:75
theorem :: GROUP_1:76
canceled;
theorem :: GROUP_1:77
:: deftheorem Def11 defines being_of_order_0 GROUP_1:def 11 :
theorem :: GROUP_1:78
canceled;
theorem Th79: :: GROUP_1:79
:: deftheorem Def12 defines ord GROUP_1:def 12 :
theorem :: GROUP_1:80
canceled;
theorem :: GROUP_1:81
canceled;
theorem Th82: :: GROUP_1:82
theorem :: GROUP_1:83
canceled;
theorem :: GROUP_1:84
theorem :: GROUP_1:85
theorem :: GROUP_1:86
:: deftheorem GROUP_1:def 13 :
canceled;
theorem :: GROUP_1:87
canceled;
theorem :: GROUP_1:88
canceled;
theorem :: GROUP_1:89
canceled;
theorem :: GROUP_1:90
:: deftheorem GROUP_1:def 14 :
canceled;
:: deftheorem GROUP_1:def 15 :
canceled;
:: deftheorem Def16 defines commutative GROUP_1:def 16 :
theorem :: GROUP_1:91
canceled;
theorem :: GROUP_1:92
theorem :: GROUP_1:93
canceled;
theorem :: GROUP_1:94
theorem :: GROUP_1:95
theorem :: GROUP_1:96
theorem :: GROUP_1:97
theorem Th98: :: GROUP_1:98
theorem :: GROUP_1:99
theorem :: GROUP_1:100
:: deftheorem defines unity-preserving GROUP_1:def 17 :