let n, m be Nat; for M being Matrix of n,m,F_Real st the_rank_of M = n holds
ex L being Real st
( L > 0 & ( for f being n -element real-valued FinSequence holds |.f.| <= L * |.((Mx2Tran M) . f).| ) )
let M be Matrix of n,m,F_Real; ( the_rank_of M = n implies ex L being Real st
( L > 0 & ( for f being n -element real-valued FinSequence holds |.f.| <= L * |.((Mx2Tran M) . f).| ) ) )
assume A1:
the_rank_of M = n
; ex L being Real st
( L > 0 & ( for f being n -element real-valued FinSequence holds |.f.| <= L * |.((Mx2Tran M) . f).| ) )
per cases
( n <> 0 or n = 0 )
;
suppose A2:
n <> 0
;
ex L being Real st
( L > 0 & ( for f being n -element real-valued FinSequence holds |.f.| <= L * |.((Mx2Tran M) . f).| ) )consider N being
Matrix of
m -' n,
m,
F_Real such that A3:
the_rank_of (M ^ N) = m
by A1, Th16;
width M = m
by A2, MATRIX13:1;
then
m - n >= 0
by A1, MATRIX13:74, XREAL_1:48;
then A4:
m - n = m -' n
by XREAL_0:def 2;
then reconsider MN =
M ^ N as
Matrix of
m,
F_Real ;
A5:
dom (id (TOP-REAL m)) = [#] (TOP-REAL m)
;
set mn =
(m -' n) |-> 0;
A6:
(
m = 0 iff
m = 0 )
;
sqr ((m -' n) |-> 0) =
(m -' n) |-> (0 ^2)
by RVSUM_1:56
.=
(m -' n) |-> (0* 0)
;
then A7:
Sum (sqr ((m -' n) |-> 0)) = (m -' n) * 0
by RVSUM_1:80;
set MN1 =
MN ~ ;
consider L being
Real such that A8:
L > 0
and A9:
for
f being
m -element real-valued FinSequence holds
|.((Mx2Tran (MN ~)) . f).| <= L * |.f.|
by Th45;
take
L
;
( L > 0 & ( for f being n -element real-valued FinSequence holds |.f.| <= L * |.((Mx2Tran M) . f).| ) )thus
L > 0
by A8;
for f being n -element real-valued FinSequence holds |.f.| <= L * |.((Mx2Tran M) . f).|let f be
n -element real-valued FinSequence;
|.f.| <= L * |.((Mx2Tran M) . f).|set fm =
f ^ ((m -' n) |-> 0);
set Mfm =
(Mx2Tran MN) . (f ^ ((m -' n) |-> 0));
A10:
(Mx2Tran MN) . (f ^ ((m -' n) |-> 0)) = (Mx2Tran M) . f
by A4, Th35;
Det MN <> 0. F_Real
by A3, MATRIX13:83;
then A11:
MN is
invertible
by LAPLACE:34;
A12:
width MN = m
by MATRIX_0:24;
reconsider MN2 =
MN ~ as
Matrix of
width MN,
m,
F_Real by A12;
A13:
(
width (MN ~) = m &
len MN = m )
by MATRIX_0:24;
A14:
(Mx2Tran (MN ~)) * (Mx2Tran MN) =
(Mx2Tran MN2) * (Mx2Tran MN)
by MATRIX_0:24
.=
Mx2Tran (MN * MN2)
by A6, Th32
.=
Mx2Tran (1. (F_Real,m))
by A11, A13, MATRIX14:18
.=
id (TOP-REAL m)
by Th33
;
sqr (f ^ ((m -' n) |-> 0)) = (sqr f) ^ (sqr ((m -' n) |-> 0))
by RVSUM_1:144;
then Sum (sqr (f ^ ((m -' n) |-> 0))) =
(Sum (sqr f)) + (Sum (sqr ((m -' n) |-> 0)))
by RVSUM_1:75
.=
Sum (sqr f)
by A7
;
then A15:
|.(f ^ ((m -' n) |-> 0)).| = |.f.|
;
A16:
f ^ ((m -' n) |-> 0) is
Point of
(TOP-REAL m)
by A4, Lm2;
then f ^ ((m -' n) |-> 0) =
(id (TOP-REAL m)) . (f ^ ((m -' n) |-> 0))
.=
(Mx2Tran (MN ~)) . ((Mx2Tran MN) . (f ^ ((m -' n) |-> 0)))
by A16, A14, A5, FUNCT_1:12
;
hence
|.f.| <= L * |.((Mx2Tran M) . f).|
by A9, A10, A15;
verum end;