environ
vocabularies HIDDEN, RLVECT_1, ALGSTR_0, VECTSP_1, XBOOLE_0, SUBSET_1, RELAT_1, ARYTM_1, ARYTM_3, SUPINF_2, XCMPLX_0, COMPLEX1, NUMBERS, CARD_1, SQUARE_1, COMPLFLD, GROUP_1, REAL_1, STRUCT_0, HAHNBAN, FUNCT_1, FUNCOP_1, MSSUBFAM, UNIALG_1, BINOP_1, LATTICES, MESFUNC1, ZFMISC_1, XXREAL_0, RLSUB_1, TARSKI, REALSET1, POWER, HAHNBAN1, FUNCT_7, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, REALSET1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, SQUARE_1, POWER, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, RLSUB_1, VECTSP_4, FUNCT_1, FUNCT_2, BINOP_1, RELSET_1, NATTRA_1, FUNCOP_1, FUNCT_3, HAHNBAN, COMPLFLD, XXREAL_0, GRCAT_1;
definitions TARSKI, RLSUB_1, HAHNBAN, RLVECT_1, VECTSP_1, ALGSTR_0;
theorems TARSKI, ZFMISC_1, ABSVALUE, FUNCT_1, FUNCT_2, COMPLEX1, COMPLFLD, VECTSP_1, FUNCOP_1, RLVECT_1, BINOP_1, HAHNBAN, VECTSP_4, XBOOLE_0, RELAT_1, XCMPLX_1, GROUP_1, XXREAL_0, XCMPLX_0, POWER, ALGSTR_0, XREAL_0;
schemes FUNCT_2, BINOP_1, NAT_1;
registrations XBOOLE_0, FUNCT_1, RELSET_1, NUMBERS, XCMPLX_0, XREAL_0, MEMBERED, STRUCT_0, RLVECT_1, VECTSP_1, COMPLFLD, HAHNBAN, ALGSTR_0, SQUARE_1;
constructors HIDDEN, REAL_1, SQUARE_1, NAT_1, BINOP_2, POWER, REALSET1, RLSUB_1, COMPLFLD, VECTSP_4, NATTRA_1, BORSUK_1, HAHNBAN, SUPINF_1, FUNCOP_1, GRCAT_1;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities SQUARE_1, BINOP_1, RLVECT_1, VECTSP_1, COMPLEX1, STRUCT_0, ALGSTR_0;
expansions TARSKI, VECTSP_1;
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
for
x1,
y1,
x2,
y2 being
Real holds
(x1 + (y1 * <i>)) * (x2 + (y2 * <i>)) = ((x1 * x2) - (y1 * y2)) + (((x1 * y2) + (x2 * y1)) * <i>) ;
definition
let K be non
empty right_complementable Abelian add-associative right_zeroed right-distributive associative commutative doubleLoopStr ;
let V be non
empty ModuleStr over
K;
existence
ex b1 being non empty strict ModuleStr over 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 ModuleStr over 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;
definition
let V be non
empty ModuleStr over
F_Complex ;
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;