environ
vocabularies HIDDEN, NUMBERS, ALGSTR_0, STRUCT_0, SUBSET_1, BINOP_1, RLVECT_1, FUNCT_1, ZFMISC_1, XBOOLE_0, FUNCT_7, RELAT_1, ARYTM_3, COMPLEX1, FUNCT_5, MCART_1, CARD_1, SUPINF_2, ARYTM_1, CARD_3, FINSEQ_1, XXREAL_0, TARSKI, XCMPLX_0, RLSUB_1, REALSET1, NORMSP_1, PRE_TOPC, REAL_1, FUNCOP_1, NAT_1, SEQ_2, ORDINAL2, CLVECT_1, NORMSP_0, METRIC_1, RELAT_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, DOMAIN_1, COMPLEX1, REAL_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, BINOP_1, REALSET1, FINSEQ_1, NAT_1, FUNCT_3, FUNCT_5, FINSEQ_4, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, SEQ_2, NORMSP_0, NORMSP_1;
definitions STRUCT_0, RLVECT_1, TARSKI, XBOOLE_0, ALGSTR_0, NORMSP_0;
theorems STRUCT_0, TARSKI, RLVECT_1, COMPLEX1, XCMPLX_0, FINSEQ_1, NAT_1, FUNCT_1, XBOOLE_0, FUNCT_2, RELAT_1, XBOOLE_1, ZFMISC_1, RELSET_1, ABSVALUE, SEQ_2, FUNCOP_1, XREAL_1, XXREAL_0, NORMSP_1, ALGSTR_0, NORMSP_0, ORDINAL1;
schemes FUNCT_2, NAT_1, XBOOLE_0;
registrations SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REALSET1, STRUCT_0, ALGSTR_0, FINSEQ_1, CARD_1, NORMSP_0, NAT_1;
constructors HIDDEN, BINOP_1, FUNCOP_1, REAL_1, COMPLEX1, SEQ_2, REALSET1, NORMSP_1, FUNCT_3, FUNCT_5, RELSET_1, FINSEQ_4, COMSEQ_2;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities STRUCT_0, XBOOLE_0, BINOP_1, REALSET1, ALGSTR_0, COMPLEX1, NORMSP_0;
expansions STRUCT_0, RLVECT_1, TARSKI, XBOOLE_0, NORMSP_0;
Lm1:
for V being non empty addLoopStr holds Sum (<*> the carrier of V) = 0. V
Lm2:
for V being non empty addLoopStr
for F being FinSequence of the carrier of V st len F = 0 holds
Sum F = 0. V
Lm3:
for V being ComplexLinearSpace
for V1 being Subset of V
for W being Subspace of V st the carrier of W = V1 holds
V1 is linearly-closed
Lm4:
now for V being ComplexLinearSpace
for V1 being Subset of V
for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [:COMPLEX,D:],D
for z being Complex
for w being VECTOR of CLSStruct(# D,d1,A,M #)
for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds
z * w = z * v
let V be
ComplexLinearSpace;
for V1 being Subset of V
for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [:COMPLEX,D:],D
for z being Complex
for w being VECTOR of CLSStruct(# D,d1,A,M #)
for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds
z * w = z * vlet V1 be
Subset of
V;
for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [:COMPLEX,D:],D
for z being Complex
for w being VECTOR of CLSStruct(# D,d1,A,M #)
for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds
z * w = z * vlet D be non
empty set ;
for d1 being Element of D
for A being BinOp of D
for M being Function of [:COMPLEX,D:],D
for z being Complex
for w being VECTOR of CLSStruct(# D,d1,A,M #)
for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds
z * w = z * vlet d1 be
Element of
D;
for A being BinOp of D
for M being Function of [:COMPLEX,D:],D
for z being Complex
for w being VECTOR of CLSStruct(# D,d1,A,M #)
for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds
z * w = z * vlet A be
BinOp of
D;
for M being Function of [:COMPLEX,D:],D
for z being Complex
for w being VECTOR of CLSStruct(# D,d1,A,M #)
for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds
z * w = z * vlet M be
Function of
[:COMPLEX,D:],
D;
for z being Complex
for w being VECTOR of CLSStruct(# D,d1,A,M #)
for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds
z * w = z * vlet z be
Complex;
for w being VECTOR of CLSStruct(# D,d1,A,M #)
for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds
z * w = z * vlet w be
VECTOR of
CLSStruct(#
D,
d1,
A,
M #);
for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds
z * w = z * vlet v be
Element of
V;
( V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v implies z * w = z * v )assume that A1:
V1 = D
and A2:
M = the
Mult of
V | [:COMPLEX,V1:]
and A3:
w = v
;
z * w = z * v
z in COMPLEX
by XCMPLX_0:def 2;
then
[z,w] in [:COMPLEX,V1:]
by A1, ZFMISC_1:def 2;
hence
z * w = z * v
by A3, A2, FUNCT_1:49;
verum
end;
Lm5:
for V being ComplexLinearSpace
for W being Subspace of V holds (0. V) + W = the carrier of W
Lm6:
for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( v in W iff v + W = the carrier of W )
deffunc H1( CNORMSTR ) -> Element of the carrier of $1 = 0. $1;
set V = the ComplexLinearSpace;
Lm7:
the carrier of ((0). the ComplexLinearSpace) = {(0. the ComplexLinearSpace)}
by Def9;
reconsider niltonil = the carrier of ((0). the ComplexLinearSpace) --> (In (0,REAL)) as Function of the carrier of ((0). the ComplexLinearSpace),REAL ;
0. the ComplexLinearSpace is VECTOR of ((0). the ComplexLinearSpace)
by Lm7, TARSKI:def 1;
then Lm8:
niltonil . (0. the ComplexLinearSpace) = 0
by FUNCOP_1:7;
Lm9:
for u being VECTOR of ((0). the ComplexLinearSpace)
for z being Complex holds niltonil . (z * u) = |.z.| * (niltonil . u)
Lm10:
for u, v being VECTOR of ((0). the ComplexLinearSpace) holds niltonil . (u + v) <= (niltonil . u) + (niltonil . v)
reconsider X = CNORMSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),niltonil #) as non empty CNORMSTR ;