let n be Nat; for K being Field
for i, j being Nat st i in Seg n & j in Seg n holds
for P being Element of Fin (Permutations n) st P = { p where p is Element of Permutations n : p . i = j } holds
for M being Matrix of n,K holds the addF of K $$ (P,(Path_product M)) = (M * (i,j)) * (Cofactor (M,i,j))
let K be Field; for i, j being Nat st i in Seg n & j in Seg n holds
for P being Element of Fin (Permutations n) st P = { p where p is Element of Permutations n : p . i = j } holds
for M being Matrix of n,K holds the addF of K $$ (P,(Path_product M)) = (M * (i,j)) * (Cofactor (M,i,j))
let i, j be Nat; ( i in Seg n & j in Seg n implies for P being Element of Fin (Permutations n) st P = { p where p is Element of Permutations n : p . i = j } holds
for M being Matrix of n,K holds the addF of K $$ (P,(Path_product M)) = (M * (i,j)) * (Cofactor (M,i,j)) )
assume that
A1:
i in Seg n
and
A2:
j in Seg n
; for P being Element of Fin (Permutations n) st P = { p where p is Element of Permutations n : p . i = j } holds
for M being Matrix of n,K holds the addF of K $$ (P,(Path_product M)) = (M * (i,j)) * (Cofactor (M,i,j))
n > 0
by A1;
then reconsider n9 = n - 1 as Element of NAT by NAT_1:20;
set P = Permutations (n -' 1);
set n91 = n9 + 1;
set P1 = Permutations n;
A3:
(n9 + 1) -' 1 = (n9 + 1) - 1
by XREAL_0:def 2;
set aa = the addF of K;
Permutations (n -' 1) in Fin (Permutations (n -' 1))
by FINSUB_1:def 5;
then A4:
In ((Permutations (n -' 1)),(Fin (Permutations (n -' 1)))) = Permutations (n -' 1)
by SUBSET_1:def 8;
let PP be Element of Fin (Permutations n); ( PP = { p where p is Element of Permutations n : p . i = j } implies for M being Matrix of n,K holds the addF of K $$ (PP,(Path_product M)) = (M * (i,j)) * (Cofactor (M,i,j)) )
assume A5:
PP = { p where p is Element of Permutations n : p . i = j }
; for M being Matrix of n,K holds the addF of K $$ (PP,(Path_product M)) = (M * (i,j)) * (Cofactor (M,i,j))
consider Proj being Function of PP,(Permutations (n -' 1)) such that
A6:
Proj is bijective
and
A7:
for q being Element of Permutations (n9 + 1) st q . i = j holds
Proj . q = Rem (q,i)
by A1, A2, A5, A3, Th20;
let M be Matrix of n,K; the addF of K $$ (PP,(Path_product M)) = (M * (i,j)) * (Cofactor (M,i,j))
set DM = Delete (M,i,j);
set PathM = Path_product M;
set PathDM = Path_product (Delete (M,i,j));
set pm = ((power K) . ((- (1_ K)),(i + j))) * (M * (i,j));
defpred S1[ set ] means for D being Element of Fin (Permutations n)
for ProjD being Element of Fin (Permutations (n -' 1)) st D = $1 & ProjD = Proj .: D & D c= PP holds
the addF of K $$ (D,(Path_product M)) = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ( the addF of K $$ (ProjD,(Path_product (Delete (M,i,j)))));
A8:
for B9 being Element of Fin (Permutations n)
for b being Element of Permutations n st S1[B9] & not b in B9 holds
S1[B9 \/ {b}]
proof
let B9 be
Element of
Fin (Permutations n);
for b being Element of Permutations n st S1[B9] & not b in B9 holds
S1[B9 \/ {b}]let b be
Element of
Permutations n;
( S1[B9] & not b in B9 implies S1[B9 \/ {b}] )
assume that A9:
S1[
B9]
and A10:
not
b in B9
;
S1[B9 \/ {b}]
A11:
b in {b}
by TARSKI:def 1;
A12:
rng Proj = Permutations (n -' 1)
by A6, FUNCT_2:def 3;
then
Proj .: B9 c= Permutations (n -' 1)
by RELAT_1:111;
then reconsider ProjB9 =
Proj .: B9 as
Element of
Fin (Permutations (n -' 1)) by FINSUB_1:def 5;
let D be
Element of
Fin (Permutations n);
for ProjD being Element of Fin (Permutations (n -' 1)) st D = B9 \/ {b} & ProjD = Proj .: D & D c= PP holds
the addF of K $$ (D,(Path_product M)) = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ( the addF of K $$ (ProjD,(Path_product (Delete (M,i,j)))))let ProjD be
Element of
Fin (Permutations (n -' 1));
( D = B9 \/ {b} & ProjD = Proj .: D & D c= PP implies the addF of K $$ (D,(Path_product M)) = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ( the addF of K $$ (ProjD,(Path_product (Delete (M,i,j))))) )
assume that A13:
D = B9 \/ {b}
and A14:
ProjD = Proj .: D
and A15:
D c= PP
;
the addF of K $$ (D,(Path_product M)) = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ( the addF of K $$ (ProjD,(Path_product (Delete (M,i,j)))))
A16:
B9 c= D
by A13, XBOOLE_1:7;
B9 c= D
by A13, XBOOLE_1:7;
then A17:
B9 c= PP
by A15;
{b} c= D
by A13, XBOOLE_1:7;
then A18:
b in PP
by A15, A11;
then consider Q1 being
Element of
Permutations n such that A19:
Q1 = b
and A20:
Q1 . i = j
by A5;
A21:
dom Proj = PP
by FUNCT_2:def 1;
then A22:
Im (
Proj,
b)
= {(Proj . b)}
by A18, FUNCT_1:59;
reconsider Q =
Proj . b as
Element of
Permutations (n -' 1) by A18, A21, A12, FUNCT_1:def 3;
A23:
Proj . b in rng Proj
by A18, A21, FUNCT_1:def 3;
reconsider Q19 =
Q1 as
Element of
Permutations (n9 + 1) ;
A24:
Rem (
Q19,
i)
= Q
by A7, A19, A20;
then A25:
(Path_product M) . Q1 = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product (Delete (M,i,j))) . Q)
by A1, A3, A20, Th22;
A26:
not
Q in ProjB9
per cases
( B9 = {} or B9 <> {} )
;
suppose A27:
B9 = {}
;
the addF of K $$ (D,(Path_product M)) = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ( the addF of K $$ (ProjD,(Path_product (Delete (M,i,j)))))then A28:
the
addF of
K $$ (
D,
(Path_product M))
= (Path_product M) . b
by A13, SETWISEO:17;
the
addF of
K $$ (
ProjD,
(Path_product (Delete (M,i,j))))
= (Path_product (Delete (M,i,j))) . (Proj . b)
by A13, A14, A22, A23, A12, A27, SETWISEO:17;
hence
the
addF of
K $$ (
D,
(Path_product M))
= (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ( the addF of K $$ (ProjD,(Path_product (Delete (M,i,j)))))
by A1, A3, A19, A20, A24, A28, Th22;
verum end; suppose A29:
B9 <> {}
;
the addF of K $$ (D,(Path_product M)) = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ( the addF of K $$ (ProjD,(Path_product (Delete (M,i,j)))))
ProjD = ProjB9 \/ {Q}
by A13, A14, A22, RELAT_1:120;
hence (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ( the addF of K $$ (ProjD,(Path_product (Delete (M,i,j))))) =
(((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * (( the addF of K $$ (ProjB9,(Path_product (Delete (M,i,j))))) + ((Path_product (Delete (M,i,j))) . Q))
by A18, A17, A21, A26, A29, SETWOP_2:2
.=
((((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ( the addF of K $$ (ProjB9,(Path_product (Delete (M,i,j)))))) + ((((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product (Delete (M,i,j))) . Q))
by VECTSP_1:def 2
.=
the
addF of
K . (
( the addF of K $$ (B9,(Path_product M))),
((Path_product M) . b))
by A9, A15, A19, A16, A25, XBOOLE_1:1
.=
the
addF of
K $$ (
D,
(Path_product M))
by A10, A13, A29, SETWOP_2:2
;
verum end;
end;
A30:
S1[ {}. (Permutations n)]
proof
let B be
Element of
Fin (Permutations n);
for ProjD being Element of Fin (Permutations (n -' 1)) st B = {}. (Permutations n) & ProjD = Proj .: B & B c= PP holds
the addF of K $$ (B,(Path_product M)) = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ( the addF of K $$ (ProjD,(Path_product (Delete (M,i,j)))))let ProjB be
Element of
Fin (Permutations (n -' 1));
( B = {}. (Permutations n) & ProjB = Proj .: B & B c= PP implies the addF of K $$ (B,(Path_product M)) = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ( the addF of K $$ (ProjB,(Path_product (Delete (M,i,j))))) )
assume that A31:
B = {}. (Permutations n)
and A32:
ProjB = Proj .: B
and
B c= PP
;
the addF of K $$ (B,(Path_product M)) = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ( the addF of K $$ (ProjB,(Path_product (Delete (M,i,j)))))
ProjB = {}. (Permutations (n -' 1))
by A31, A32;
then A33:
the
addF of
K $$ (
ProjB,
(Path_product (Delete (M,i,j))))
= the_unity_wrt the
addF of
K
by FVSUM_1:8, SETWISEO:31;
A34:
the_unity_wrt the
addF of
K = 0. K
by FVSUM_1:7;
the
addF of
K $$ (
B,
(Path_product M))
= the_unity_wrt the
addF of
K
by A31, FVSUM_1:8, SETWISEO:31;
hence
the
addF of
K $$ (
B,
(Path_product M))
= (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ( the addF of K $$ (ProjB,(Path_product (Delete (M,i,j)))))
by A33, A34;
verum
end;
A35:
for B being Element of Fin (Permutations n) holds S1[B]
from SETWISEO:sch 2(A30, A8);
A36:
dom Proj = PP
by FUNCT_2:def 1;
rng Proj = Permutations (n -' 1)
by A6, FUNCT_2:def 3;
then
Proj .: PP = In ((Permutations (n -' 1)),(Fin (Permutations (n -' 1))))
by A4, A36, RELAT_1:113;
hence the addF of K $$ (PP,(Path_product M)) =
((M * (i,j)) * ((power K) . ((- (1_ K)),(i + j)))) * (Det (Delete (M,i,j)))
by A35
.=
(M * (i,j)) * (Cofactor (M,i,j))
by GROUP_1:def 3
;
verum