let n, m be Nat; for M being Matrix of n,m,F_Real
for A being affinely-independent Subset of (TOP-REAL n) st the_rank_of M = n holds
(Mx2Tran M) .: A is affinely-independent
let M be Matrix of n,m,F_Real; for A being affinely-independent Subset of (TOP-REAL n) st the_rank_of M = n holds
(Mx2Tran M) .: A is affinely-independent
set MT = Mx2Tran M;
set TRn = TOP-REAL n;
set TRm = TOP-REAL m;
let A be affinely-independent Subset of (TOP-REAL n); ( the_rank_of M = n implies (Mx2Tran M) .: A is affinely-independent )
assume A1:
the_rank_of M = n
; (Mx2Tran M) .: A is affinely-independent
per cases
( A is empty or not A is empty )
;
suppose
not
A is
empty
;
(Mx2Tran M) .: A is affinely-independent then consider v being
Element of
(TOP-REAL n) such that A2:
v in A
and A3:
((- v) + A) \ {(0. (TOP-REAL n))} is
linearly-independent
by RLAFFIN1:def 4;
A4:
dom (Mx2Tran M) = [#] (TOP-REAL n)
by FUNCT_2:def 1;
then A5:
(Mx2Tran M) . v in (Mx2Tran M) .: A
by A2, FUNCT_1:def 6;
(Mx2Tran M) . (0. (TOP-REAL n)) = 0. (TOP-REAL m)
by MATRTOP1:29;
then A6:
{(0. (TOP-REAL m))} =
Im (
(Mx2Tran M),
(0. (TOP-REAL n)))
by A4, FUNCT_1:59
.=
(Mx2Tran M) .: {(0. (TOP-REAL n))}
by RELAT_1:def 16
;
- v = (0. (TOP-REAL n)) - v
by RLVECT_1:14;
then A7:
(Mx2Tran M) . (- v) =
((Mx2Tran M) . (0. (TOP-REAL n))) - ((Mx2Tran M) . v)
by MATRTOP1:28
.=
(0. (TOP-REAL m)) - ((Mx2Tran M) . v)
by MATRTOP1:29
.=
- ((Mx2Tran M) . v)
by RLVECT_1:14
;
Mx2Tran M is
one-to-one
by A1, MATRTOP1:39;
then A8:
(Mx2Tran M) .: (((- v) + A) \ {(0. (TOP-REAL n))}) =
((Mx2Tran M) .: ((- v) + A)) \ ((Mx2Tran M) .: {(0. (TOP-REAL n))})
by FUNCT_1:64
.=
((- ((Mx2Tran M) . v)) + ((Mx2Tran M) .: A)) \ {(0. (TOP-REAL m))}
by A6, A7, MATRTOP1:30
;
(Mx2Tran M) .: (((- v) + A) \ {(0. (TOP-REAL n))}) is
linearly-independent
by A1, A3, Th23;
hence
(Mx2Tran M) .: A is
affinely-independent
by A5, A8, RLAFFIN1:def 4;
verum end;