begin
Lm1:
for F being non empty right_complementable Abelian add-associative right_zeroed right-distributive doubleLoopStr
for x, y being Element of F holds x * (- y) = - (x * y)
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem Th5:
begin
:: deftheorem defines [** HAHNBAN1:def 1 :
:: deftheorem defines i_FC HAHNBAN1:def 2 :
theorem
canceled;
theorem
canceled;
theorem Th8:
theorem Th9:
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
begin
:: deftheorem HAHNBAN1:def 3 :
canceled;
:: deftheorem HAHNBAN1:def 4 :
canceled;
:: deftheorem HAHNBAN1:def 5 :
canceled;
:: deftheorem Def6 defines + HAHNBAN1:def 6 :
:: deftheorem Def7 defines - HAHNBAN1:def 7 :
:: deftheorem defines - HAHNBAN1:def 8 :
:: deftheorem Def9 defines * HAHNBAN1:def 9 :
:: deftheorem defines 0Functional HAHNBAN1:def 10 :
:: deftheorem Def11 defines additive HAHNBAN1:def 11 :
:: deftheorem Def12 defines homogeneous HAHNBAN1:def 12 :
:: deftheorem defines 0-preserving HAHNBAN1:def 13 :
theorem
canceled;
theorem
canceled;
theorem Th20:
theorem Th21:
theorem
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
begin
definition
let K be non
empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive doubleLoopStr ;
let V be non
empty VectSpStr of
K;
func V *' -> non
empty strict VectSpStr of
K means :
Def14:
( ( for
x being
set holds
(
x in the
carrier of
it iff
x is
linear-Functional of
V ) ) & ( for
f,
g being
linear-Functional of
V holds the
addF of
it . f,
g = f + g ) &
0. it = 0Functional V & ( for
f being
linear-Functional of
V for
x being
Element of
K holds the
lmult of
it . x,
f = x * f ) );
existence
ex b1 being non empty strict VectSpStr of K st
( ( for x being set holds
( x in the carrier of b1 iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of b1 . f,g = f + g ) & 0. b1 = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of b1 . x,f = x * f ) )
uniqueness
for b1, b2 being non empty strict VectSpStr of K st ( for x being set holds
( x in the carrier of b1 iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of b1 . f,g = f + g ) & 0. b1 = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of b1 . x,f = x * f ) & ( for x being set holds
( x in the carrier of b2 iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of b2 . f,g = f + g ) & 0. b2 = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of b2 . x,f = x * f ) holds
b1 = b2
end;
:: deftheorem Def14 defines *' HAHNBAN1:def 14 :
begin
:: deftheorem HAHNBAN1:def 15 :
canceled;
:: deftheorem Def16 defines subadditive HAHNBAN1:def 16 :
:: deftheorem Def17 defines additive HAHNBAN1:def 17 :
:: deftheorem Def18 defines Real_homogeneous HAHNBAN1:def 18 :
theorem Th29:
:: deftheorem Def19 defines homogeneous HAHNBAN1:def 19 :
:: deftheorem defines 0-preserving HAHNBAN1:def 20 :
:: deftheorem defines 0RFunctional HAHNBAN1:def 21 :
begin
definition
let V be non
empty VectSpStr of
F_Complex ;
func RealVS V -> strict RLSStruct means :
Def22:
(
addLoopStr(# the
carrier of
it,the
addF of
it,the
ZeroF of
it #)
= addLoopStr(# the
carrier of
V,the
addF of
V,the
ZeroF of
V #) & ( for
r being
Real for
v being
Vector of
V holds the
Mult of
it . r,
v = [**r,0 **] * v ) );
existence
ex b1 being strict RLSStruct st
( addLoopStr(# the carrier of b1,the addF of b1,the ZeroF of b1 #) = addLoopStr(# the carrier of V,the addF of V,the ZeroF of V #) & ( for r being Real
for v being Vector of V holds the Mult of b1 . r,v = [**r,0 **] * v ) )
uniqueness
for b1, b2 being strict RLSStruct st addLoopStr(# the carrier of b1,the addF of b1,the ZeroF of b1 #) = addLoopStr(# the carrier of V,the addF of V,the ZeroF of V #) & ( for r being Real
for v being Vector of V holds the Mult of b1 . r,v = [**r,0 **] * v ) & addLoopStr(# the carrier of b2,the addF of b2,the ZeroF of b2 #) = addLoopStr(# the carrier of V,the addF of V,the ZeroF of V #) & ( for r being Real
for v being Vector of V holds the Mult of b2 . r,v = [**r,0 **] * v ) holds
b1 = b2
end;
:: deftheorem Def22 defines RealVS HAHNBAN1:def 22 :
theorem Th30:
theorem Th31:
theorem Th32:
:: deftheorem Def23 defines projRe HAHNBAN1:def 23 :
:: deftheorem Def24 defines projIm HAHNBAN1:def 24 :
:: deftheorem defines RtoC HAHNBAN1:def 25 :
:: deftheorem defines CtoR HAHNBAN1:def 26 :
:: deftheorem Def27 defines i-shift HAHNBAN1:def 27 :
:: deftheorem Def28 defines prodReIm HAHNBAN1:def 28 :
theorem Th33:
theorem
theorem Th35:
theorem
begin
theorem