let n, m be Nat; :: thesis: for M being Matrix of n,m,F_Real
for A being affinely-independent Subset of (REAL-NS n) st the_rank_of M = n holds
for v being Element of (REAL-NS n) st v in Affin A holds
( (Mx2Tran M) . v in Affin ((Mx2Tran M) .: A) & ( for f being n -element real-valued FinSequence holds (v |-- A) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M) . f) ) )
let M be Matrix of n,m,F_Real; :: thesis: for A being affinely-independent Subset of (REAL-NS n) st the_rank_of M = n holds
for v being Element of (REAL-NS n) st v in Affin A holds
( (Mx2Tran M) . v in Affin ((Mx2Tran M) .: A) & ( for f being n -element real-valued FinSequence holds (v |-- A) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M) . f) ) )
let B be affinely-independent Subset of (REAL-NS n); :: thesis: ( the_rank_of M = n implies for v being Element of (REAL-NS n) st v in Affin B holds
( (Mx2Tran M) . v in Affin ((Mx2Tran M) .: B) & ( for f being n -element real-valued FinSequence holds (v |-- B) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: B)) . ((Mx2Tran M) . f) ) ) )
assume A1: the_rank_of M = n ; :: thesis: for v being Element of (REAL-NS n) st v in Affin B holds
( (Mx2Tran M) . v in Affin ((Mx2Tran M) .: B) & ( for f being n -element real-valued FinSequence holds (v |-- B) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: B)) . ((Mx2Tran M) . f) ) )
let w be Element of (REAL-NS n); :: thesis: ( w in Affin B implies ( (Mx2Tran M) . w in Affin ((Mx2Tran M) .: B) & ( for f being n -element real-valued FinSequence holds (w |-- B) . f = (((Mx2Tran M) . w) |-- ((Mx2Tran M) .: B)) . ((Mx2Tran M) . f) ) ) )
assume A2: w in Affin B ; :: thesis: ( (Mx2Tran M) . w in Affin ((Mx2Tran M) .: B) & ( for f being n -element real-valued FinSequence holds (w |-- B) . f = (((Mx2Tran M) . w) |-- ((Mx2Tran M) .: B)) . ((Mx2Tran M) . f) ) )
reconsider A = B as affinely-independent Subset of (TOP-REAL n) by Th41;
reconsider v = w as Element of (TOP-REAL n) by Th4;
A3: v in Affin A by A2, Th43;
v |-- A = w |-- B by A2, Th45;
hence ( (Mx2Tran M) . w in Affin ((Mx2Tran M) .: B) & ( for f being n -element real-valued FinSequence holds (w |-- B) . f = (((Mx2Tran M) . w) |-- ((Mx2Tran M) .: B)) . ((Mx2Tran M) . f) ) ) by A1, A3, MATRTOP2:25; :: thesis: verum