let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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); :: thesis: ( 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 } ; :: thesis: 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; :: thesis: 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 S_{1}[ 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 S_{1}[B9] & not b in B9 holds

S_{1}[B9 \/ {b}]
_{1}[ {}. (Permutations n)]
_{1}[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 ;

:: thesis: verum

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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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); :: thesis: ( 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 } ; :: thesis: 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; :: thesis: 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 S

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 S

S

proof

A30:
S
let B9 be Element of Fin (Permutations n); :: thesis: for b being Element of Permutations n st S_{1}[B9] & not b in B9 holds

S_{1}[B9 \/ {b}]

let b be Element of Permutations n; :: thesis: ( S_{1}[B9] & not b in B9 implies S_{1}[B9 \/ {b}] )

assume that

A9: S_{1}[B9]
and

A10: not b in B9 ; :: thesis: S_{1}[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); :: thesis: 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)); :: thesis: ( 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 ; :: thesis: 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

end;S

let b be Element of Permutations n; :: thesis: ( S

assume that

A9: S

A10: not b in B9 ; :: thesis: S

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); :: thesis: 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)); :: thesis: ( 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 ; :: thesis: 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

proof

assume
Q in ProjB9
; :: thesis: contradiction

then ex x being object st

( x in dom Proj & x in B9 & Proj . x = Q ) by FUNCT_1:def 6;

hence contradiction by A6, A10, A18, A21, FUNCT_1:def 4; :: thesis: verum

end;then ex x being object st

( x in dom Proj & x in B9 & Proj . x = Q ) by FUNCT_1:def 6;

hence contradiction by A6, A10, A18, A21, FUNCT_1:def 4; :: thesis: verum

per cases
( B9 = {} or B9 <> {} )
;

end;

suppose A27:
B9 = {}
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

suppose A29:
B9 <> {}
; :: thesis: 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 ;

:: thesis: verum

end;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 ;

:: thesis: verum

proof

A35:
for B being Element of Fin (Permutations n) holds S
let B be Element of Fin (Permutations n); :: thesis: 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)); :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;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)); :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

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 ;

:: thesis: verum