let n, m be Nat; for M being Matrix of n,m,F_Real
for A being linearly-independent Subset of (TOP-REAL m) 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 m) st the_rank_of M = n holds
(Mx2Tran M) " A is linearly-independent
let A be linearly-independent Subset of (TOP-REAL m); ( 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 Bm = MX2FinS (1. (F_Real,m)) as OrdBasis of m -VectSp_over F_Real by MATRLIN2:45;
reconsider A1 = A as Subset of (m -VectSp_over F_Real) by Lm1;
reconsider Bn = MX2FinS (1. (F_Real,n)) as OrdBasis of n -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;
A4:
Mx2Tran (M1,Bn,Bm) is one-to-one
by A1, A3, MATRTOP1:39;
reconsider R = A /\ (rng (Mx2Tran (M1,Bn,Bm))) as Subset of (m -VectSp_over F_Real) ;
A5:
R c= A
by XBOOLE_1:17;
A1 is linearly-independent
by Th7;
then A6:
( dom (Mx2Tran (M1,Bn,Bm)) = [#] (n -VectSp_over F_Real) & R is linearly-independent )
by A5, FUNCT_2:def 1, VECTSP_7:1;
(Mx2Tran (M1,Bn,Bm)) " R is linearly-independent
proof
assume
not
(Mx2Tran (M1,Bn,Bm)) " R is
linearly-independent
;
contradiction
then consider L being
Linear_Combination of
(Mx2Tran (M1,Bn,Bm)) " R such that A7:
Carrier L <> {}
and A8:
Sum L = 0. (n -VectSp_over F_Real)
by RANKNULL:41;
set C =
Carrier L;
A9:
Carrier L c= (Mx2Tran (M1,Bn,Bm)) " R
by VECTSP_6:def 4;
(
(Mx2Tran (M1,Bn,Bm)) .: ((Mx2Tran (M1,Bn,Bm)) " R) = R &
(Mx2Tran (M1,Bn,Bm)) @ L is
Linear_Combination of
(Mx2Tran (M1,Bn,Bm)) .: (Carrier L) )
by FUNCT_1:77, RANKNULL:29, XBOOLE_1:17;
then A10:
(Mx2Tran (M1,Bn,Bm)) @ L is
Linear_Combination of
R
by A9, RELAT_1:123, VECTSP_6:4;
(Mx2Tran (M1,Bn,Bm)) | (Carrier L) is
one-to-one
by A4, FUNCT_1:52;
then A11:
Carrier ((Mx2Tran (M1,Bn,Bm)) @ L) = (Mx2Tran (M1,Bn,Bm)) .: (Carrier L)
by RANKNULL:39;
(Mx2Tran (M1,Bn,Bm)) | ((Mx2Tran (M1,Bn,Bm)) " R) is
one-to-one
by A4, FUNCT_1:52;
then Sum ((Mx2Tran (M1,Bn,Bm)) @ L) =
(Mx2Tran (M1,Bn,Bm)) . (Sum L)
by Th14
.=
0. (m -VectSp_over F_Real)
by A8, RANKNULL:9
;
hence
contradiction
by A6, A7, A11, A10, VECTSP_7:def 1;
verum
end;
then
(Mx2Tran (M1,Bn,Bm)) " A is linearly-independent
by RELAT_1:133;
hence
(Mx2Tran M) " A is linearly-independent
by A3, Th7; verum