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