let m, n be Nat; for M being Matrix of n,m,F_Real
for A being affinely-independent Subset of (TOP-REAL m) 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 m) 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 m); ( the_rank_of M = n implies (Mx2Tran M) " A is affinely-independent )
assume A2:
the_rank_of M = n
; (Mx2Tran M) " A is affinely-independent
reconsider R = A /\ (rng (Mx2Tran M)) as affinely-independent Subset of (TOP-REAL m) by RLAFFIN1:43, XBOOLE_1:17;
A3:
(Mx2Tran M) " A = (Mx2Tran M) " (A /\ (rng (Mx2Tran M)))
by RELAT_1:133;
per cases
( R is empty or not R is empty )
;
suppose
not
R is
empty
;
(Mx2Tran M) " A is affinely-independent then consider v being
Element of
(TOP-REAL m) such that A4:
v in R
and A5:
((- v) + R) \ {(0. (TOP-REAL m))} is
linearly-independent
by RLAFFIN1:def 4;
v in rng (Mx2Tran M)
by A4, XBOOLE_0:def 4;
then consider x being
set such that A6:
x in dom (Mx2Tran M)
and A7:
(Mx2Tran M) . x = v
by FUNCT_1:def 3;
reconsider x =
x as
Element of
(TOP-REAL n) by A6;
- x = (0. (TOP-REAL n)) - x
by RLVECT_1:14;
then A8:
(Mx2Tran M) . (- x) =
((Mx2Tran M) . (0. (TOP-REAL n))) - ((Mx2Tran M) . x)
by MATRTOP1:28
.=
(0. (TOP-REAL m)) - ((Mx2Tran M) . x)
by MATRTOP1:29
.=
- v
by A7, RLVECT_1:14
;
A9:
dom (Mx2Tran M) = [#] (TOP-REAL n)
by FUNCT_2:def 1;
(Mx2Tran M) . (0. (TOP-REAL n)) = 0. (TOP-REAL m)
by MATRTOP1:29;
then A10:
{(0. (TOP-REAL m))} =
Im (
(Mx2Tran M),
(0. (TOP-REAL n)))
by A9, FUNCT_1:59
.=
(Mx2Tran M) .: {(0. (TOP-REAL n))}
by RELAT_1:def 16
;
Mx2Tran M is
one-to-one
by A2, MATRTOP1:39;
then A11:
(Mx2Tran M) " {(0. (TOP-REAL m))} c= {(0. (TOP-REAL n))}
by A10, FUNCT_1:82;
{(0. (TOP-REAL n))} c= [#] (TOP-REAL n)
by ZFMISC_1:31;
then
{(0. (TOP-REAL n))} c= (Mx2Tran M) " {(0. (TOP-REAL m))}
by A9, A10, FUNCT_1:76;
then
(Mx2Tran M) " {(0. (TOP-REAL m))} = {(0. (TOP-REAL n))}
by A11, XBOOLE_0:def 10;
then (Mx2Tran M) " (((- v) + R) \ {(0. (TOP-REAL m))}) =
((Mx2Tran M) " ((- v) + R)) \ {(0. (TOP-REAL n))}
by FUNCT_1:69
.=
((- x) + ((Mx2Tran M) " R)) \ {(0. (TOP-REAL n))}
by A8, MATRTOP1:31
;
then A12:
((- x) + ((Mx2Tran M) " R)) \ {(0. (TOP-REAL n))} is
linearly-independent
by A2, A5, Th26;
x in (Mx2Tran M) " R
by A4, A6, A7, FUNCT_1:def 7;
hence
(Mx2Tran M) " A is
affinely-independent
by A3, A12, RLAFFIN1:def 4;
verum end;