begin
:: 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
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
:: 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
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem VECTSP_1:def 21 :
canceled;
:: deftheorem Def22 defines " VECTSP_1:def 22 :
:: deftheorem defines / VECTSP_1:def 23 :
theorem
canceled;
theorem
canceled;
theorem Th36:
theorem
canceled;
theorem
canceled;
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem
theorem Th44:
theorem
:: 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 ;
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;
( 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
( 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
( 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
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
verum
end;
Lm5:
now
let F be non
empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
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
for v, w being Element of 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;
( MLT = the multF of F implies for x, y being Element of
for v, w being Element of 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
;
for x, y being Element of
for v, w being Element of 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 x,
y be
Element of ;
for v, w being Element of 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 v,
w be
Element of ;
( 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 ;
thus x * (v + w) =
x * (v' + w')
by A1
.=
(x * v') + (x * w')
by Def18
.=
(x * v) + (x * w)
by A1
;
( (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
;
( (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
;
(1. F) * v = vthus (1. F) * v =
(1. F) * v'
by A1
.=
v
by Def19
;
verum
end;
:: deftheorem Def26 defines VectSp-like VECTSP_1:def 26 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th59:
theorem
theorem
canceled;
theorem
canceled;
theorem
Lm6:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of holds - (w + (- v)) = v - w
Lm7:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of holds - ((- v) - w) = w + v
theorem
theorem
theorem Th66:
theorem
theorem Th68:
theorem Th69:
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th78:
:: deftheorem VECTSP_1:def 27 :
canceled;
:: deftheorem Def28 defines Fanoian VECTSP_1:def 28 :
:: deftheorem Def29 defines Fanoian VECTSP_1:def 29 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem Th86:
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
begin
theorem
theorem