let n, m be Nat; :: thesis: for M being Matrix of n,m,F_Real
for f being n -element real-valued FinSequence ex L being m -element FinSequence of REAL st
( |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| & ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) )
let M be Matrix of n,m,F_Real; :: thesis: for f being n -element real-valued FinSequence ex L being m -element FinSequence of REAL st
( |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| & ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) )
let f be n -element real-valued FinSequence; :: thesis: ex L being m -element FinSequence of REAL st
( |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| & ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) )
set Lf = LineVec2Mx (@ f);
set LfM = (LineVec2Mx (@ f)) * M;
set LM = Line (((LineVec2Mx (@ f)) * M),1);
deffunc H₁( Nat) -> object = |.(@ (Col (M,$1))).|;
consider L being FinSequence such that
A1: ( len L = m & ( for k being Nat st k in dom L holds
L . k = H₁(k) ) ) from FINSEQ_1:sch 2();
rng L c= REAL

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng L or y in REAL )
assume y in rng L ; :: thesis: y in REAL
then consider x being object such that
A2: x in dom L and
A3: L . x = y by FUNCT_1:def 3;
reconsider x = x as Nat by A2;
L . x = H₁(x) by A1, A2;
hence y in REAL by A3, XREAL_0:def 1; :: thesis: verum

end;

then L is FinSequence of REAL by FINSEQ_1:def 4;
then reconsider L1 = L as Element of m -tuples_on REAL by A1, FINSEQ_2:92;
take L1 ; :: thesis: ( |.((Mx2Tran M) . f).| <= (Sum L1) * |.f.| & ( for i being Nat st i in dom L1 holds
L1 . i = |.(@ (Col (M,i))).| ) )

per cases ( n <> 0 or n = 0 ) ;

suppose A4: n <> 0 ; :: thesis: ( |.((Mx2Tran M) . f).| <= (Sum L1) * |.f.| & ( for i being Nat st i in dom L1 holds
L1 . i = |.(@ (Col (M,i))).| ) )

then A5: len M = n by MATRIX13:1;
(Mx2Tran M) . f = Line (((LineVec2Mx (@ f)) * M),1) by A4, Def3;
then A6: len (Line (((LineVec2Mx (@ f)) * M),1)) = m by CARD_1:def 7;
A7: |.((Mx2Tran M) . f).| = sqrt (Sum (sqr (@ (Line (((LineVec2Mx (@ f)) * M),1))))) by A4, Def3;
reconsider LM = Line (((LineVec2Mx (@ f)) * M),1) as Element of m -tuples_on REAL by A6, FINSEQ_2:92;
len (abs LM) = m by CARD_1:def 7;
then reconsider aLM = abs LM as Element of m -tuples_on REAL by FINSEQ_2:92;
A8: len f = n by CARD_1:def 7;
then A9: width (LineVec2Mx (@ f)) = n by MATRIX13:1;
width M = m by A4, MATRIX13:1;
then A10: width ((LineVec2Mx (@ f)) * M) = m by A5, A9, MATRIX_3:def 4;
len (LineVec2Mx (@ f)) = 1 by MATRIX13:1;
then A11: len ((LineVec2Mx (@ f)) * M) = 1 by A5, A9, MATRIX_3:def 4;

now :: thesis: for i being Nat st i in Seg m holds
aLM . i <= (|.f.| * L1) . i

let i be Nat; :: thesis: ( i in Seg m implies aLM . i <= (|.f.| * L1) . i )
A12: len (Col (M,i)) = n by A5, MATRIX_0:def 8;
then A13: |.|(f,(@ (Col (M,i))))|.| <= |.f.| * H₁(i) by A8, EUCLID_2:15;
assume A14: i in Seg m ; :: thesis: aLM . i <= (|.f.| * L1) . i
then A15: ( 1 <= i & i <= m ) by FINSEQ_1:1;
then A16: [1,i] in Indices ((LineVec2Mx (@ f)) * M) by A11, A10, MATRIX_0:30;
i in dom L by A1, A15, FINSEQ_3:25;
then A17: L . i = H₁(i) by A1;
LM . i = ((LineVec2Mx (@ f)) * M) * (1,i) by A10, A14, MATRIX_0:def 7
.= (Line ((LineVec2Mx (@ f)),1)) "*" (Col (M,i)) by A5, A9, A16, MATRIX_3:def 4
.= Sum (mlt ((@ f),(Col (M,i)))) by MATRIX15:25
.= Sum (mlt (f,(@ (Col (M,i))))) by A8, A12, MATRPROB:35, MATRPROB:36
.= |(f,(@ (Col (M,i))))| by RVSUM_1:def 16 ;
then aLM . i <= |.f.| * H₁(i) by A13, VALUED_1:18;
hence aLM . i <= (|.f.| * L1) . i by A17, RVSUM_1:44; :: thesis: verum

end;

then A18: Sum aLM <= Sum (|.f.| * L1) by RVSUM_1:82;
sqr LM = LM (#) LM by VALUED_1:def 8;
then sqrt (Sum (sqr LM)) <= Sum (sqrt (sqr LM)) by Th5;
then ( Sum (|.f.| * L1) = |.f.| * (Sum L1) & sqrt (Sum (sqr LM)) <= Sum aLM ) by Th4, RVSUM_1:87;
hence ( |.((Mx2Tran M) . f).| <= (Sum L1) * |.f.| & ( for i being Nat st i in dom L1 holds
L1 . i = |.(@ (Col (M,i))).| ) ) by A7, A1, A18, XXREAL_0:2; :: thesis: verum

end;

suppose A19: n = 0 ; :: thesis: ( |.((Mx2Tran M) . f).| <= (Sum L1) * |.f.| & ( for i being Nat st i in dom L1 holds
L1 . i = |.(@ (Col (M,i))).| ) )

now :: thesis: for i being Nat st i in dom L1 holds
0 <= L1 . i

let i be Nat; :: thesis: ( i in dom L1 implies 0 <= L1 . i )
assume i in dom L1 ; :: thesis: 0 <= L1 . i
then L1 . i = |.(@ (Col (M,i))).| by A1;
hence 0 <= L1 . i ; :: thesis: verum

end;

then A20: Sum L1 >= 0 by RVSUM_1:84;
|.((Mx2Tran M) . f).| = |.(0. (TOP-REAL m)).| by A19, Def3
.= 0 by EUCLID_2:39 ;
hence ( |.((Mx2Tran M) . f).| <= (Sum L1) * |.f.| & ( for i being Nat st i in dom L1 holds
L1 . i = |.(@ (Col (M,i))).| ) ) by A1, A20; :: thesis: verum

end;

end;