let n be Nat; :: thesis:
let K be commutative Ring; :: thesis:
let a, b be Element of K; :: thesis:
let l be Nat; :: thesis:
let pK, qK be FinSequence of K; :: thesis:
let perm be Element of Permutations n; :: thesis:
assume that
A1: l in Seg n and
A2: len pK = n and
A3: len qK = n ; :: thesis:
Seg n <> {} by A1;
then A4: n <> 0 ;
reconsider L = l as Element of NAT by ORDINAL1:def 12;
set mm = the multF of K;
let M be Matrix of n,K; :: thesis:
set Rpq = RLine (M,l,((a * pK) + (b * qK)));
set Ppq = Path_matrix (perm,(RLine (M,l,((a * pK) + (b * qK)))));
A5: len (Path_matrix (perm,(RLine (M,l,((a * pK) + (b * qK)))))) = n by MATRIX_3:def 7;
then consider fpq being sequence of the carrier of K such that
A6: fpq . 1 = (Path_matrix (perm,(RLine (M,l,((a * pK) + (b * qK)))))) . 1 and
A7: for k being 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
A8: 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 A4, FINSOP_1:def 1;
set Rq = RLine (M,l,qK);
set Pq = Path_matrix (perm,(RLine (M,l,qK)));
A9: len (Path_matrix (perm,(RLine (M,l,qK)))) = n by MATRIX_3:def 7;
then consider fq being sequence of the carrier of K such that
A10: fq . 1 = (Path_matrix (perm,(RLine (M,l,qK)))) . 1 and
A11: for k being 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
A12: the multF of K $$ (Path_matrix (perm,(RLine (M,l,qK)))) = fq . (len (Path_matrix (perm,(RLine (M,l,qK))))) by A4, FINSOP_1:def 1;
set Rp = RLine (M,l,pK);
set Pp = Path_matrix (perm,(RLine (M,l,pK)));
A13: len (Path_matrix (perm,(RLine (M,l,pK)))) = n by MATRIX_3:def 7;
then consider fp being sequence of the carrier of K such that
A14: fp . 1 = (Path_matrix (perm,(RLine (M,l,pK)))) . 1 and
A15: for k being 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
A16: the multF of K $$ (Path_matrix (perm,(RLine (M,l,pK)))) = fp . (len (Path_matrix (perm,(RLine (M,l,pK))))) by A4, FINSOP_1:def 1;
A17: n >= 1 by A4, NAT_1:14;
defpred S₁[ Nat] means ( 1 <= $1 & $1 < L implies ( fp . $1 = fq . $1 & fpq . $1 = fp . $1 ) );
A18: 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:
assume A19: k in Seg n ; :: thesis:
A20: perm . k in Seg n by A19, MATRIX_7:14;
then reconsider pk = perm . k as Element of NAT ;
A21: k in dom (Path_matrix (perm,(RLine (M,l,pK)))) by A13, A19, FINSEQ_1:def 3;
A22: k in dom (Path_matrix (perm,(RLine (M,l,qK)))) by A9, A19, FINSEQ_1:def 3;
[k,pk] in [:(Seg n),(Seg n):] by A19, A20, ZFMISC_1:87;
then A23: [k,pk] in Indices M by MATRIX_0:24;
dom qK = Seg n by A3, FINSEQ_1:def 3;
then A24: qK /. pk = qK . pk by A19, MATRIX_7:14, PARTFUN1:def 6;
dom pK = Seg n by A2, FINSEQ_1:def 3;
then pK /. pk = pK . pk by A19, MATRIX_7:14, PARTFUN1:def 6;
then reconsider ppk = pK . pk, qpk = qK . pk as Element of K by A24;
A25: len (b * qK) = n by A3, Lm5;
then dom (b * qK) = Seg n by FINSEQ_1:def 3;
then A26: (b * qK) . pk = b * qpk by A19, FVSUM_1:50, MATRIX_7:14;
A27: len (a * pK) = n by A2, Lm5;
then A28: len ((a * pK) + (b * qK)) = n by A25, Lm6;
then A29: dom ((a * pK) + (b * qK)) = Seg n by FINSEQ_1:def 3;
dom (a * pK) = Seg n by A27, FINSEQ_1:def 3;
then A30: (a * pK) . pk = a * ppk by A19, FVSUM_1:50, MATRIX_7:14;
A31: width M = n by MATRIX_0:24;
A32: k in dom (Path_matrix (perm,(RLine (M,l,((a * pK) + (b * qK)))))) by A5, A19, 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:

proof

assume A33: k <> L ; :: thesis:
then A34: (RLine (M,l,qK)) * (k,pk) = M * (k,pk) by A3, A23, A31, Def3;
(RLine (M,l,pK)) * (k,pk) = M * (k,pk) by A2, A23, A31, A33, Def3;
then A35: (Path_matrix (perm,(RLine (M,l,pK)))) . k = M * (k,pk) by A21, MATRIX_3:def 7;
(RLine (M,l,((a * pK) + (b * qK)))) * (k,pk) = M * (k,pk) by A28, A23, A31, A33, 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 A32, A22, A34, A35, MATRIX_3:def 7; :: thesis:

end;

assume A36: k = L ; :: thesis:
then A37: (RLine (M,l,pK)) * (k,pk) = pK . pk by A2, A23, A31, Def3;
A38: (RLine (M,l,qK)) * (k,pk) = qK . pk by A3, A23, A31, A36, Def3;
take ppk ; :: thesis:
take qpk ; :: thesis:
(RLine (M,l,((a * pK) + (b * qK)))) * (k,pk) = ((a * pK) + (b * qK)) . pk by A28, A23, A31, A36, Def3;
then (RLine (M,l,((a * pK) + (b * qK)))) * (k,pk) = (a * ppk) + (b * qpk) by A19, A29, A30, A26, FVSUM_1:17, 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 A32, A21, A22, A37, A38, MATRIX_3:def 7; :: thesis:

end;

A39: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A40: S₁[k] ; :: thesis:
set k1 = k + 1;
assume that
A41: 1 <= k + 1 and
A42: k + 1 < L ; :: thesis:
L <= n by A1, FINSEQ_1:1;
then A43: k + 1 <= n by A42, XXREAL_0:2;
then A44: k < n by NAT_1:13;
A45: k + 1 in Seg n by A41, A43;

now :: thesis:

per cases ;

case k = 0 ; :: thesis:

hence ( fp . (k + 1) = fq . (k + 1) & fpq . (k + 1) = fp . (k + 1) ) by A6, A14, A10, A18, A42, A45; :: thesis:

end;

case A46: k > 0 ; :: thesis:

then A47: fp . (k + 1) = the multF of K . ((fp . k),((Path_matrix (perm,(RLine (M,l,pK)))) . (k + 1))) by A13, A15, A44;
A48: 0 < k + 0 by A46;
A49: fq . (k + 1) = the multF of K . ((fq . k),((Path_matrix (perm,(RLine (M,l,qK)))) . (k + 1))) by A9, A11, A44, A46;
fpq . (k + 1) = the multF of K . ((fpq . k),((Path_matrix (perm,(RLine (M,l,((a * pK) + (b * qK)))))) . (k + 1))) by A5, A7, A44, A46;
hence ( fp . (k + 1) = fq . (k + 1) & fpq . (k + 1) = fp . (k + 1) ) by A18, A40, A42, A45, A48, A47, A49, NAT_1:13, NAT_1:19; :: thesis:

end;

hence ( fp . (k + 1) = fq . (k + 1) & fpq . (k + 1) = fp . (k + 1) ) ; :: thesis:

end;

defpred S₂[ Nat] means ( 1 <= $1 & L <= $1 & $1 <= n implies for k being Nat st $1 = k holds
fpq . k = (a * (fp . k)) + (b * (fq . k)) );
A50: S₁[ 0 ] ;
A51: fpq . L = (a * (fp . L)) + (b * (fq . L))

proof

consider PpL, PqL being Element of K such that
A52: PpL = (Path_matrix (perm,(RLine (M,l,pK)))) . L and
A53: PqL = (Path_matrix (perm,(RLine (M,l,qK)))) . L and
A54: (Path_matrix (perm,(RLine (M,l,((a * pK) + (b * qK)))))) . L = (a * PpL) + (b * PqL) by A1, A18;
A55: L >= 1 by A1, FINSEQ_1:1;

now :: thesis:

per cases by A55, XXREAL_0:1;

case A56: L > 1 ; :: thesis:

then reconsider L1 = L - 1 as Element of NAT by NAT_1:20;
A57: L1 + 1 > 1 + 0 by A56;
A58: L1 < L1 + 1 by NAT_1:19;
L <= n by A1, FINSEQ_1:1;
then A59: L1 < n by A58, XXREAL_0:2;
then fp . L = (fp . L1) * PpL by A13, A15, A52, A57;
then A60: (fp . L1) * (a * PpL) = a * (fp . L) by GROUP_1:def 3;
A61: for k being Nat holds S₁[k] from NAT_1:sch 2(A50, A39);
A62: 1 <= L1 by A57, NAT_1:19;
then fp . L1 = fq . L1 by A61, A58;
then fq . L = (fp . L1) * PqL by A9, A11, A53, A57, A59;
then A63: (fp . L1) * (b * PqL) = b * (fq . L) by GROUP_1:def 3;
fpq . L1 = fp . L1 by A61, A58, A62;
then fpq . L = (fp . L1) * ((a * PpL) + (b * PqL)) by A5, A7, A54, A57, A59;
hence fpq . L = (a * (fp . L)) + (b * (fq . L)) by A60, A63, VECTSP_1:def 7; :: thesis:

end;

case L = 1 ; :: thesis:

hence fpq . L = (a * (fp . L)) + (b * (fq . L)) by A6, A14, A10, A52, A53, A54; :: thesis:

end;

hence fpq . L = (a * (fp . L)) + (b * (fq . L)) ; :: thesis:

end;

A64: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis:
assume A65: S₂[k] ; :: thesis:
set k1 = k + 1;
assume that
A66: 1 <= k + 1 and
A67: L <= k + 1 and
A68: k + 1 <= n ; :: thesis:
let k9 be Nat; :: thesis:
assume A69: k9 = k + 1 ; :: thesis:

now :: thesis:

per cases by A67, XXREAL_0:1;

case k + 1 = L ; :: thesis:

hence fpq . k9 = (a * (fp . k9)) + (b * (fq . k9)) by A51, A69; :: thesis:

end;

case A70: k + 1 > L ; :: thesis:

A71: k + 1 in Seg n by A66, A68;
then A72: (Path_matrix (perm,(RLine (M,l,((a * pK) + (b * qK)))))) . (k + 1) = (Path_matrix (perm,(RLine (M,l,pK)))) . (k + 1) by A18, A70;
k + 1 in dom (Path_matrix (perm,(RLine (M,l,pK)))) by A13, A71, 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 6;
then reconsider Ppk1 = (Path_matrix (perm,(RLine (M,l,pK)))) . (k + 1) as Element of K ;
A73: k < n by A68, NAT_1:13;
A74: (b * (fq . k)) * Ppk1 = b * ((fq . k) * Ppk1) by GROUP_1:def 3;
A75: (a * (fp . k)) * Ppk1 = a * ((fp . k) * Ppk1) by GROUP_1:def 3;
A76: 1 <= L by A1, FINSEQ_1:1;
A77: k >= L by A70, NAT_1:13;
then fpq . k = (a * (fp . k)) + (b * (fq . k)) by A65, A68, A76, NAT_1:13, XXREAL_0:2;
then A78: fpq . (k + 1) = ((a * (fp . k)) + (b * (fq . k))) * Ppk1 by A5, A7, A77, A73, A76, A72;
(Path_matrix (perm,(RLine (M,l,pK)))) . (k + 1) = (Path_matrix (perm,(RLine (M,l,qK)))) . (k + 1) by A18, A70, A71;
then A79: fq . (k + 1) = (fq . k) * Ppk1 by A9, A11, A77, A73, A76;
fp . (k + 1) = (fp . k) * Ppk1 by A13, A15, A77, A73, A76;
hence fpq . k9 = (a * (fp . k9)) + (b * (fq . k9)) by A69, A78, A79, A75, A74, VECTSP_1:def 7; :: thesis:

end;

hence fpq . k9 = (a * (fp . k9)) + (b * (fq . k9)) ; :: thesis:

end;

A80: L <= n by A1, FINSEQ_1:1;
A81: S₂[ 0 ] ;
for k being Nat holds S₂[k] from NAT_1:sch 2(A81, A64);
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 A17, A5, A13, A9, A8, A16, A12, A80; :: thesis: