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 :
for x, y being real number holds [**x,y**] = x + (y * <i> );
:: deftheorem defines i_FC HAHNBAN1:def 2 :
i_FC = <i> ;
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 :
for K being non empty addLoopStr
for V being non empty VectSpStr of K
for f, g, b5 being Functional of V holds
( b5 = f + g iff for x being Element of V holds b5 . x = (f . x) + (g . x) );
:: deftheorem Def7 defines - HAHNBAN1:def 7 :
for K being non empty addLoopStr
for V being non empty VectSpStr of K
for f, b4 being Functional of V holds
( b4 = - f iff for x being Element of V holds b4 . x = - (f . x) );
:: deftheorem defines - HAHNBAN1:def 8 :
for K being non empty addLoopStr
for V being non empty VectSpStr of K
for f, g being Functional of V holds f - g = f + (- g);
:: deftheorem Def9 defines * HAHNBAN1:def 9 :
for K being non empty multMagma
for V being non empty VectSpStr of K
for v being Element of K
for f, b5 being Functional of V holds
( b5 = v * f iff for x being Element of V holds b5 . x = v * (f . x) );
:: deftheorem defines 0Functional HAHNBAN1:def 10 :
for K being non empty ZeroStr
for V being VectSpStr of K holds 0Functional V = ([#] V) --> (0. K);
:: deftheorem HAHNBAN1:def 11 :
canceled;
:: deftheorem Def12 defines homogeneous HAHNBAN1:def 12 :
for K being non empty multMagma
for V being non empty VectSpStr of K
for F being Functional of V holds
( F is homogeneous iff for x being Vector of V
for r being Scalar of holds F . (r * x) = r * (F . x) );
:: deftheorem defines 0-preserving HAHNBAN1:def 13 :
for K being non empty ZeroStr
for V being non empty VectSpStr of K
for F being Functional of V holds
( F is 0-preserving iff F . (0. V) = 0. K );
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 :
for K being non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive doubleLoopStr
for V being non empty VectSpStr of K
for b3 being non empty strict VectSpStr of K holds
( b3 = V *' iff ( ( for x being set holds
( x in the carrier of b3 iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of b3 . f,g = f + g ) & 0. b3 = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of b3 . x,f = x * f ) ) );
begin
:: deftheorem HAHNBAN1:def 15 :
canceled;
:: deftheorem Def16 defines subadditive HAHNBAN1:def 16 :
for K being 1-sorted
for V being non empty VectSpStr of K
for F being RFunctional of V holds
( F is subadditive iff for x, y being Vector of V holds F . (x + y) <= (F . x) + (F . y) );
:: deftheorem Def17 defines additive HAHNBAN1:def 17 :
for K being 1-sorted
for V being non empty VectSpStr of K
for F being RFunctional of V holds
( F is additive iff for x, y being Vector of V holds F . (x + y) = (F . x) + (F . y) );
:: deftheorem Def18 defines Real_homogeneous HAHNBAN1:def 18 :
for V being non empty VectSpStr of F_Complex
for F being RFunctional of V holds
( F is Real_homogeneous iff for v being Vector of V
for r being Real holds F . ([**r,0 **] * v) = r * (F . v) );
theorem Th29:
:: deftheorem Def19 defines homogeneous HAHNBAN1:def 19 :
for V being non empty VectSpStr of F_Complex
for F being RFunctional of V holds
( F is homogeneous iff for v being Vector of V
for r being Scalar of holds F . (r * v) = |.r.| * (F . v) );
:: deftheorem defines 0-preserving HAHNBAN1:def 20 :
for K being 1-sorted
for V being VectSpStr of K
for F being RFunctional of V holds
( F is 0-preserving iff F . (0. V) = 0 );
:: deftheorem defines 0RFunctional HAHNBAN1:def 21 :
for K being 1-sorted
for V being VectSpStr of K holds 0RFunctional V = ([#] V) --> 0 ;
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 :
for V being non empty VectSpStr of F_Complex
for b2 being strict RLSStruct holds
( b2 = RealVS V iff ( 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 ) ) );
theorem Th30:
theorem Th31:
theorem Th32:
:: deftheorem Def23 defines projRe HAHNBAN1:def 23 :
for V being non empty VectSpStr of F_Complex
for l being Functional of V
for b3 being Functional of (RealVS V) holds
( b3 = projRe l iff for i being Element of V holds b3 . i = Re (l . i) );
:: deftheorem Def24 defines projIm HAHNBAN1:def 24 :
for V being non empty VectSpStr of F_Complex
for l being Functional of V
for b3 being Functional of (RealVS V) holds
( b3 = projIm l iff for i being Element of V holds b3 . i = Im (l . i) );
:: deftheorem defines RtoC HAHNBAN1:def 25 :
for V being non empty VectSpStr of F_Complex
for l being Functional of (RealVS V) holds RtoC l = l;
:: deftheorem defines CtoR HAHNBAN1:def 26 :
for V being non empty VectSpStr of F_Complex
for l being RFunctional of V holds CtoR l = l;
:: deftheorem Def27 defines i-shift HAHNBAN1:def 27 :
for V being non empty VectSpStr of F_Complex
for l, b3 being RFunctional of V holds
( b3 = i-shift l iff for v being Element of V holds b3 . v = l . (i_FC * v) );
:: deftheorem Def28 defines prodReIm HAHNBAN1:def 28 :
for V being non empty VectSpStr of F_Complex
for l being Functional of (RealVS V)
for b3 being Functional of V holds
( b3 = prodReIm l iff for v being Element of V holds b3 . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] );
theorem Th33:
theorem
theorem Th35:
theorem
begin
theorem