let n, m be Nat; :: thesis: 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
for v being Element of (TOP-REAL 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 (TOP-REAL n) st the_rank_of M = n holds
for v being Element of (TOP-REAL 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) ) )
reconsider Z = 0 as Element of NAT ;
set TRn = TOP-REAL n;
set TRm = TOP-REAL m;
let A be affinely-independent Subset of (TOP-REAL n); :: thesis: ( the_rank_of M = n implies for v being Element of (TOP-REAL 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) ) ) )
assume A1: the_rank_of M = n ; :: thesis: for v being Element of (TOP-REAL 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) ) )
set MT = Mx2Tran M;
let v be Element of (TOP-REAL n); :: thesis: ( v in Affin A implies ( (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) ) ) )
assume A2: v in Affin A ; :: thesis: ( (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) ) )
set vA = v |-- A;
set C = Carrier (v |-- A);
defpred S1[ object , object ] means ( ( not $1 in rng (Mx2Tran M) implies $2 = 0 ) & ( $1 in rng (Mx2Tran M) implies for f being n -element real-valued FinSequence st (Mx2Tran M) . f = $1 holds
$2 = (v |-- A) . f ) );
consider H being FinSequence of the carrier of (TOP-REAL n) such that
A3: H is one-to-one and
A4: rng H = Carrier (v |-- A) and
A5: Sum ((v |-- A) (#) H) = Sum (v |-- A) by RLVECT_2:def 8;
A6: Sum (v |-- A) = v by A2, RLAFFIN1:def 7;
reconsider MTR = (Mx2Tran M) * H as FinSequence of (TOP-REAL m) ;
A7: dom (Mx2Tran M) = [#] (TOP-REAL n) by FUNCT_2:def 1;
then rng H c= dom (Mx2Tran M) ;
then A8: len MTR = len H by FINSEQ_2:29;
A9: Mx2Tran M is one-to-one by A1, MATRTOP1:39;
A10: for x being object st x in the carrier of (TOP-REAL m) holds
ex y being object st
( y in REAL & S1[x,y] )
proof
let y be object ; :: thesis: ( y in the carrier of (TOP-REAL m) implies ex y being object st
( y in REAL & S1[y,y] ) )
assume y in the carrier of (TOP-REAL m) ; :: thesis: ex y being object st
( y in REAL & S1[y,y] )
per cases ( y in rng (Mx2Tran M) or not y in rng (Mx2Tran M) ) ;
suppose A11: y in rng (Mx2Tran M) ; :: thesis: ex y being object st
( y in REAL & S1[y,y] )
then consider x being object such that
A12: x in dom (Mx2Tran M) and
A13: (Mx2Tran M) . x = y by FUNCT_1:def 3;
reconsider x = x as Element of (TOP-REAL n) by A12;
take (v |-- A) . x ; :: thesis: ( (v |-- A) . x in REAL & S1[y,(v |-- A) . x] )
thus ( (v |-- A) . x in REAL & ( not y in rng (Mx2Tran M) implies (v |-- A) . x = 0 ) ) by A11; :: thesis: ( y in rng (Mx2Tran M) implies for f being n -element real-valued FinSequence st (Mx2Tran M) . f = y holds
(v |-- A) . x = (v |-- A) . f )
assume y in rng (Mx2Tran M) ; :: thesis: for f being n -element real-valued FinSequence st (Mx2Tran M) . f = y holds
(v |-- A) . x = (v |-- A) . f
let f be n -element real-valued FinSequence; :: thesis: ( (Mx2Tran M) . f = y implies (v |-- A) . x = (v |-- A) . f )
assume A14: (Mx2Tran M) . f = y ; :: thesis: (v |-- A) . x = (v |-- A) . f
f is Element of (TOP-REAL n) by Lm3;
hence (v |-- A) . x = (v |-- A) . f by A7, A9, A13, A14, FUNCT_1:def 4; :: thesis: verum
end;
suppose A15: not y in rng (Mx2Tran M) ; :: thesis: ex y being object st
( y in REAL & S1[y,y] )
take x = 0 ; :: thesis: ( x in REAL & S1[y,x] )
thus ( x in REAL & S1[y,x] ) by A15; :: thesis: verum
end;
end;
end;
consider F being Function of the carrier of (TOP-REAL m),REAL such that
A16: for x being object st x in the carrier of (TOP-REAL m) holds
S1[x,F . x] from FUNCT_2:sch 1(A10);
 reconsider F = F as Element of Funcs ( the carrier of (TOP-REAL m),REAL) by FUNCT_2:8;
A17: now :: thesis: for w being Element of (TOP-REAL m) st not w in (Mx2Tran M) .: (Carrier (v |-- A)) holds
not F . w <> 0
let w be Element of (TOP-REAL m); :: thesis: ( not w in (Mx2Tran M) .: (Carrier (v |-- A)) implies not F . w <> 0 )
assume A18: not w in (Mx2Tran M) .: (Carrier (v |-- A)) ; :: thesis: not F . w <> 0
assume A19: F . w <> 0 ; :: thesis: contradiction
then w in rng (Mx2Tran M) by A16;
then consider f being object such that
A20: f in dom (Mx2Tran M) and
A21: (Mx2Tran M) . f = w by FUNCT_1:def 3;
reconsider f = f as Element of (TOP-REAL n) by A20;
(v |-- A) . f = F . w by A16, A19, A21;
then f in Carrier (v |-- A) by A19, RLVECT_2:19;
hence contradiction by A18, A20, A21, FUNCT_1:def 6; :: thesis: verum
end;
then reconsider F = F as Linear_Combination of TOP-REAL m by RLVECT_2:def 3;
A22: (Mx2Tran M) .: (Carrier (v |-- A)) c= Carrier F
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (Mx2Tran M) .: (Carrier (v |-- A)) or y in Carrier F )
assume A23: y in (Mx2Tran M) .: (Carrier (v |-- A)) ; :: thesis: y in Carrier F
then consider x being object such that
A24: x in dom (Mx2Tran M) and
A25: x in Carrier (v |-- A) and
A26: (Mx2Tran M) . x = y by FUNCT_1:def 6;
reconsider x = x as Element of (TOP-REAL n) by A24;
A27: (v |-- A) . x <> 0 by A25, RLVECT_2:19;
reconsider f = y as Element of (TOP-REAL m) by A23;
S1[f,F . f] by A16;
then F . f = (v |-- A) . x by A24, A26, FUNCT_1:def 3;
hence y in Carrier F by A27, RLVECT_2:19; :: thesis: verum
end;
Carrier F c= (Mx2Tran M) .: (Carrier (v |-- A))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier F or x in (Mx2Tran M) .: (Carrier (v |-- A)) )
assume A28: x in Carrier F ; :: thesis: x in (Mx2Tran M) .: (Carrier (v |-- A))
then reconsider w = x as Element of (TOP-REAL m) ;
F . w <> 0 by A28, RLVECT_2:19;
hence x in (Mx2Tran M) .: (Carrier (v |-- A)) by A17; :: thesis: verum
end;
then A29: Carrier F = (Mx2Tran M) .: (Carrier (v |-- A)) by A22;
Carrier (v |-- A) c= A by RLVECT_2:def 6;
then (Mx2Tran M) .: (Carrier (v |-- A)) c= (Mx2Tran M) .: A by RELAT_1:123;
then reconsider F = F as Linear_Combination of (Mx2Tran M) .: A by A29, RLVECT_2:def 6;
set Fm = F (#) MTR;
consider fm being sequence of (TOP-REAL m) such that
A30: Sum (F (#) MTR) = fm . (len (F (#) MTR)) and
A31: fm . 0 = 0. (TOP-REAL m) and
A32: for j being Nat
for v being Element of (TOP-REAL m) st j < len (F (#) MTR) & v = (F (#) MTR) . (j + 1) holds
fm . (j + 1) = (fm . j) + v by RLVECT_1:def 12;
A33: rng MTR = (Mx2Tran M) .: (Carrier (v |-- A)) by A4, RELAT_1:127;
dom (v |-- A) = [#] (TOP-REAL n) by FUNCT_2:def 1;
then A34: len ((v |-- A) * H) = len H by A4, FINSEQ_2:29;
set vAH = (v |-- A) (#) H;
consider h being sequence of (TOP-REAL n) such that
A35: Sum ((v |-- A) (#) H) = h . (len ((v |-- A) (#) H)) and
A36: h . 0 = 0. (TOP-REAL n) and
A37: for j being Nat
for v being Element of (TOP-REAL n) st j < len ((v |-- A) (#) H) & v = ((v |-- A) (#) H) . (j + 1) holds
h . (j + 1) = (h . j) + v by RLVECT_1:def 12;
A38: len ((v |-- A) (#) H) = len H by RLVECT_2:def 7;
defpred S2[ Nat] means ( $1 <= len (F (#) MTR) implies fm . $1 = (Mx2Tran M) . (h . $1) );
A39: len (F (#) MTR) = len MTR by RLVECT_2:def 7;
A40: (Mx2Tran M) .: (Carrier (v |-- A)) c= rng (Mx2Tran M) by RELAT_1:111;
A41: for j being Nat st S2[j] holds
S2[j + 1]
proof
reconsider TRM = TOP-REAL m as RealLinearSpace ;
reconsider TRN = TOP-REAL n as RealLinearSpace ;
let j be Nat; :: thesis: ( S2[j] implies S2[j + 1] )
reconsider J = j as Element of NAT by ORDINAL1:def 12;
set j1 = J + 1;
assume A42: S2[j] ; :: thesis: S2[j + 1]
reconsider MTRj1 = MTR /. (J + 1) as Element of TRM ;
reconsider hj1 = H /. (J + 1) as n -element real-valued FinSequence ;
reconsider Hj1 = H /. (J + 1) as Element of TRN ;
assume A43: j + 1 <= len (F (#) MTR) ; :: thesis: fm . (j + 1) = (Mx2Tran M) . (h . (j + 1))
A44: 1 <= J + 1 by NAT_1:11;
then A45: J + 1 in dom MTR by A39, A43, FINSEQ_3:25;
then A46: MTRj1 = MTR . (J + 1) by PARTFUN1:def 6;
A47: MTR . (J + 1) in (Mx2Tran M) .: (Carrier (v |-- A)) by A33, A45, FUNCT_1:def 3;
J + 1 in dom H by A39, A8, A43, A44, FINSEQ_3:25;
then A48: Hj1 = H . (J + 1) by PARTFUN1:def 6;
then MTR . (J + 1) = (Mx2Tran M) . Hj1 by A45, FUNCT_1:12;
then A49: F . MTRj1 = (v |-- A) . Hj1 by A16, A40, A46, A47;
A50: J + 1 in dom ((v |-- A) (#) H) by A39, A38, A8, A43, A44, FINSEQ_3:25;
then ((v |-- A) (#) H) . (J + 1) in rng ((v |-- A) (#) H) by FUNCT_1:def 3;
then reconsider vAHj1 = ((v |-- A) (#) H) . (J + 1) as Element of (TOP-REAL n) ;
A51: J + 1 in dom (F (#) MTR) by A43, A44, FINSEQ_3:25;
then (F (#) MTR) . (J + 1) in rng (F (#) MTR) by FUNCT_1:def 3;
then reconsider Fmj1 = (F (#) MTR) . (J + 1) as Element of (TOP-REAL m) ;
A52: (Mx2Tran M) . vAHj1 = (Mx2Tran M) . (((v |-- A) . Hj1) * Hj1) by A50, RLVECT_2:def 7
.= (Mx2Tran M) . (((v |-- A) . Hj1) * hj1) by EUCLID:65
.= ((v |-- A) . Hj1) * ((Mx2Tran M) . hj1) by MATRTOP1:23
.= (F . MTRj1) * MTRj1 by A45, A48, A46, A49, EUCLID:65, FUNCT_1:12
.= Fmj1 by A51, RLVECT_2:def 7 ;
A53: j < len (F (#) MTR) by A43, NAT_1:13;
then h . (J + 1) = (h . J) + vAHj1 by A37, A39, A38, A8;
hence (Mx2Tran M) . (h . (j + 1)) = ((Mx2Tran M) . (h . J)) + ((Mx2Tran M) . vAHj1) by MATRTOP1:27
.= fm . (j + 1) by A32, A52, A53, A42 ;
:: thesis: verum
end;
A54: S2[ 0 ] by A36, A31, MATRTOP1:29;
for j being Nat holds S2[j] from NAT_1:sch 2(A54, A41);
 then Sum (F (#) MTR) = (Mx2Tran M) . (Sum ((v |-- A) (#) H)) by A35, A30, A39, A38, A8;
then A55: Sum F = (Mx2Tran M) . v by A9, A29, A3, A5, A6, A33, RLVECT_2:def 8;
A56: now :: thesis: for i being Nat st 1 <= i & i <= len H holds
(F * MTR) . i = ((v |-- A) * H) . i
let i be Nat; :: thesis: ( 1 <= i & i <= len H implies (F * MTR) . i = ((v |-- A) * H) . i )
assume A57: ( 1 <= i & i <= len H ) ; :: thesis: (F * MTR) . i = ((v |-- A) * H) . i
then A58: i in dom H by FINSEQ_3:25;
then A59: ((v |-- A) * H) . i = (v |-- A) . (H . i) by FUNCT_1:13;
H . i in rng H by A58, FUNCT_1:def 3;
then reconsider Hi = H . i as Element of (TOP-REAL n) ;
A60: MTR . i = (Mx2Tran M) . (H . i) by A58, FUNCT_1:13;
A61: i in dom MTR by A8, A57, FINSEQ_3:25;
then A62: MTR . i in rng MTR by FUNCT_1:def 3;
(F * MTR) . i = F . (MTR . i) by A61, FUNCT_1:13;
then S1[(Mx2Tran M) . Hi,(F * MTR) . i] by A16, A60;
hence (F * MTR) . i = ((v |-- A) * H) . i by A33, A40, A59, A60, A62; :: thesis: verum
end;
dom F = [#] (TOP-REAL m) by FUNCT_2:def 1;
then len (F * MTR) = len MTR by A33, FINSEQ_2:29;
then (v |-- A) * H = F * MTR by A8, A34, A56;
then Sum (F * MTR) = sum (v |-- A) by A3, A4, RLAFFIN1:def 3
.= 1 by A2, RLAFFIN1:def 7 ;
then A63: sum F = 1 by A9, A29, A3, A33, RLAFFIN1:def 3;
then Sum F in { (Sum L) where L is Linear_Combination of (Mx2Tran M) .: A : sum L = 1 } ;
hence A64: (Mx2Tran M) . v in Affin ((Mx2Tran M) .: A) by A55, RLAFFIN1:59; :: thesis: for f being n -element real-valued FinSequence holds (v |-- A) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M) . f)
let f be n -element real-valued FinSequence; :: thesis: (v |-- A) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M) . f)
f is Element of (TOP-REAL n) by Lm3;
then A65: (Mx2Tran M) . f in rng (Mx2Tran M) by A7, FUNCT_1:def 3;
(Mx2Tran M) .: A is affinely-independent by A1, Th24;
then F = ((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A) by A55, A63, A64, RLAFFIN1:def 7;
hence (v |-- A) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M) . f) by A16, A65; :: thesis: verum