let n be Nat; :: thesis: for K being commutative Ring
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 (Path_product (RLine (M,l,((a * pK) + (b * qK))))) . perm = (a * ((Path_product (RLine (M,l,pK))) . perm)) + (b * ((Path_product (RLine (M,l,qK))) . perm))
let K be commutative Ring; :: 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 (Path_product (RLine (M,l,((a * pK) + (b * qK))))) . perm = (a * ((Path_product (RLine (M,l,pK))) . perm)) + (b * ((Path_product (RLine (M,l,qK))) . perm))
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 (Path_product (RLine (M,l,((a * pK) + (b * qK))))) . perm = (a * ((Path_product (RLine (M,l,pK))) . perm)) + (b * ((Path_product (RLine (M,l,qK))) . perm))
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 (Path_product (RLine (M,l,((a * pK) + (b * qK))))) . perm = (a * ((Path_product (RLine (M,l,pK))) . perm)) + (b * ((Path_product (RLine (M,l,qK))) . perm))
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 (Path_product (RLine (M,l,((a * pK) + (b * qK))))) . perm = (a * ((Path_product (RLine (M,l,pK))) . perm)) + (b * ((Path_product (RLine (M,l,qK))) . perm))
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 (Path_product (RLine (M,l,((a * pK) + (b * qK))))) . perm = (a * ((Path_product (RLine (M,l,pK))) . perm)) + (b * ((Path_product (RLine (M,l,qK))) . perm)) )
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 (Path_product (RLine (M,l,((a * pK) + (b * qK))))) . perm = (a * ((Path_product (RLine (M,l,pK))) . perm)) + (b * ((Path_product (RLine (M,l,qK))) . perm))
set mm = the multF of K;
let M be Matrix of n,K; :: thesis: (Path_product (RLine (M,l,((a * pK) + (b * qK))))) . perm = (a * ((Path_product (RLine (M,l,pK))) . perm)) + (b * ((Path_product (RLine (M,l,qK))) . perm))
set Rpq = RLine (M,l,((a * pK) + (b * qK)));
set Rp = RLine (M,l,pK);
set Rq = RLine (M,l,qK);
set Ppq = Path_matrix (perm,(RLine (M,l,((a * pK) + (b * qK)))));
set Pathpq = Path_product (RLine (M,l,((a * pK) + (b * qK))));
set Pp = Path_matrix (perm,(RLine (M,l,pK)));
set Pathp = Path_product (RLine (M,l,pK));
set Pq = Path_matrix (perm,(RLine (M,l,qK)));
set Pathq = Path_product (RLine (M,l,qK));

now :: thesis: ( ( perm is even & (Path_product (RLine (M,l,((a * pK) + (b * qK))))) . perm = (a * ((Path_product (RLine (M,l,pK))) . perm)) + (b * ((Path_product (RLine (M,l,qK))) . perm)) ) or ( perm is odd & (Path_product (RLine (M,l,((a * pK) + (b * qK))))) . perm = (a * ((Path_product (RLine (M,l,pK))) . perm)) + (b * ((Path_product (RLine (M,l,qK))) . perm)) ) )

per cases ( perm is even or perm is odd ) ;

case A4: perm is even ; :: thesis: (Path_product (RLine (M,l,((a * pK) + (b * qK))))) . perm = (a * ((Path_product (RLine (M,l,pK))) . perm)) + (b * ((Path_product (RLine (M,l,qK))) . perm))

then the multF of K $$ (Path_matrix (perm,(RLine (M,l,((a * pK) + (b * qK)))))) = - (( the multF of K $$ (Path_matrix (perm,(RLine (M,l,((a * pK) + (b * qK))))))),perm) by MATRIX_1:def 16;
then A5: (Path_product (RLine (M,l,((a * pK) + (b * qK))))) . perm = the multF of K $$ (Path_matrix (perm,(RLine (M,l,((a * pK) + (b * qK)))))) by MATRIX_3:def 8;
the multF of K $$ (Path_matrix (perm,(RLine (M,l,qK)))) = - (( the multF of K $$ (Path_matrix (perm,(RLine (M,l,qK))))),perm) by A4, MATRIX_1:def 16;
then A6: (Path_product (RLine (M,l,qK))) . perm = the multF of K $$ (Path_matrix (perm,(RLine (M,l,qK)))) by MATRIX_3:def 8;
the multF of K $$ (Path_matrix (perm,(RLine (M,l,pK)))) = - (( the multF of K $$ (Path_matrix (perm,(RLine (M,l,pK))))),perm) by A4, MATRIX_1:def 16;
then (Path_product (RLine (M,l,pK))) . perm = the multF of K $$ (Path_matrix (perm,(RLine (M,l,pK)))) by MATRIX_3:def 8;
hence (Path_product (RLine (M,l,((a * pK) + (b * qK))))) . perm = (a * ((Path_product (RLine (M,l,pK))) . perm)) + (b * ((Path_product (RLine (M,l,qK))) . perm)) by A1, A2, A3, A6, A5, Th31; :: thesis: verum

end;

case A7: perm is odd ; :: thesis: (Path_product (RLine (M,l,((a * pK) + (b * qK))))) . perm = (a * ((Path_product (RLine (M,l,pK))) . perm)) + (b * ((Path_product (RLine (M,l,qK))) . perm))

then - ( the multF of K $$ (Path_matrix (perm,(RLine (M,l,((a * pK) + (b * qK))))))) = - (( the multF of K $$ (Path_matrix (perm,(RLine (M,l,((a * pK) + (b * qK))))))),perm) by MATRIX_1:def 16;
then A8: (Path_product (RLine (M,l,((a * pK) + (b * qK))))) . perm = - ( the multF of K $$ (Path_matrix (perm,(RLine (M,l,((a * pK) + (b * qK))))))) by MATRIX_3:def 8;
- ( the multF of K $$ (Path_matrix (perm,(RLine (M,l,pK))))) = - (( the multF of K $$ (Path_matrix (perm,(RLine (M,l,pK))))),perm) by A7, MATRIX_1:def 16;
then A9: (Path_product (RLine (M,l,pK))) . perm = - ( the multF of K $$ (Path_matrix (perm,(RLine (M,l,pK))))) by MATRIX_3:def 8;
A10: - (a * ( the multF of K $$ (Path_matrix (perm,(RLine (M,l,pK)))))) = a * (- ( the multF of K $$ (Path_matrix (perm,(RLine (M,l,pK)))))) by VECTSP_1:8;
- ( the multF of K $$ (Path_matrix (perm,(RLine (M,l,qK))))) = - (( the multF of K $$ (Path_matrix (perm,(RLine (M,l,qK))))),perm) by A7, MATRIX_1:def 16;
then A11: (Path_product (RLine (M,l,qK))) . perm = - ( the multF of K $$ (Path_matrix (perm,(RLine (M,l,qK))))) by MATRIX_3:def 8;
A12: - ((a * ( the multF of K $$ (Path_matrix (perm,(RLine (M,l,pK)))))) + (b * ( the multF of K $$ (Path_matrix (perm,(RLine (M,l,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 VECTSP_1:17;
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 A1, A2, A3, Th31;
hence (Path_product (RLine (M,l,((a * pK) + (b * qK))))) . perm = (a * ((Path_product (RLine (M,l,pK))) . perm)) + (b * ((Path_product (RLine (M,l,qK))) . perm)) by A9, A11, A8, A10, A12, VECTSP_1:8; :: thesis: verum

end;

end;

end;

hence (Path_product (RLine (M,l,((a * pK) + (b * qK))))) . perm = (a * ((Path_product (RLine (M,l,pK))) . perm)) + (b * ((Path_product (RLine (M,l,qK))) . perm)) ; :: thesis: verum