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 12;
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 the multF of K $$ (Path_matrix (p1,M)) = (M * (i,j)) * ( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM)))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:2, TARSKI:def 1;
then
Path_matrix (
p1,
M)
= <*(M * (i,j))*>
by A7, FINSEQ_1:40;
then A8:
the
multF of
K $$ (Path_matrix (p1,M)) = M * (
i,
j)
by FINSOP_1:11;
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:10;
the_unity_wrt the
multF of
K = 1_ K
by FVSUM_1:5;
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;
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
sequence of the
carrier of
K such that A11:
f . 1
= (Path_matrix ((Rem (p1,i)),DM)) . 1
and A12:
for
k being
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
sequence of the
carrier of
K such that A14:
F . 1
= (Path_matrix (p1,M)) . 1
and A15:
for
k being
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_1:def 12;
reconsider R9 =
Rem (
p1,
i) as
Permutation of
(Seg n) by MATRIX_1:def 12;
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:60;
A22:
rng p19 = Seg (N + 1)
by FUNCT_2:def 3;
dom p19 = Seg (N + 1)
by FUNCT_2:52;
then A23:
j in Seg (N + 1)
by A1, A2, A22, FUNCT_1:def 3;
A24:
rng R9 = Seg n
by FUNCT_2:def 3;
dom R9 = Seg n
by FUNCT_2:52;
then A25:
(Rem (p1,i)) . k in Seg n
by A20, A24, FUNCT_1:def 3;
then consider Rk being
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:5;
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:52;
then
p19 . k <> p19 . i
by A1, A20, A28, A29, FUNCT_1:def 4;
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:52;
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 4;
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 12;
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:1;
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:1;
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:6;
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:6;
k >= 1
by A48, NAT_1:14;
then A51:
k in Seg n
by A50;
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;
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:1;
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 3
.=
(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:1;
A66:
(N + 1) - 1
= n
;
N + 1
> 0 + 1
by A10, XREAL_1:6;
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 Rem (p1,i) is odd )
;
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_1: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 3
.=
(((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_1: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:
Rem (
p1,
i) is
odd
;
(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_1:def 16
.=
((power K) . ((- (1_ K)),(i + j))) * ((M * (i,j)) * (- ( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM)))))
by VECTSP_1:8
.=
(((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * (- ( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM))))
by GROUP_1:def 3
.=
(((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_1:def 16
.=
(((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i)))
by MATRIX_3:def 8
;
verum end;