let n, m be Nat; for M being Matrix of n,m,F_Real
for A being linearly-independent Subset of (TOP-REAL n) st the_rank_of M = n holds
(Mx2Tran M) .: A is linearly-independent
let M be Matrix of n,m,F_Real; for A being linearly-independent Subset of (TOP-REAL n) st the_rank_of M = n holds
(Mx2Tran M) .: A is linearly-independent
let A be linearly-independent Subset of (TOP-REAL n); ( the_rank_of M = n implies (Mx2Tran M) .: A is linearly-independent )
assume A1:
the_rank_of M = n
; (Mx2Tran M) .: A is linearly-independent
set nV = n -VectSp_over F_Real;
set mV = m -VectSp_over F_Real;
reconsider Bn = MX2FinS (1. (F_Real,n)) as OrdBasis of n -VectSp_over F_Real by MATRLIN2:45;
reconsider Bm = MX2FinS (1. (F_Real,m)) as OrdBasis of m -VectSp_over F_Real by MATRLIN2:45;
A2:
len Bm = m
by MATRTOP1:19;
len Bn = n
by MATRTOP1:19;
then reconsider M1 = M as Matrix of len Bn, len Bm,F_Real by A2;
set MT = Mx2Tran (M1,Bn,Bm);
A3:
Mx2Tran M = Mx2Tran (M1,Bn,Bm)
by MATRTOP1:20;
reconsider A1 = A as Subset of (n -VectSp_over F_Real) by Lm1;
A4:
A1 is linearly-independent
by Th7;
(Mx2Tran (M1,Bn,Bm)) .: A1 is linearly-independent
proof
assume
not
(Mx2Tran (M1,Bn,Bm)) .: A1 is
linearly-independent
;
contradiction
then consider L being
Linear_Combination of
(Mx2Tran (M1,Bn,Bm)) .: A1 such that A5:
Carrier L <> {}
and A6:
Sum L = 0. (m -VectSp_over F_Real)
by RANKNULL:41;
A7:
Mx2Tran (
M1,
Bn,
Bm) is
one-to-one
by A1, A3, MATRTOP1:39;
then A8:
ker (Mx2Tran (M1,Bn,Bm)) = (0). (n -VectSp_over F_Real)
by RANKNULL:15;
A9:
(Mx2Tran (M1,Bn,Bm)) | A1 is
one-to-one
by A7, FUNCT_1:52;
then A10:
(Mx2Tran (M1,Bn,Bm)) @ ((Mx2Tran (M1,Bn,Bm)) # L) = L
by RANKNULL:43;
(Mx2Tran (M1,Bn,Bm)) | (Carrier ((Mx2Tran (M1,Bn,Bm)) # L)) is
one-to-one
by A7, FUNCT_1:52;
then
(Mx2Tran (M1,Bn,Bm)) .: (Carrier ((Mx2Tran (M1,Bn,Bm)) # L)) = Carrier L
by A10, RANKNULL:39;
then A11:
Carrier ((Mx2Tran (M1,Bn,Bm)) # L) <> {}
by A5;
(Mx2Tran (M1,Bn,Bm)) . (Sum ((Mx2Tran (M1,Bn,Bm)) # L)) = 0. (m -VectSp_over F_Real)
by A6, A9, A10, Th14;
then
Sum ((Mx2Tran (M1,Bn,Bm)) # L) in ker (Mx2Tran (M1,Bn,Bm))
by RANKNULL:10;
then
Sum ((Mx2Tran (M1,Bn,Bm)) # L) = 0. (n -VectSp_over F_Real)
by A8, VECTSP_4:35;
hence
contradiction
by A4, A11, VECTSP_7:def 1;
verum
end;
hence
(Mx2Tran M) .: A is linearly-independent
by A3, Th7; verum