let n be Nat; :: thesis:
let K be Field; :: thesis:
let i, j be Nat; :: thesis:
assume that
A1: i in Seg n and
A2: j in Seg n ; :: thesis:
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:
assume A5: PP = { p where p is Element of Permutations n : p . i = j } ; :: thesis:
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:
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₁[ 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₁[B9] & not b in B9 holds
S₁[B9 \/ {b}]

proof

let B9 be Element of Fin (Permutations n); :: thesis:
let b be Element of Permutations n; :: thesis:
assume that
A9: S₁[B9] and
A10: not b in B9 ; :: thesis:
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:
let ProjD be Element of Fin (Permutations (n -' 1)); :: thesis:
assume that
A13: D = B9 \/ {b} and
A14: ProjD = Proj .: D and
A15: D c= PP ; :: thesis:
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:
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:

end;

per cases ;

suppose A27: B9 = {} ; :: thesis:

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:

end;

suppose A29: B9 <> {} ; :: thesis:

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:

end;

A30: S₁[ {}. (Permutations n)]

proof

let B be Element of Fin (Permutations n); :: thesis:
let ProjB be Element of Fin (Permutations (n -' 1)); :: thesis:
assume that
A31: B = {}. (Permutations n) and
A32: ProjB = Proj .: B and
B c= PP ; :: thesis:
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:

end;

A35: for B being Element of Fin (Permutations n) holds S₁[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: