let G be non-trivial RealNormSpace-Sequence; :: thesis: for S being non trivial RealNormSpace
for f being PartFunc of (product G),S
for x being Point of (product G) ex L being bounded LinearOperator of (product G),S st
for h being Element of (product G) ex w being FinSequence of S st
( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . h) ) & L . h = Sum w )
let S be non trivial RealNormSpace; :: thesis: for f being PartFunc of (product G),S
for x being Point of (product G) ex L being bounded LinearOperator of (product G),S st
for h being Element of (product G) ex w being FinSequence of S st
( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . h) ) & L . h = Sum w )
let f be PartFunc of (product G),S; :: thesis: for x being Point of (product G) ex L being bounded LinearOperator of (product G),S st
for h being Element of (product G) ex w being FinSequence of S st
( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . h) ) & L . h = Sum w )
let x be Point of (product G); :: thesis: ex L being bounded LinearOperator of (product G),S st
for h being Element of (product G) ex w being FinSequence of S st
( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . h) ) & L . h = Sum w )
set m = len G;
defpred S1[ set , set ] means ex w being FinSequence of S st
( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . $1) ) & $2 = Sum w );
A1: for v being Element of (product G) ex y being Element of S st S1[v,y]
proof
let v be Element of (product G); :: thesis: ex y being Element of S st S1[v,y]
defpred S2[ set , set ] means ex i being Element of NAT st
( i = $1 & $2 = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . v) );
A2: for i being Nat st i in Seg (len G) holds
ex r being Element of S st S2[i,r]
proof
let i be Nat; :: thesis: ( i in Seg (len G) implies ex r being Element of S st S2[i,r] )
assume i in Seg (len G) ; :: thesis: ex r being Element of S st S2[i,r]
reconsider i0 = i as Element of NAT by ORDINAL1:def 12;
(partdiff (f,x,i0)) . ((proj (modetrans (G,i0))) . v) in the carrier of S ;
hence ex r being Element of S st S2[i,r] ; :: thesis: verum
end;
consider w being FinSequence of S such that
A3: ( dom w = Seg (len G) & ( for i being Nat st i in Seg (len G) holds
S2[i,w . i] ) ) from FINSEQ_1:sch 5(A2);
A4: now
let i be Element of NAT ; :: thesis: ( i in Seg (len G) implies w . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . v) )
assume i in Seg (len G) ; :: thesis: w . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . v)
then S2[i,w . i] by A3;
hence w . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . v) ; :: thesis: verum
end;
reconsider w0 = Sum w as Element of S ;
ex w being FinSequence of S st
( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . v) ) & w0 = Sum w ) by A4, A3;
hence ex y0 being Element of S st S1[v,y0] ; :: thesis: verum
end;
consider L being Function of (product G),S such that
A5: for h being Element of (product G) holds S1[h,L . h] from FUNCT_2:sch 3(A1);
 A6: for s, t being Element of (product G) holds L . (s + t) = (L . s) + (L . t)
proof
let s, t be Element of (product G); :: thesis: L . (s + t) = (L . s) + (L . t)
consider w being FinSequence of S such that
A7: ( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . s) ) & L . s = Sum w ) by A5;
consider v being FinSequence of S such that
A8: ( dom v = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
v . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . t) ) & L . t = Sum v ) by A5;
consider u being FinSequence of S such that
A9: ( dom u = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
u . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . (s + t)) ) & L . (s + t) = Sum u ) by A5;
B1: len w = len G by A7, FINSEQ_1:def 3;
B2: len v = len G by A8, FINSEQ_1:def 3;
B3: len u = len G by A9, FINSEQ_1:def 3;
now
let i be Element of NAT ; :: thesis: ( i in dom w implies u . i = (w /. i) + (v /. i) )
assume A11: i in dom w ; :: thesis: u . i = (w /. i) + (v /. i)
then A12: ( 1 <= i & i <= len G ) by A7, FINSEQ_1:1;
then w /. i = w . i by B1, FINSEQ_4:15;
then A13: w /. i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . s) by A7, A11;
v /. i = v . i by A12, B2, FINSEQ_4:15;
then A14: v /. i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . t) by A7, A8, A11;
F1: partdiff (f,x,i) is bounded LinearOperator of (G . (modetrans (G,i))),S by LOPBAN_1:def 9;
u . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . (s + t)) by A7, A9, A11;
then u . i = (partdiff (f,x,i)) . (((proj (modetrans (G,i))) . s) + ((proj (modetrans (G,i))) . t)) by YTh9;
hence u . i = (w /. i) + (v /. i) by A13, A14, F1, GRCAT_1:def 8; :: thesis: verum
end;
hence L . (s + t) = (L . s) + (L . t) by A9, A7, A8, B1, B2, B3, RLVECT_2:2; :: thesis: verum
end;
for s being Element of (product G)
for r being Real holds L . (r * s) = r * (L . s)
proof
let s be Element of (product G); :: thesis: for r being Real holds L . (r * s) = r * (L . s)
let r be Real; :: thesis: L . (r * s) = r * (L . s)
consider w being FinSequence of S such that
A15: ( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . s) ) & L . s = Sum w ) by A5;
consider u being FinSequence of S such that
A16: ( dom u = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
u . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . (r * s)) ) & L . (r * s) = Sum u ) by A5;
B1: ( len w = len G & len u = len G ) by A15, A16, FINSEQ_1:def 3;
now
let i be Element of NAT ; :: thesis: ( i in dom w implies u . i = r * (w /. i) )
assume A17: i in dom w ; :: thesis: u . i = r * (w /. i)
then ( 1 <= i & i <= len G ) by A15, FINSEQ_1:1;
then w /. i = w . i by B1, FINSEQ_4:15;
then A19: w /. i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . s) by A15, A17;
F1: partdiff (f,x,i) is bounded LinearOperator of (G . (modetrans (G,i))),S by LOPBAN_1:def 9;
u . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . (r * s)) by A15, A16, A17;
then u . i = (partdiff (f,x,i)) . (r * ((proj (modetrans (G,i))) . s)) by YTh16;
hence u . i = r * (w /. i) by A19, F1, LOPBAN_1:def 5; :: thesis: verum
end;
hence L . (r * s) = r * (L . s) by A15, A16, B1, RLVECT_2:3; :: thesis: verum
end;
then reconsider L = L as LinearOperator of (product G),S by A6, GRCAT_1:def 8, LOPBAN_1:def 5;
defpred S2[ set , set ] means ex i being Element of NAT st
( i = $1 & $2 = ||.(partdiff (f,x,i)).|| );
XA2: for i being Nat st i in Seg (len G) holds
ex r being Element of REAL st S2[i,r]
proof
let i be Nat; :: thesis: ( i in Seg (len G) implies ex r being Element of REAL st S2[i,r] )
assume i in Seg (len G) ; :: thesis: ex r being Element of REAL st S2[i,r]
reconsider i0 = i as Element of NAT by ORDINAL1:def 12;
reconsider r = ||.(partdiff (f,x,i0)).|| as Element of REAL ;
S2[i,r] ;
hence ex r being Element of REAL st S2[i,r] ; :: thesis: verum
end;
consider Kw being FinSequence of REAL such that
LK10: ( dom Kw = Seg (len G) & ( for i being Nat st i in Seg (len G) holds
S2[i,Kw . i] ) ) from FINSEQ_1:sch 5(XA2);
LK1: now
let i be Element of NAT ; :: thesis: ( i in Seg (len G) implies Kw . i = ||.(partdiff (f,x,i)).|| )
assume i in Seg (len G) ; :: thesis: Kw . i = ||.(partdiff (f,x,i)).||
then S2[i,Kw . i] by LK10;
hence Kw . i = ||.(partdiff (f,x,i)).|| ; :: thesis: verum
end;
LK20: now
let i be Nat; :: thesis: ( i in dom Kw implies 0 <= Kw . i )
assume i in dom Kw ; :: thesis: 0 <= Kw . i
then Kw . i = ||.(partdiff (f,x,i)).|| by LK1, LK10;
hence 0 <= Kw . i ; :: thesis: verum
end;
set LK = Sum Kw;
LK2: 0 <= Sum Kw by LK20, RVSUM_1:84;
for s being Element of (product G) holds ||.(L . s).|| <= (Sum Kw) * ||.s.||
proof
let s be Element of (product G); :: thesis: ||.(L . s).|| <= (Sum Kw) * ||.s.||
consider w being FinSequence of S such that
H1: ( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . s) ) & L . s = Sum w ) by A5;
defpred S3[ set , set ] means ex i being Element of NAT st
( i = $1 & $2 = ||.(partdiff (f,x,i)).|| * ||.s.|| );
XA3: for i being Nat st i in Seg (len G) holds
ex r being Element of REAL st S3[i,r]
proof
let i be Nat; :: thesis: ( i in Seg (len G) implies ex r being Element of REAL st S3[i,r] )
assume i in Seg (len G) ; :: thesis: ex r being Element of REAL st S3[i,r]
reconsider i0 = i as Element of NAT by ORDINAL1:def 12;
reconsider r = ||.(partdiff (f,x,i0)).|| * ||.s.|| as Element of REAL ;
S3[i,r] ;
hence ex r being Element of REAL st S3[i,r] ; :: thesis: verum
end;
consider Dw being FinSequence of REAL such that
LK30: ( dom Dw = Seg (len G) & ( for i being Nat st i in Seg (len G) holds
S3[i,Dw . i] ) ) from FINSEQ_1:sch 5(XA3);
LK3: now
let i be Element of NAT ; :: thesis: ( i in Seg (len G) implies Dw . i = ||.(partdiff (f,x,i)).|| * ||.s.|| )
assume i in Seg (len G) ; :: thesis: Dw . i = ||.(partdiff (f,x,i)).|| * ||.s.||
then S3[i,Dw . i] by LK30;
hence Dw . i = ||.(partdiff (f,x,i)).|| * ||.s.|| ; :: thesis: verum
end;
defpred S4[ set , set ] means ex i being Element of NAT st
( i = $1 & $2 = ||.(w /. i).|| );
XA4: for i being Nat st i in Seg (len G) holds
ex r being Element of REAL st S4[i,r]
proof
let i be Nat; :: thesis: ( i in Seg (len G) implies ex r being Element of REAL st S4[i,r] )
assume i in Seg (len G) ; :: thesis: ex r being Element of REAL st S4[i,r]
reconsider i0 = i as Element of NAT by ORDINAL1:def 12;
reconsider r = ||.(w /. i0).|| as Element of REAL ;
S4[i,r] ;
hence ex r being Element of REAL st S4[i,r] ; :: thesis: verum
end;
consider yseq being FinSequence of REAL such that
H20: ( dom yseq = Seg (len G) & ( for i being Nat st i in Seg (len G) holds
S4[i,yseq . i] ) ) from FINSEQ_1:sch 5(XA4);
H2: now
let i be Element of NAT ; :: thesis: ( i in Seg (len G) implies yseq . i = ||.(w /. i).|| )
assume i in Seg (len G) ; :: thesis: yseq . i = ||.(w /. i).||
then S4[i,yseq . i] by H20;
hence yseq . i = ||.(w /. i).|| ; :: thesis: verum
end;
len w = len yseq by H1, H20, FINSEQ_3:29;
then H3: ||.(L . s).|| <= Sum yseq by H1, H2, PDIFF617;
len G = len yseq by H20, FINSEQ_1:def 3;
then X1: yseq is Element of (len G) -tuples_on REAL by FINSEQ_2:92;
len Dw = len G by LK30, FINSEQ_1:def 3;
then X1A: Dw is Element of (len G) -tuples_on REAL by FINSEQ_2:92;
now
let i be Nat; :: thesis: ( i in Seg (len G) implies yseq . i <= Dw . i )
assume H40: i in Seg (len G) ; :: thesis: yseq . i <= Dw . i
then H41: yseq . i = ||.(w /. i).|| by H2;
w /. i = w . i by H40, H1, PARTFUN1:def 6;
then H5: ||.(w /. i).|| = ||.((partdiff (f,x,i)) . ((proj (modetrans (G,i))) . s)).|| by H1, H40;
reconsider DF1 = partdiff (f,x,i) as bounded LinearOperator of (G . (modetrans (G,i))),S by LOPBAN_1:def 9;
H6: ||.(DF1 . ((proj (modetrans (G,i))) . s)).|| <= ||.(partdiff (f,x,i)).|| * ||.((proj (modetrans (G,i))) . s).|| by LOPBAN_1:32;
product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by PRVECT_2:6;
then reconsider ss = s as Element of product (carr G) ;
reconsider xi = (proj (modetrans (G,i))) . s as Point of (G . (modetrans (G,i))) ;
xi = ss . (modetrans (G,i)) by Def1;
then ||.(partdiff (f,x,i)).|| * ||.((proj (modetrans (G,i))) . s).|| <= ||.(partdiff (f,x,i)).|| * ||.s.|| by PRVECT_2:10, XREAL_1:64;
then ||.(w /. i).|| <= ||.(partdiff (f,x,i)).|| * ||.s.|| by H5, H6, XXREAL_0:2;
hence yseq . i <= Dw . i by LK3, H40, H41; :: thesis: verum
end;
then H7: Sum yseq <= Sum Dw by X1, X1A, RVSUM_1:82;
len Kw = len G by LK10, FINSEQ_1:def 3;
then reconsider KKw = Kw as Element of (len G) -tuples_on REAL by FINSEQ_2:92;
||.s.|| * KKw in (len G) -tuples_on REAL ;
then ex t being Element of REAL * st
( t = ||.s.|| * KKw & len t = len G ) ;
then Z1: dom Dw = dom (||.s.|| * Kw) by LK30, FINSEQ_1:def 3;
now
let k be Nat; :: thesis: ( k in dom Dw implies Dw . k = (||.s.|| * Kw) . k )
assume Z3: k in dom Dw ; :: thesis: Dw . k = (||.s.|| * Kw) . k
then Dw . k = ||.(partdiff (f,x,k)).|| * ||.s.|| by LK3, LK30;
then Dw . k = ||.s.|| * (Kw . k) by LK1, Z3, LK30;
hence Dw . k = (||.s.|| * Kw) . k by RVSUM_1:45; :: thesis: verum
end;
then Dw = ||.s.|| * Kw by Z1, FINSEQ_1:13;
then Sum Dw = (Sum Kw) * ||.s.|| by RVSUM_1:87;
hence ||.(L . s).|| <= (Sum Kw) * ||.s.|| by H3, H7, XXREAL_0:2; :: thesis: verum
end;
then reconsider L = L as bounded LinearOperator of (product G),S by LK2, LOPBAN_1:def 8;
take L ; :: thesis: for h being Element of (product G) ex w being FinSequence of S st
( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . h) ) & L . h = Sum w )
thus for h being Element of (product G) ex w being FinSequence of S st
( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . h) ) & L . h = Sum w ) by A5; :: thesis: verum