let n be Nat; for p1 being Element of Permutations (n + 1)
for K being Field
for i, j being Nat st i in Seg (n + 1) & p1 . i = j holds
for M being Matrix of n + 1,K
for DM being Matrix of n,K st DM = Delete M,i,j holds
(Path_product M) . p1 = (((power K) . (- (1_ K)),(i + j)) * (M * i,j)) * ((Path_product DM) . (Rem p1,i))
let p1 be Element of Permutations (n + 1); for K being Field
for i, j being Nat st i in Seg (n + 1) & p1 . i = j holds
for M being Matrix of n + 1,K
for DM being Matrix of n,K st DM = Delete M,i,j holds
(Path_product M) . p1 = (((power K) . (- (1_ K)),(i + j)) * (M * i,j)) * ((Path_product DM) . (Rem p1,i))
let K be Field; for i, j being Nat st i in Seg (n + 1) & p1 . i = j holds
for M being Matrix of n + 1,K
for DM being Matrix of n,K st DM = Delete M,i,j holds
(Path_product M) . p1 = (((power K) . (- (1_ K)),(i + j)) * (M * i,j)) * ((Path_product DM) . (Rem p1,i))
reconsider N = n as Element of NAT by ORDINAL1:def 13;
set n1 = N + 1;
let i, j be Nat; ( i in Seg (n + 1) & p1 . i = j implies for M being Matrix of n + 1,K
for DM being Matrix of n,K st DM = Delete M,i,j holds
(Path_product M) . p1 = (((power K) . (- (1_ K)),(i + j)) * (M * i,j)) * ((Path_product DM) . (Rem p1,i)) )
assume that
A1:
i in Seg (n + 1)
and
A2:
p1 . i = j
; for M being Matrix of n + 1,K
for DM being Matrix of n,K st DM = Delete M,i,j holds
(Path_product M) . p1 = (((power K) . (- (1_ K)),(i + j)) * (M * i,j)) * ((Path_product DM) . (Rem p1,i))
set mm = the multF of K;
set R = Rem p1,i;
let M be Matrix of n + 1,K; for DM being Matrix of n,K st DM = Delete M,i,j holds
(Path_product M) . p1 = (((power K) . (- (1_ K)),(i + j)) * (M * i,j)) * ((Path_product DM) . (Rem p1,i))
let DM be Matrix of n,K; ( DM = Delete M,i,j implies (Path_product M) . p1 = (((power K) . (- (1_ K)),(i + j)) * (M * i,j)) * ((Path_product DM) . (Rem p1,i)) )
assume A3:
DM = Delete M,i,j
; (Path_product M) . p1 = (((power K) . (- (1_ K)),(i + j)) * (M * i,j)) * ((Path_product DM) . (Rem p1,i))
set PR = Path_matrix (Rem p1,i),DM;
set Pp1 = Path_matrix p1,M;
len (Path_matrix p1,M) = N + 1
by MATRIX_3:def 7;
then
dom (Path_matrix p1,M) = Seg (N + 1)
by FINSEQ_1:def 3;
then A4:
(Path_matrix p1,M) . i = M * i,j
by A1, A2, MATRIX_3:def 7;
A5:
now per cases
( N = 0 or N > 0 )
;
suppose A6:
N = 0
;
the multF of K $$ (Path_matrix p1,M) = (M * i,j) * (the multF of K $$ (Path_matrix (Rem p1,i),DM))then A7:
len (Path_matrix p1,M) = 1
by MATRIX_3:def 7;
(Path_matrix p1,M) . 1
= M * i,
j
by A1, A4, A6, FINSEQ_1:4, TARSKI:def 1;
then
Path_matrix p1,
M = <*(M * i,j)*>
by A7, FINSEQ_1:57;
then A8:
the
multF of
K $$ (Path_matrix p1,M) = M * i,
j
by FINSOP_1:12;
len (Path_matrix (Rem p1,i),DM) = 0
by A6, MATRIX_3:def 7;
then
Path_matrix (Rem p1,i),
DM = <*> the
carrier of
K
;
then A9:
the
multF of
K $$ (Path_matrix (Rem p1,i),DM) = the_unity_wrt the
multF of
K
by FINSOP_1:11;
the_unity_wrt the
multF of
K = 1_ K
by FVSUM_1:7;
hence
the
multF of
K $$ (Path_matrix p1,M) = (M * i,j) * (the multF of K $$ (Path_matrix (Rem p1,i),DM))
by A8, A9, VECTSP_1:def 13;
verum end; suppose A10:
N > 0
;
the multF of K $$ (Path_matrix p1,M) = (M * i,j) * (the multF of K $$ (Path_matrix (Rem p1,i),DM))
len (Path_matrix (Rem p1,i),DM) = n
by MATRIX_3:def 7;
then consider f being
Function of
NAT ,the
carrier of
K such that A11:
f . 1
= (Path_matrix (Rem p1,i),DM) . 1
and A12:
for
k being
Element of
NAT st
0 <> k &
k < n holds
f . (k + 1) = the
multF of
K . (f . k),
((Path_matrix (Rem p1,i),DM) . (k + 1))
and A13:
the
multF of
K $$ (Path_matrix (Rem p1,i),DM) = f . n
by A10, FINSOP_1:def 1;
len (Path_matrix p1,M) = N + 1
by MATRIX_3:def 7;
then consider F being
Function of
NAT ,the
carrier of
K such that A14:
F . 1
= (Path_matrix p1,M) . 1
and A15:
for
k being
Element of
NAT st
0 <> k &
k < N + 1 holds
F . (k + 1) = the
multF of
K . (F . k),
((Path_matrix p1,M) . (k + 1))
and A16:
the
multF of
K $$ (Path_matrix p1,M) = F . (N + 1)
by FINSOP_1:def 1;
defpred S1[
Nat]
means ( 1
<= $1 & $1
< i implies
f . $1
= F . $1 );
A17:
for
k being
Nat st
k in Seg n holds
( (
k < i implies
(Path_matrix (Rem p1,i),DM) . k = (Path_matrix p1,M) . k ) & (
k >= i implies
(Path_matrix (Rem p1,i),DM) . k = (Path_matrix p1,M) . (k + 1) ) )
proof
len (Path_matrix p1,M) = N + 1
by MATRIX_3:def 7;
then A18:
dom (Path_matrix p1,M) = Seg (N + 1)
by FINSEQ_1:def 3;
len (Path_matrix (Rem p1,i),DM) = n
by MATRIX_3:def 7;
then A19:
dom (Path_matrix (Rem p1,i),DM) = Seg n
by FINSEQ_1:def 3;
reconsider p19 =
p1 as
Permutation of
(Seg (N + 1)) by MATRIX_2:def 11;
reconsider R9 =
Rem p1,
i as
Permutation of
(Seg n) by MATRIX_2:def 11;
let k be
Nat;
( k in Seg n implies ( ( k < i implies (Path_matrix (Rem p1,i),DM) . k = (Path_matrix p1,M) . k ) & ( k >= i implies (Path_matrix (Rem p1,i),DM) . k = (Path_matrix p1,M) . (k + 1) ) ) )
assume A20:
k in Seg n
;
( ( k < i implies (Path_matrix (Rem p1,i),DM) . k = (Path_matrix p1,M) . k ) & ( k >= i implies (Path_matrix (Rem p1,i),DM) . k = (Path_matrix p1,M) . (k + 1) ) )
reconsider k1 =
k + 1 as
Element of
NAT ;
A21:
k1 in Seg (N + 1)
by A20, FINSEQ_1:81;
A22:
rng p19 = Seg (N + 1)
by FUNCT_2:def 3;
dom p19 = Seg (N + 1)
by FUNCT_2:67;
then A23:
j in Seg (N + 1)
by A1, A2, A22, FUNCT_1:def 5;
A24:
rng R9 = Seg n
by FUNCT_2:def 3;
dom R9 = Seg n
by FUNCT_2:67;
then A25:
(Rem p1,i) . k in Seg n
by A20, A24, FUNCT_1:def 5;
then consider Rk being
Element of
NAT such that A26:
Rk = (Rem p1,i) . k
and
1
<= Rk
and
Rk <= n
;
A27:
(N + 1) -' 1
= (N + 1) - 1
by XREAL_0:def 2;
n <= N + 1
by NAT_1:11;
then A28:
Seg n c= Seg (N + 1)
by FINSEQ_1:7;
thus
(
k < i implies
(Path_matrix (Rem p1,i),DM) . k = (Path_matrix p1,M) . k )
( k >= i implies (Path_matrix (Rem p1,i),DM) . k = (Path_matrix p1,M) . (k + 1) )proof
assume A29:
k < i
;
(Path_matrix (Rem p1,i),DM) . k = (Path_matrix p1,M) . k
dom p19 = Seg (N + 1)
by FUNCT_2:67;
then
p19 . k <> p19 . i
by A1, A20, A28, A29, FUNCT_1:def 8;
then
(
p1 . k < j or
p1 . k > j )
by A2, XXREAL_0:1;
then
( (
Rk = p1 . k &
p1 . k < j ) or (
p1 . k > j &
Rk = (p1 . k) - 1 ) )
by A1, A2, A20, A26, A29, Def3;
then
( (
Rk = p1 . k &
p1 . k < j ) or (
p1 . k > j &
p1 . k = Rk + 1 ) )
;
then
( (
Rk = p1 . k &
p1 . k < j ) or (
p1 . k > j &
Rk >= j &
p1 . k = Rk + 1 ) )
by NAT_1:13;
then
( (
DM * k,
Rk = M * k,
Rk &
(Path_matrix (Rem p1,i),DM) . k = DM * k,
Rk &
(Path_matrix p1,M) . k = M * k,
Rk ) or (
(Path_matrix (Rem p1,i),DM) . k = DM * k,
Rk &
DM * k,
Rk = M * k,
(Rk + 1) &
(Path_matrix p1,M) . k = M * k,
(Rk + 1) ) )
by A1, A3, A20, A25, A23, A26, A28, A27, A19, A18, A29, Th13, MATRIX_3:def 7;
hence
(Path_matrix (Rem p1,i),DM) . k = (Path_matrix p1,M) . k
;
verum
end;
A30:
dom p19 = Seg (N + 1)
by FUNCT_2:67;
assume A31:
k >= i
;
(Path_matrix (Rem p1,i),DM) . k = (Path_matrix p1,M) . (k + 1)
then
k1 > i
by NAT_1:13;
then
p19 . k1 <> p19 . i
by A1, A21, A30, FUNCT_1:def 8;
then
(
p1 . k1 < j or
p1 . k1 > j )
by A2, XXREAL_0:1;
then
( (
Rk = p1 . k1 &
p1 . k1 < j ) or (
p1 . k1 > j &
Rk = (p1 . k1) - 1 ) )
by A1, A2, A20, A26, A31, Def3;
then
( (
Rk = p1 . k1 &
p1 . k1 < j ) or (
p1 . k1 > j &
p1 . k1 = Rk + 1 ) )
;
then
( (
Rk = p1 . k1 &
p1 . k1 < j ) or (
p1 . k1 > j &
Rk >= j &
p1 . k1 = Rk + 1 ) )
by NAT_1:13;
then
( (
DM * k,
Rk = M * (k + 1),
Rk &
(Path_matrix (Rem p1,i),DM) . k = DM * k,
Rk &
(Path_matrix p1,M) . k1 = M * (k + 1),
Rk ) or (
(Path_matrix (Rem p1,i),DM) . k = DM * k,
Rk &
DM * k,
Rk = M * (k + 1),
(Rk + 1) &
(Path_matrix p1,M) . k1 = M * k1,
(Rk + 1) ) )
by A1, A3, A20, A25, A23, A26, A27, A21, A19, A18, A31, Th13, MATRIX_3:def 7;
hence
(Path_matrix (Rem p1,i),DM) . k = (Path_matrix p1,M) . (k + 1)
;
verum
end; A32:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A33:
S1[
k]
;
S1[k + 1]
reconsider e =
k as
Element of
NAT by ORDINAL1:def 13;
assume that A34:
1
<= k + 1
and A35:
k + 1
< i
;
f . (k + 1) = F . (k + 1)
set k1 =
e + 1;
i <= N + 1
by A1, FINSEQ_1:3;
then
e + 1
< N + 1
by A35, XXREAL_0:2;
then
e + 1
<= n
by NAT_1:13;
then A36:
e + 1
in Seg N
by A34;
per cases
( k = 0 or k >= 1 )
by NAT_1:14;
suppose A37:
k >= 1
;
f . (k + 1) = F . (k + 1)
i <= N + 1
by A1, FINSEQ_1:3;
then A38:
e + 1
< N + 1
by A35, XXREAL_0:2;
then
k < N + 1
by NAT_1:13;
then A39:
F . (e + 1) = the
multF of
K . (F . k),
((Path_matrix p1,M) . (e + 1))
by A15, A37;
e + 1
<= n
by A38, NAT_1:13;
then A40:
e + 1
in Seg N
by A34;
k < n
by A38, XREAL_1:8;
then
f . (e + 1) = the
multF of
K . (f . k),
((Path_matrix (Rem p1,i),DM) . (e + 1))
by A12, A37;
hence
f . (k + 1) = F . (k + 1)
by A17, A33, A35, A37, A39, A40, NAT_1:13;
verum end;
end; defpred S2[
Nat]
means (
i <= $1 & $1
<= N + 1 implies ( ( $1
= 1 implies
F . $1
= M * i,
j ) & ( $1
> 1 implies for
a being
Element of
K st
a = f . ($1 - 1) holds
F . $1
= (M * i,j) * a ) ) );
A41:
S1[
0 ]
;
A42:
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A41, A32);
A43:
for
k being
Nat st
S2[
k] holds
S2[
k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
assume A44:
S2[
k]
;
S2[k + 1]
set k1 =
k + 1;
assume that A45:
i <= k + 1
and A46:
k + 1
<= N + 1
;
( ( k + 1 = 1 implies F . (k + 1) = M * i,j ) & ( k + 1 > 1 implies for a being Element of K st a = f . ((k + 1) - 1) holds
F . (k + 1) = (M * i,j) * a ) )
per cases
( k = 0 or k > 0 )
;
suppose A47:
k = 0
;
( ( k + 1 = 1 implies F . (k + 1) = M * i,j ) & ( k + 1 > 1 implies for a being Element of K st a = f . ((k + 1) - 1) holds
F . (k + 1) = (M * i,j) * a ) )end; suppose A48:
k > 0
;
( ( k + 1 = 1 implies F . (k + 1) = M * i,j ) & ( k + 1 > 1 implies for a being Element of K st a = f . ((k + 1) - 1) holds
F . (k + 1) = (M * i,j) * a ) )hence
(
k + 1
= 1 implies
F . (k + 1) = M * i,
j )
;
( k + 1 > 1 implies for a being Element of K st a = f . ((k + 1) - 1) holds
F . (k + 1) = (M * i,j) * a )assume
k + 1
> 1
;
for a being Element of K st a = f . ((k + 1) - 1) holds
F . (k + 1) = (M * i,j) * alet a be
Element of
K;
( a = f . ((k + 1) - 1) implies F . (k + 1) = (M * i,j) * a )assume A49:
a = f . ((k + 1) - 1)
;
F . (k + 1) = (M * i,j) * aA50:
k <= n
by A46, XREAL_1:8;
k >= 1
by A48, NAT_1:14;
then A51:
k in Seg n
by A50, FINSEQ_1:3;
len (Path_matrix (Rem p1,i),DM) = n
by MATRIX_3:def 7;
then A52:
dom (Path_matrix (Rem p1,i),DM) = Seg n
by FINSEQ_1:def 3;
then A53:
(Path_matrix (Rem p1,i),DM) . k = DM * k,
((Rem p1,i) . k)
by A51, MATRIX_3:def 7;
k < N + 1
by A46, NAT_1:13;
then A54:
F . (k + 1) = the
multF of
K . (F . k),
((Path_matrix p1,M) . (k + 1))
by A15, A48, A51;
per cases
( k + 1 = i or k + 1 > i )
by A45, XXREAL_0:1;
suppose A56:
k + 1
> i
;
F . (k + 1) = (M * i,j) * aA57:
k < N + 1
by A46, NAT_1:13;
A58:
k >= i
by A56, NAT_1:13;
i >= 1
by A1, FINSEQ_1:3;
then A59:
k >= 1
by A58, XXREAL_0:2;
per cases
( k = 1 or k > 1 )
by A59, XXREAL_0:1;
suppose A60:
k > 1
;
F . (k + 1) = (M * i,j) * areconsider k9 =
k - 1 as
Element of
NAT by A48, NAT_1:20;
reconsider fk9 =
f . k9 as
Element of
K ;
k9 + 1
<= n
by A57, NAT_1:13;
then A61:
k9 < n
by NAT_1:13;
k9 + 1
> 0 + 1
by A60;
then A62:
a = the
multF of
K . fk9,
((Path_matrix (Rem p1,i),DM) . (k9 + 1))
by A12, A49, A61;
F . k = (M * i,j) * fk9
by A44, A46, A56, A60, NAT_1:13;
hence F . (k + 1) =
((M * i,j) * fk9) * (DM * k,((Rem p1,i) . k))
by A17, A51, A54, A53, A58
.=
(M * i,j) * (fk9 * (DM * k,((Rem p1,i) . k)))
by GROUP_1:def 4
.=
(M * i,j) * a
by A51, A52, A62, MATRIX_3:def 7
;
verum end; end; end;
end; A63:
S2[
0 ]
;
A64:
for
k being
Nat holds
S2[
k]
from NAT_1:sch 2(A63, A43);
A65:
i <= N + 1
by A1, FINSEQ_1:3;
A66:
(N + 1) - 1
= n
;
N + 1
> 0 + 1
by A10, XREAL_1:8;
hence
the
multF of
K $$ (Path_matrix p1,M) = (M * i,j) * (the multF of K $$ (Path_matrix (Rem p1,i),DM))
by A16, A13, A64, A65, A66;
verum end;
per cases
( Rem p1,i is even or not Rem p1,i is even )
;
suppose A67:
Rem p1,
i is
even
;
(Path_product M) . p1 = (((power K) . (- (1_ K)),(i + j)) * (M * i,j)) * ((Path_product DM) . (Rem p1,i))thus (Path_product M) . p1 =
- (the multF of K $$ (Path_matrix p1,M)),
p1
by MATRIX_3:def 8
.=
((power K) . (- (1_ K)),(i + j)) * (- (the multF of K $$ (Path_matrix p1,M)),(Rem p1,i))
by A1, A2, Th21
.=
((power K) . (- (1_ K)),(i + j)) * ((M * i,j) * (the multF of K $$ (Path_matrix (Rem p1,i),DM)))
by A5, A67, MATRIX_2:def 16
.=
(((power K) . (- (1_ K)),(i + j)) * (M * i,j)) * (the multF of K $$ (Path_matrix (Rem p1,i),DM))
by GROUP_1:def 4
.=
(((power K) . (- (1_ K)),(i + j)) * (M * i,j)) * (- (the multF of K $$ (Path_matrix (Rem p1,i),DM)),(Rem p1,i))
by A67, MATRIX_2:def 16
.=
(((power K) . (- (1_ K)),(i + j)) * (M * i,j)) * ((Path_product DM) . (Rem p1,i))
by MATRIX_3:def 8
;
verum end; suppose A68:
not
Rem p1,
i is
even
;
(Path_product M) . p1 = (((power K) . (- (1_ K)),(i + j)) * (M * i,j)) * ((Path_product DM) . (Rem p1,i))thus (Path_product M) . p1 =
- (the multF of K $$ (Path_matrix p1,M)),
p1
by MATRIX_3:def 8
.=
((power K) . (- (1_ K)),(i + j)) * (- (the multF of K $$ (Path_matrix p1,M)),(Rem p1,i))
by A1, A2, Th21
.=
((power K) . (- (1_ K)),(i + j)) * (- ((M * i,j) * (the multF of K $$ (Path_matrix (Rem p1,i),DM))))
by A5, A68, MATRIX_2:def 16
.=
((power K) . (- (1_ K)),(i + j)) * ((M * i,j) * (- (the multF of K $$ (Path_matrix (Rem p1,i),DM))))
by VECTSP_1:40
.=
(((power K) . (- (1_ K)),(i + j)) * (M * i,j)) * (- (the multF of K $$ (Path_matrix (Rem p1,i),DM)))
by GROUP_1:def 4
.=
(((power K) . (- (1_ K)),(i + j)) * (M * i,j)) * (- (the multF of K $$ (Path_matrix (Rem p1,i),DM)),(Rem p1,i))
by A68, MATRIX_2:def 16
.=
(((power K) . (- (1_ K)),(i + j)) * (M * i,j)) * ((Path_product DM) . (Rem p1,i))
by MATRIX_3:def 8
;
verum end;