let n be Nat; :: thesis: for K being Field
for a, b being Element of K
for l being Nat
for pK, qK being FinSequence of K
for perm being Element of Permutations n st l in Seg n & len pK = n & len qK = n holds
for M being Matrix of n,K holds the multF of K $$ (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) = (a * (the multF of K $$ (Path_matrix perm,(RLine M,l,pK)))) + (b * (the multF of K $$ (Path_matrix perm,(RLine M,l,qK))))
let K be Field; :: thesis: for a, b being Element of K
for l being Nat
for pK, qK being FinSequence of K
for perm being Element of Permutations n st l in Seg n & len pK = n & len qK = n holds
for M being Matrix of n,K holds the multF of K $$ (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) = (a * (the multF of K $$ (Path_matrix perm,(RLine M,l,pK)))) + (b * (the multF of K $$ (Path_matrix perm,(RLine M,l,qK))))
let a, b be Element of K; :: thesis: for l being Nat
for pK, qK being FinSequence of K
for perm being Element of Permutations n st l in Seg n & len pK = n & len qK = n holds
for M being Matrix of n,K holds the multF of K $$ (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) = (a * (the multF of K $$ (Path_matrix perm,(RLine M,l,pK)))) + (b * (the multF of K $$ (Path_matrix perm,(RLine M,l,qK))))
let l be Nat; :: thesis: for pK, qK being FinSequence of K
for perm being Element of Permutations n st l in Seg n & len pK = n & len qK = n holds
for M being Matrix of n,K holds the multF of K $$ (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) = (a * (the multF of K $$ (Path_matrix perm,(RLine M,l,pK)))) + (b * (the multF of K $$ (Path_matrix perm,(RLine M,l,qK))))
let pK, qK be FinSequence of K; :: thesis: for perm being Element of Permutations n st l in Seg n & len pK = n & len qK = n holds
for M being Matrix of n,K holds the multF of K $$ (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) = (a * (the multF of K $$ (Path_matrix perm,(RLine M,l,pK)))) + (b * (the multF of K $$ (Path_matrix perm,(RLine M,l,qK))))
let perm be Element of Permutations n; :: thesis: ( l in Seg n & len pK = n & len qK = n implies for M being Matrix of n,K holds the multF of K $$ (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) = (a * (the multF of K $$ (Path_matrix perm,(RLine M,l,pK)))) + (b * (the multF of K $$ (Path_matrix perm,(RLine M,l,qK)))) )
assume that
A1: l in Seg n and
A2: len pK = n and
A3: len qK = n ; :: thesis: for M being Matrix of n,K holds the multF of K $$ (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) = (a * (the multF of K $$ (Path_matrix perm,(RLine M,l,pK)))) + (b * (the multF of K $$ (Path_matrix perm,(RLine M,l,qK))))
B1: Seg n <> {} by A1;
then B2: n <> 0 ;
reconsider L = l as Element of NAT by ORDINAL1:def 13;
set mm = the multF of K;
let M be Matrix of n,K; :: thesis: the multF of K $$ (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) = (a * (the multF of K $$ (Path_matrix perm,(RLine M,l,pK)))) + (b * (the multF of K $$ (Path_matrix perm,(RLine M,l,qK))))
set Rpq = RLine M,l,((a * pK) + (b * qK));
set Ppq = Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)));
A4: len (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) = n by MATRIX_3:def 7;
then consider fpq being Function of NAT ,the carrier of K such that
A5: fpq . 1 = (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) . 1 and
A6: for k being Element of NAT st 0 <> k & k < len (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) holds
fpq . (k + 1) = the multF of K . (fpq . k),((Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) . (k + 1)) and
A7: the multF of K $$ (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) = fpq . (len (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK))))) by A1, FINSEQ_1:4, FINSOP_1:def 1, B1, B2;
set Rq = RLine M,l,qK;
set Pq = Path_matrix perm,(RLine M,l,qK);
A8: len (Path_matrix perm,(RLine M,l,qK)) = n by MATRIX_3:def 7;
then consider fq being Function of NAT ,the carrier of K such that
A9: fq . 1 = (Path_matrix perm,(RLine M,l,qK)) . 1 and
A10: for k being Element of NAT st 0 <> k & k < len (Path_matrix perm,(RLine M,l,qK)) holds
fq . (k + 1) = the multF of K . (fq . k),((Path_matrix perm,(RLine M,l,qK)) . (k + 1)) and
A11: the multF of K $$ (Path_matrix perm,(RLine M,l,qK)) = fq . (len (Path_matrix perm,(RLine M,l,qK))) by A1, FINSEQ_1:4, FINSOP_1:def 1, B1, B2;
set Rp = RLine M,l,pK;
set Pp = Path_matrix perm,(RLine M,l,pK);
A12: len (Path_matrix perm,(RLine M,l,pK)) = n by MATRIX_3:def 7;
then consider fp being Function of NAT ,the carrier of K such that
A13: fp . 1 = (Path_matrix perm,(RLine M,l,pK)) . 1 and
A14: for k being Element of NAT st 0 <> k & k < len (Path_matrix perm,(RLine M,l,pK)) holds
fp . (k + 1) = the multF of K . (fp . k),((Path_matrix perm,(RLine M,l,pK)) . (k + 1)) and
A15: the multF of K $$ (Path_matrix perm,(RLine M,l,pK)) = fp . (len (Path_matrix perm,(RLine M,l,pK))) by A1, FINSEQ_1:4, FINSOP_1:def 1, B1, B2;
A16: n >= 1 by A1, FINSEQ_1:4, NAT_1:14, B1, B2;
defpred S1[ Nat] means ( 1 <= $1 & $1 < L implies ( fp . $1 = fq . $1 & fpq . $1 = fp . $1 ) );
A17: for k being Element of NAT st k in Seg n holds
( ( k <> L implies ( (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) . k = (Path_matrix perm,(RLine M,l,pK)) . k & (Path_matrix perm,(RLine M,l,pK)) . k = (Path_matrix perm,(RLine M,l,qK)) . k ) ) & ( k = L implies ex Ppk, Pqk being Element of K st
( Ppk = (Path_matrix perm,(RLine M,l,pK)) . k & Pqk = (Path_matrix perm,(RLine M,l,qK)) . k & (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) . k = (a * Ppk) + (b * Pqk) ) ) )
proof
let k be Element of NAT ; :: thesis: ( k in Seg n implies ( ( k <> L implies ( (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) . k = (Path_matrix perm,(RLine M,l,pK)) . k & (Path_matrix perm,(RLine M,l,pK)) . k = (Path_matrix perm,(RLine M,l,qK)) . k ) ) & ( k = L implies ex Ppk, Pqk being Element of K st
( Ppk = (Path_matrix perm,(RLine M,l,pK)) . k & Pqk = (Path_matrix perm,(RLine M,l,qK)) . k & (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) . k = (a * Ppk) + (b * Pqk) ) ) ) )
assume A18: k in Seg n ; :: thesis: ( ( k <> L implies ( (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) . k = (Path_matrix perm,(RLine M,l,pK)) . k & (Path_matrix perm,(RLine M,l,pK)) . k = (Path_matrix perm,(RLine M,l,qK)) . k ) ) & ( k = L implies ex Ppk, Pqk being Element of K st
( Ppk = (Path_matrix perm,(RLine M,l,pK)) . k & Pqk = (Path_matrix perm,(RLine M,l,qK)) . k & (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) . k = (a * Ppk) + (b * Pqk) ) ) )
A19: perm . k in Seg n by A4, A18, MATRIX_7:14;
then reconsider pk = perm . k as Element of NAT ;
A20: k in dom (Path_matrix perm,(RLine M,l,pK)) by A12, A18, FINSEQ_1:def 3;
A21: k in dom (Path_matrix perm,(RLine M,l,qK)) by A8, A18, FINSEQ_1:def 3;
[k,pk] in [:(Seg n),(Seg n):] by A18, A19, ZFMISC_1:106;
then A22: [k,pk] in Indices M by MATRIX_1:25;
dom qK = Seg n by A3, FINSEQ_1:def 3;
then A23: qK /. pk = qK . pk by A4, A18, MATRIX_7:14, PARTFUN1:def 8;
dom pK = Seg n by A2, FINSEQ_1:def 3;
then pK /. pk = pK . pk by A4, A18, MATRIX_7:14, PARTFUN1:def 8;
then reconsider ppk = pK . pk, qpk = qK . pk as Element of K by A23;
A24: len (b * qK) = n by A3, Lm5;
then dom (b * qK) = Seg n by FINSEQ_1:def 3;
then A25: (b * qK) . pk = b * qpk by A4, A18, FVSUM_1:62, MATRIX_7:14;
A26: len (a * pK) = n by A2, Lm5;
then A27: len ((a * pK) + (b * qK)) = n by A24, Lm6;
then A28: dom ((a * pK) + (b * qK)) = Seg n by FINSEQ_1:def 3;
dom (a * pK) = Seg n by A26, FINSEQ_1:def 3;
then A29: (a * pK) . pk = a * ppk by A4, A18, FVSUM_1:62, MATRIX_7:14;
A30: width M = n by MATRIX_1:25;
A31: k in dom (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) by A4, A18, FINSEQ_1:def 3;
thus ( k <> L implies ( (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) . k = (Path_matrix perm,(RLine M,l,pK)) . k & (Path_matrix perm,(RLine M,l,pK)) . k = (Path_matrix perm,(RLine M,l,qK)) . k ) ) :: thesis: ( k = L implies ex Ppk, Pqk being Element of K st
( Ppk = (Path_matrix perm,(RLine M,l,pK)) . k & Pqk = (Path_matrix perm,(RLine M,l,qK)) . k & (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) . k = (a * Ppk) + (b * Pqk) ) )
proof
assume A32: k <> L ; :: thesis: ( (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) . k = (Path_matrix perm,(RLine M,l,pK)) . k & (Path_matrix perm,(RLine M,l,pK)) . k = (Path_matrix perm,(RLine M,l,qK)) . k )
then A33: (RLine M,l,qK) * k,pk = M * k,pk by A3, A22, A30, Def3;
(RLine M,l,pK) * k,pk = M * k,pk by A2, A22, A30, A32, Def3;
then A34: (Path_matrix perm,(RLine M,l,pK)) . k = M * k,pk by A20, MATRIX_3:def 7;
(RLine M,l,((a * pK) + (b * qK))) * k,pk = M * k,pk by A27, A22, A30, A32, Def3;
hence ( (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) . k = (Path_matrix perm,(RLine M,l,pK)) . k & (Path_matrix perm,(RLine M,l,pK)) . k = (Path_matrix perm,(RLine M,l,qK)) . k ) by A31, A21, A33, A34, MATRIX_3:def 7; :: thesis: verum
end;
assume A35: k = L ; :: thesis: ex Ppk, Pqk being Element of K st
( Ppk = (Path_matrix perm,(RLine M,l,pK)) . k & Pqk = (Path_matrix perm,(RLine M,l,qK)) . k & (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) . k = (a * Ppk) + (b * Pqk) )
then A36: (RLine M,l,pK) * k,pk = pK . pk by A2, A22, A30, Def3;
A37: (RLine M,l,qK) * k,pk = qK . pk by A3, A22, A30, A35, Def3;
take ppk ; :: thesis: ex Pqk being Element of K st
( ppk = (Path_matrix perm,(RLine M,l,pK)) . k & Pqk = (Path_matrix perm,(RLine M,l,qK)) . k & (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) . k = (a * ppk) + (b * Pqk) )
take qpk ; :: thesis: ( ppk = (Path_matrix perm,(RLine M,l,pK)) . k & qpk = (Path_matrix perm,(RLine M,l,qK)) . k & (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) . k = (a * ppk) + (b * qpk) )
(RLine M,l,((a * pK) + (b * qK))) * k,pk = ((a * pK) + (b * qK)) . pk by A27, A22, A30, A35, Def3;
then (RLine M,l,((a * pK) + (b * qK))) * k,pk = (a * ppk) + (b * qpk) by A4, A18, A28, A29, A25, FVSUM_1:21, MATRIX_7:14;
hence ( ppk = (Path_matrix perm,(RLine M,l,pK)) . k & qpk = (Path_matrix perm,(RLine M,l,qK)) . k & (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) . k = (a * ppk) + (b * qpk) ) by A31, A20, A21, A36, A37, MATRIX_3:def 7; :: thesis: verum
end;
A38: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume A39: S1[k] ; :: thesis: S1[k + 1]
set k1 = k + 1;
assume that
A40: 1 <= k + 1 and
A41: k + 1 < L ; :: thesis: ( fp . (k + 1) = fq . (k + 1) & fpq . (k + 1) = fp . (k + 1) )
L <= n by A1, FINSEQ_1:3;
then A42: k + 1 <= n by A41, XXREAL_0:2;
then A43: k < n by NAT_1:13;
A44: k + 1 in Seg n by A40, A42;
now
per cases ( k = 0 or k > 0 ) ;
case k = 0 ; :: thesis: ( fp . (k + 1) = fq . (k + 1) & fpq . (k + 1) = fp . (k + 1) )
hence ( fp . (k + 1) = fq . (k + 1) & fpq . (k + 1) = fp . (k + 1) ) by A5, A13, A9, A17, A41, A44; :: thesis: verum
end;
case A45: k > 0 ; :: thesis: ( fp . (k + 1) = fq . (k + 1) & fpq . (k + 1) = fp . (k + 1) )
then A46: fp . (k + 1) = the multF of K . (fp . k),((Path_matrix perm,(RLine M,l,pK)) . (k + 1)) by A12, A14, A43;
A47: 0 < k + 0 by A45;
A48: fq . (k + 1) = the multF of K . (fq . k),((Path_matrix perm,(RLine M,l,qK)) . (k + 1)) by A8, A10, A43, A45;
fpq . (k + 1) = the multF of K . (fpq . k),((Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) . (k + 1)) by A4, A6, A43, A45;
hence ( fp . (k + 1) = fq . (k + 1) & fpq . (k + 1) = fp . (k + 1) ) by A17, A39, A41, A44, A47, A46, A48, NAT_1:13, NAT_1:19; :: thesis: verum
end;
end;
end;
hence ( fp . (k + 1) = fq . (k + 1) & fpq . (k + 1) = fp . (k + 1) ) ; :: thesis: verum
end;
defpred S2[ Nat] means ( 1 <= $1 & L <= $1 & $1 <= n implies for k being Element of NAT st $1 = k holds
fpq . k = (a * (fp . k)) + (b * (fq . k)) );
A49: S1[ 0 ] ;
A50: fpq . L = (a * (fp . L)) + (b * (fq . L))
proof
consider PpL, PqL being Element of K such that
A51: PpL = (Path_matrix perm,(RLine M,l,pK)) . L and
A52: PqL = (Path_matrix perm,(RLine M,l,qK)) . L and
A53: (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) . L = (a * PpL) + (b * PqL) by A1, A17;
A54: L >= 1 by A1, FINSEQ_1:3;
now
per cases ( L > 1 or L = 1 ) by A54, XXREAL_0:1;
case A55: L > 1 ; :: thesis: fpq . L = (a * (fp . L)) + (b * (fq . L))
then reconsider L1 = L - 1 as Element of NAT by NAT_1:20;
A56: L1 + 1 > 1 + 0 by A55;
A57: L1 < L1 + 1 by NAT_1:19;
L <= n by A1, FINSEQ_1:3;
then A58: L1 < n by A57, XXREAL_0:2;
then fp . L = (fp . L1) * PpL by A12, A14, A51, A56;
then A59: (fp . L1) * (a * PpL) = a * (fp . L) by GROUP_1:def 4;
A60: for k being Element of NAT holds S1[k] from NAT_1:sch 1(A49, A38);
A61: 1 <= L1 by A56, NAT_1:19;
then fp . L1 = fq . L1 by A60, A57;
then fq . L = (fp . L1) * PqL by A8, A10, A52, A56, A58;
then A62: (fp . L1) * (b * PqL) = b * (fq . L) by GROUP_1:def 4;
fpq . L1 = fp . L1 by A60, A57, A61;
then fpq . L = (fp . L1) * ((a * PpL) + (b * PqL)) by A4, A6, A53, A56, A58;
hence fpq . L = (a * (fp . L)) + (b * (fq . L)) by A59, A62, VECTSP_1:def 18; :: thesis: verum
end;
case L = 1 ; :: thesis: fpq . L = (a * (fp . L)) + (b * (fq . L))
hence fpq . L = (a * (fp . L)) + (b * (fq . L)) by A5, A13, A9, A51, A52, A53; :: thesis: verum
end;
end;
end;
hence fpq . L = (a * (fp . L)) + (b * (fq . L)) ; :: thesis: verum
end;
A63: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S2[k] implies S2[k + 1] )
assume A64: S2[k] ; :: thesis: S2[k + 1]
set k1 = k + 1;
assume that
A65: 1 <= k + 1 and
A66: L <= k + 1 and
A67: k + 1 <= n ; :: thesis: for k being Element of NAT st k + 1 = k holds
fpq . k = (a * (fp . k)) + (b * (fq . k))
let k9 be Element of NAT ; :: thesis: ( k + 1 = k9 implies fpq . k9 = (a * (fp . k9)) + (b * (fq . k9)) )
assume A68: k9 = k + 1 ; :: thesis: fpq . k9 = (a * (fp . k9)) + (b * (fq . k9))
now
per cases ( k + 1 = L or k + 1 > L ) by A66, XXREAL_0:1;
case k + 1 = L ; :: thesis: fpq . k9 = (a * (fp . k9)) + (b * (fq . k9))
hence fpq . k9 = (a * (fp . k9)) + (b * (fq . k9)) by A50, A68; :: thesis: verum
end;
case A69: k + 1 > L ; :: thesis: fpq . k9 = (a * (fp . k9)) + (b * (fq . k9))
A70: k + 1 in Seg n by A65, A67;
then A71: (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) . (k + 1) = (Path_matrix perm,(RLine M,l,pK)) . (k + 1) by A17, A69;
k + 1 in dom (Path_matrix perm,(RLine M,l,pK)) by A12, A70, FINSEQ_1:def 3;
then (Path_matrix perm,(RLine M,l,pK)) /. (k + 1) = (Path_matrix perm,(RLine M,l,pK)) . (k + 1) by PARTFUN1:def 8;
then reconsider Ppk1 = (Path_matrix perm,(RLine M,l,pK)) . (k + 1) as Element of K ;
A72: k < n by A67, NAT_1:13;
A73: (b * (fq . k)) * Ppk1 = b * ((fq . k) * Ppk1) by GROUP_1:def 4;
A74: (a * (fp . k)) * Ppk1 = a * ((fp . k) * Ppk1) by GROUP_1:def 4;
A75: 1 <= L by A1, FINSEQ_1:3;
A76: k >= L by A69, NAT_1:13;
then fpq . k = (a * (fp . k)) + (b * (fq . k)) by A64, A67, A75, NAT_1:13, XXREAL_0:2;
then A77: fpq . (k + 1) = ((a * (fp . k)) + (b * (fq . k))) * Ppk1 by A4, A6, A76, A72, A75, A71;
(Path_matrix perm,(RLine M,l,pK)) . (k + 1) = (Path_matrix perm,(RLine M,l,qK)) . (k + 1) by A17, A69, A70;
then A78: fq . (k + 1) = (fq . k) * Ppk1 by A8, A10, A76, A72, A75;
fp . (k + 1) = (fp . k) * Ppk1 by A12, A14, A76, A72, A75;
hence fpq . k9 = (a * (fp . k9)) + (b * (fq . k9)) by A68, A77, A78, A74, A73, VECTSP_1:def 18; :: thesis: verum
end;
end;
end;
hence fpq . k9 = (a * (fp . k9)) + (b * (fq . k9)) ; :: thesis: verum
end;
A79: L <= n by A1, FINSEQ_1:3;
A80: S2[ 0 ] ;
for k being Element of NAT holds S2[k] from NAT_1:sch 1(A80, A63);
 hence the multF of K $$ (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) = (a * (the multF of K $$ (Path_matrix perm,(RLine M,l,pK)))) + (b * (the multF of K $$ (Path_matrix perm,(RLine M,l,qK)))) by A16, A4, A12, A8, A7, A15, A11, A79; :: thesis: verum