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 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 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 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; 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; 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; 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; ( 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
; 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))))))
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; 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)))));
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 S1[ 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 ;
( 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 A19:
k in Seg n
;
( ( 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) ) ) )
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 ) )
( 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 A33:
k <> L
;
( (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 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;
verum
end;
assume A36:
k = L
;
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 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
;
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
;
( 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 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;
verum
end;
A39:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A40:
S1[
k]
;
S1[k + 1]
set k1 =
k + 1;
assume that A41:
1
<= k + 1
and A42:
k + 1
< L
;
( fp . (k + 1) = fq . (k + 1) & fpq . (k + 1) = fp . (k + 1) )
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 ( ( k = 0 & fp . (k + 1) = fq . (k + 1) & fpq . (k + 1) = fp . (k + 1) ) or ( k > 0 & fp . (k + 1) = fq . (k + 1) & fpq . (k + 1) = fp . (k + 1) ) )per cases
( k = 0 or k > 0 )
;
case A46:
k > 0
;
( fp . (k + 1) = fq . (k + 1) & fpq . (k + 1) = fp . (k + 1) )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;
verum end; end; end;
hence
(
fp . (k + 1) = fq . (k + 1) &
fpq . (k + 1) = fp . (k + 1) )
;
verum
end;
defpred S2[ 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:
S1[ 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 ( ( L > 1 & fpq . L = (a * (fp . L)) + (b * (fq . L)) ) or ( L = 1 & fpq . L = (a * (fp . L)) + (b * (fq . L)) ) )per cases
( L > 1 or L = 1 )
by A55, XXREAL_0:1;
case A56:
L > 1
;
fpq . L = (a * (fp . L)) + (b * (fq . L))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
S1[
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;
verum end; end; end;
hence
fpq . L = (a * (fp . L)) + (b * (fq . L))
;
verum
end;
A64:
for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
assume A65:
S2[
k]
;
S2[k + 1]
set k1 =
k + 1;
assume that A66:
1
<= k + 1
and A67:
L <= k + 1
and A68:
k + 1
<= n
;
for k being Nat st k + 1 = k holds
fpq . k = (a * (fp . k)) + (b * (fq . k))
let k9 be
Nat;
( k + 1 = k9 implies fpq . k9 = (a * (fp . k9)) + (b * (fq . k9)) )
assume A69:
k9 = k + 1
;
fpq . k9 = (a * (fp . k9)) + (b * (fq . k9))
now ( ( k + 1 = L & fpq . k9 = (a * (fp . k9)) + (b * (fq . k9)) ) or ( k + 1 > L & fpq . k9 = (a * (fp . k9)) + (b * (fq . k9)) ) )per cases
( k + 1 = L or k + 1 > L )
by A67, XXREAL_0:1;
case
k + 1
= L
;
fpq . k9 = (a * (fp . k9)) + (b * (fq . k9))hence
fpq . k9 = (a * (fp . k9)) + (b * (fq . k9))
by A51, A69;
verum end; case A70:
k + 1
> L
;
fpq . k9 = (a * (fp . k9)) + (b * (fq . k9))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;
verum end; end; end;
hence
fpq . k9 = (a * (fp . k9)) + (b * (fq . k9))
;
verum
end;
A80:
L <= n
by A1, FINSEQ_1:1;
A81:
S2[ 0 ]
;
for k being Nat holds S2[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; verum