:: Abelian Groups, Fields and Vector Spaces
:: by Eugeniusz Kusak, Wojciech Leo\'nczuk and Micha{\l} Muzalewski
::
:: Received November 23, 1989
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem VECTSP_1:def 1 :
canceled;
:: deftheorem VECTSP_1:def 2 :
canceled;
:: deftheorem VECTSP_1:def 3 :
canceled;
:: deftheorem VECTSP_1:def 4 :
canceled;
:: deftheorem VECTSP_1:def 5 :
canceled;
:: deftheorem defines G_Real VECTSP_1:def 6 :
theorem :: VECTSP_1:1
canceled;
theorem :: VECTSP_1:2
canceled;
theorem :: VECTSP_1:3
canceled;
theorem :: VECTSP_1:4
canceled;
theorem :: VECTSP_1:5
canceled;
theorem :: VECTSP_1:6
:: deftheorem VECTSP_1:def 7 :
canceled;
:: deftheorem VECTSP_1:def 8 :
canceled;
:: deftheorem VECTSP_1:def 9 :
canceled;
:: deftheorem VECTSP_1:def 10 :
canceled;
:: deftheorem Def11 defines right-distributive VECTSP_1:def 11 :
:: deftheorem Def12 defines left-distributive VECTSP_1:def 12 :
:: deftheorem Def13 defines right_unital VECTSP_1:def 13 :
:: deftheorem VECTSP_1:def 14 :
canceled;
:: deftheorem defines F_Real VECTSP_1:def 15 :
:: deftheorem Def16 defines well-unital VECTSP_1:def 16 :
Lm1:
for L being non empty multLoopStr st L is well-unital holds
L is unital
Lm2:
for L being non empty multLoopStr st L is well-unital holds
1. L = 1_ L
:: deftheorem VECTSP_1:def 17 :
canceled;
:: deftheorem Def18 defines distributive VECTSP_1:def 18 :
:: deftheorem Def19 defines left_unital VECTSP_1:def 19 :
:: deftheorem Def20 defines almost_left_invertible VECTSP_1:def 20 :
set FR = F_Real ;
Lm3:
for L being non empty doubleLoopStr st L is distributive holds
( L is right-distributive & L is left-distributive )
theorem :: VECTSP_1:7
canceled;
theorem :: VECTSP_1:8
canceled;
theorem :: VECTSP_1:9
canceled;
theorem :: VECTSP_1:10
canceled;
theorem :: VECTSP_1:11
canceled;
theorem :: VECTSP_1:12
canceled;
theorem :: VECTSP_1:13
canceled;
theorem :: VECTSP_1:14
canceled;
theorem :: VECTSP_1:15
canceled;
theorem :: VECTSP_1:16
canceled;
theorem :: VECTSP_1:17
canceled;
theorem :: VECTSP_1:18
canceled;
theorem :: VECTSP_1:19
canceled;
theorem :: VECTSP_1:20
theorem :: VECTSP_1:21
theorem :: VECTSP_1:22
theorem :: VECTSP_1:23
canceled;
theorem :: VECTSP_1:24
canceled;
theorem :: VECTSP_1:25
canceled;
theorem :: VECTSP_1:26
canceled;
theorem :: VECTSP_1:27
canceled;
theorem :: VECTSP_1:28
canceled;
theorem :: VECTSP_1:29
canceled;
theorem :: VECTSP_1:30
canceled;
theorem :: VECTSP_1:31
canceled;
theorem :: VECTSP_1:32
canceled;
theorem :: VECTSP_1:33
:: deftheorem VECTSP_1:def 21 :
canceled;
:: deftheorem Def22 defines " VECTSP_1:def 22 :
:: deftheorem defines / VECTSP_1:def 23 :
theorem :: VECTSP_1:34
canceled;
theorem :: VECTSP_1:35
canceled;
theorem Th36: :: VECTSP_1:36
theorem :: VECTSP_1:37
canceled;
theorem :: VECTSP_1:38
canceled;
theorem Th39: :: VECTSP_1:39
theorem Th40: :: VECTSP_1:40
theorem Th41: :: VECTSP_1:41
theorem Th42: :: VECTSP_1:42
theorem :: VECTSP_1:43
theorem Th44: :: VECTSP_1:44
theorem :: VECTSP_1:45
:: deftheorem defines * VECTSP_1:def 24 :
:: deftheorem defines comp VECTSP_1:def 25 :
Lm4:
now
let F be non
empty right_complementable Abelian add-associative right_zeroed associative distributive left_unital doubleLoopStr ;
:: thesis: for MLT being Function of [:the carrier of F,the carrier of F:],the carrier of F holds
( VectSpStr(# the carrier of F,the addF of F,(0. F),MLT #) is Abelian & VectSpStr(# the carrier of F,the addF of F,(0. F),MLT #) is add-associative & VectSpStr(# the carrier of F,the addF of F,(0. F),MLT #) is right_zeroed & VectSpStr(# the carrier of F,the addF of F,(0. F),MLT #) is right_complementable )let MLT be
Function of
[:the carrier of F,the carrier of F:],the
carrier of
F;
:: thesis: ( VectSpStr(# the carrier of F,the addF of F,(0. F),MLT #) is Abelian & VectSpStr(# the carrier of F,the addF of F,(0. F),MLT #) is add-associative & VectSpStr(# the carrier of F,the addF of F,(0. F),MLT #) is right_zeroed & VectSpStr(# the carrier of F,the addF of F,(0. F),MLT #) is right_complementable )set GF =
VectSpStr(# the
carrier of
F,the
addF of
F,
(0. F),
MLT #);
thus
VectSpStr(# the
carrier of
F,the
addF of
F,
(0. F),
MLT #) is
Abelian
:: thesis: ( VectSpStr(# the carrier of F,the addF of F,(0. F),MLT #) is add-associative & VectSpStr(# the carrier of F,the addF of F,(0. F),MLT #) is right_zeroed & VectSpStr(# the carrier of F,the addF of F,(0. F),MLT #) is right_complementable )
thus
VectSpStr(# the
carrier of
F,the
addF of
F,
(0. F),
MLT #) is
add-associative
:: thesis: ( VectSpStr(# the carrier of F,the addF of F,(0. F),MLT #) is right_zeroed & VectSpStr(# the carrier of F,the addF of F,(0. F),MLT #) is right_complementable )
thus
VectSpStr(# the
carrier of
F,the
addF of
F,
(0. F),
MLT #) is
right_zeroed
:: thesis: VectSpStr(# the carrier of F,the addF of F,(0. F),MLT #) is right_complementable
thus
VectSpStr(# the
carrier of
F,the
addF of
F,
(0. F),
MLT #) is
right_complementable
:: thesis: verum
proof
let x be
Element of
VectSpStr(# the
carrier of
F,the
addF of
F,
(0. F),
MLT #);
:: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider x' =
x as
Element of
F ;
consider t being
Element of
F such that A1:
x' + t = 0. F
by ALGSTR_0:def 11;
reconsider t' =
t as
Element of
VectSpStr(# the
carrier of
F,the
addF of
F,
(0. F),
MLT #) ;
take
t'
;
:: according to ALGSTR_0:def 11 :: thesis: x + t' = 0. VectSpStr(# the carrier of F,the addF of F,(0. F),MLT #)
thus
x + t' = 0. VectSpStr(# the
carrier of
F,the
addF of
F,
(0. F),
MLT #)
by A1;
:: thesis: verum
end;
end;
Lm5:
now
let F be non
empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
:: thesis: for MLT being Function of [:the carrier of F,the carrier of F:],the carrier of F st MLT = the multF of F holds
for x, y being Element of F
for v, w being Element of VectSpStr(# the carrier of F,the addF of F,(0. F),MLT #) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )let MLT be
Function of
[:the carrier of F,the carrier of F:],the
carrier of
F;
:: thesis: ( MLT = the multF of F implies for x, y being Element of F
for v, w being Element of VectSpStr(# the carrier of F,the addF of F,(0. F),MLT #) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v ) )assume A1:
MLT = the
multF of
F
;
:: thesis: for x, y being Element of F
for v, w being Element of VectSpStr(# the carrier of F,the addF of F,(0. F),MLT #) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )set LS =
VectSpStr(# the
carrier of
F,the
addF of
F,
(0. F),
MLT #);
let x,
y be
Element of
F;
:: thesis: for v, w being Element of VectSpStr(# the carrier of F,the addF of F,(0. F),MLT #) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )let v,
w be
Element of
VectSpStr(# the
carrier of
F,the
addF of
F,
(0. F),
MLT #);
:: thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )reconsider v' =
v,
w' =
w as
Element of
F ;
thus x * (v + w) =
x * (v' + w')
by A1
.=
(x * v') + (x * w')
by Def18
.=
(x * v) + (x * w)
by A1
;
:: thesis: ( (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )thus (x + y) * v =
(x + y) * v'
by A1
.=
(x * v') + (y * v')
by Def18
.=
(x * v) + (y * v)
by A1
;
:: thesis: ( (x * y) * v = x * (y * v) & (1. F) * v = v )thus (x * y) * v =
(x * y) * v'
by A1
.=
x * (y * v')
by GROUP_1:def 4
.=
x * (y * v)
by A1
;
:: thesis: (1. F) * v = vthus (1. F) * v =
(1. F) * v'
by A1
.=
v
by Def19
;
:: thesis: verum
end;
:: deftheorem Def26 defines VectSp-like VECTSP_1:def 26 :
theorem :: VECTSP_1:46
canceled;
theorem :: VECTSP_1:47
canceled;
theorem :: VECTSP_1:48
canceled;
theorem :: VECTSP_1:49
canceled;
theorem :: VECTSP_1:50
canceled;
theorem :: VECTSP_1:51
canceled;
theorem :: VECTSP_1:52
canceled;
theorem :: VECTSP_1:53
canceled;
theorem :: VECTSP_1:54
canceled;
theorem :: VECTSP_1:55
canceled;
theorem :: VECTSP_1:56
canceled;
theorem :: VECTSP_1:57
canceled;
theorem :: VECTSP_1:58
canceled;
theorem Th59: :: VECTSP_1:59
theorem :: VECTSP_1:60
theorem :: VECTSP_1:61
canceled;
theorem :: VECTSP_1:62
canceled;
theorem :: VECTSP_1:63
Lm6:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V holds - (w + (- v)) = v - w
Lm7:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V holds - ((- v) - w) = w + v
theorem :: VECTSP_1:64
theorem :: VECTSP_1:65
theorem Th66: :: VECTSP_1:66
theorem :: VECTSP_1:67
theorem Th68: :: VECTSP_1:68
theorem Th69: :: VECTSP_1:69
theorem :: VECTSP_1:70
theorem :: VECTSP_1:71
canceled;
theorem :: VECTSP_1:72
canceled;
theorem :: VECTSP_1:73
theorem :: VECTSP_1:74
theorem :: VECTSP_1:75
canceled;
theorem :: VECTSP_1:76
canceled;
theorem :: VECTSP_1:77
canceled;
theorem Th78: :: VECTSP_1:78
:: deftheorem VECTSP_1:def 27 :
canceled;
:: deftheorem Def28 defines Fanoian VECTSP_1:def 28 :
:: deftheorem Def29 defines Fanoian VECTSP_1:def 29 :
theorem :: VECTSP_1:79
canceled;
theorem :: VECTSP_1:80
canceled;
theorem :: VECTSP_1:81
canceled;
theorem :: VECTSP_1:82
canceled;
theorem :: VECTSP_1:83
canceled;
theorem :: VECTSP_1:84
theorem :: VECTSP_1:85
canceled;
theorem Th86: :: VECTSP_1:86
theorem :: VECTSP_1:87
theorem :: VECTSP_1:88
theorem :: VECTSP_1:89
theorem :: VECTSP_1:90
theorem :: VECTSP_1:91
canceled;
theorem :: VECTSP_1:92
theorem :: VECTSP_1:93
theorem :: VECTSP_1:94
theorem :: VECTSP_1:95
theorem :: VECTSP_1:96