let n be Nat; 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; 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; 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; 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; 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; ( 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
; 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; (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 ( ( 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
;
(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;
verum end; case A7:
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))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;
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))
; verum