let K be Field; :: thesis: for n being Nat
for A being Matrix of n,K st n >= 1 & A is V196(K) holds
Det A = the multF of K $$ (diagonal_of_Matrix A)
let n be Nat; :: thesis: for A being Matrix of n,K st n >= 1 & A is V196(K) holds
Det A = the multF of K $$ (diagonal_of_Matrix A)
let A be Matrix of n,K; :: thesis: ( n >= 1 & A is V196(K) implies Det A = the multF of K $$ (diagonal_of_Matrix A) )
assume that
A1: n >= 1 and
A2: A is V196(K) ; :: thesis: Det A = the multF of K $$ (diagonal_of_Matrix A)
set k1 = the multF of K $$ (diagonal_of_Matrix A);
set X = Permutations n;
set Y = the carrier of K;
reconsider p0 = idseq n as Permutation of (Seg n) ;
A3: len (diagonal_of_Matrix A) = n by MATRIX_3:def 10;
deffunc H1( object ) -> Element of the carrier of K = IFEQ ((idseq n),$1,( the multF of K $$ (diagonal_of_Matrix A)),(0. K));
A4: for x being object st x in Permutations n holds
H1(x) in the carrier of K ;
ex f2 being Function of (Permutations n), the carrier of K st
for x being object st x in Permutations n holds
f2 . x = H1(x) from FUNCT_2:sch 2(A4);
 then consider f2 being Function of (Permutations n), the carrier of K such that
A5: for x being object st x in Permutations n holds
f2 . x = H1(x) ;
A6: p0 is even by MATRIX_1:16;
A7: for x being object st x in dom (Path_product A) holds
(Path_product A) . x = f2 . x
proof
let x be object ; :: thesis: ( x in dom (Path_product A) implies (Path_product A) . x = f2 . x )
assume x in dom (Path_product A) ; :: thesis: (Path_product A) . x = f2 . x
for p being Element of Permutations n holds f2 . p = - (( the multF of K $$ (Path_matrix (p,A))),p)
proof
let p be Element of Permutations n; :: thesis: f2 . p = - (( the multF of K $$ (Path_matrix (p,A))),p)
A8: now :: thesis: - ((0. K),p) = 0. K
per cases ( p is even or p is odd ) ;
suppose p is even ; :: thesis: - ((0. K),p) = 0. K
hence - ((0. K),p) = 0. K by MATRIX_1:def 16; :: thesis: verum
end;
suppose p is odd ; :: thesis: - ((0. K),p) = 0. K
then - ((0. K),p) = - (0. K) by MATRIX_1:def 16
.= 0. K by RLVECT_1:12 ;
hence - ((0. K),p) = 0. K ; :: thesis: verum
end;
end;
end;
now :: thesis: ( ( p = idseq n & f2 . p = - (( the multF of K $$ (Path_matrix (p,A))),p) ) or ( p <> idseq n & f2 . p = - (( the multF of K $$ (Path_matrix (p,A))),p) ) )
per cases ( p = idseq n or p <> idseq n ) ;
case A9: p = idseq n ; :: thesis: f2 . p = - (( the multF of K $$ (Path_matrix (p,A))),p)
A10: for i, j being Nat st i in dom (diagonal_of_Matrix A) & j = p . i holds
(diagonal_of_Matrix A) . i = A * (i,j)
proof
let i, j be Nat; :: thesis: ( i in dom (diagonal_of_Matrix A) & j = p . i implies (diagonal_of_Matrix A) . i = A * (i,j) )
assume that
A11: i in dom (diagonal_of_Matrix A) and
A12: j = p . i ; :: thesis: (diagonal_of_Matrix A) . i = A * (i,j)
A13: i in Seg n by A3, A11, FINSEQ_1:def 3;
then p . i = i by A9, FUNCT_1:17;
hence (diagonal_of_Matrix A) . i = A * (i,j) by A12, A13, MATRIX_3:def 10; :: thesis: verum
end;
len (Permutations n) = n by MATRIX_1:9;
then A14: - (( the multF of K $$ (Path_matrix (p,A))),p) = the multF of K $$ (Path_matrix (p,A)) by A6, A9, MATRIX_1:def 16;
f2 . p = H1(p) by A5
.= the multF of K $$ (diagonal_of_Matrix A) by A9, FUNCOP_1:def 8 ;
hence f2 . p = - (( the multF of K $$ (Path_matrix (p,A))),p) by A3, A14, A10, MATRIX_3:def 7; :: thesis: verum
end;
case A15: p <> idseq n ; :: thesis: f2 . p = - (( the multF of K $$ (Path_matrix (p,A))),p)
reconsider Ab = NAT as non empty set ;
defpred S1[ Nat] means ( $1 < n implies ex p3 being FinSequence of K st
( len p3 = $1 + 1 & p3 . 1 = (Path_matrix (p,A)) . 1 & ( for n3 being Nat st 0 <> n3 & n3 < $1 + 1 & n3 < n holds
p3 . (n3 + 1) = the multF of K . ((p3 . n3),((Path_matrix (p,A)) . (n3 + 1))) ) ) );
A16: rng (Path_matrix (p,A)) c= the carrier of K by FINSEQ_1:def 4;
A17: len (Path_matrix (p,A)) = n by MATRIX_3:def 7;
then 1 in Seg (len (Path_matrix (p,A))) by A1;
then 1 in dom (Path_matrix (p,A)) by FINSEQ_1:def 3;
then (Path_matrix (p,A)) . 1 in rng (Path_matrix (p,A)) by FUNCT_1:def 3;
then reconsider d = (Path_matrix (p,A)) . 1 as Element of K by A16;
reconsider q3 = <*d*> as FinSequence of K ;
A18: for n3 being Nat st 0 <> n3 & n3 < 0 + 1 & n3 < n holds
q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,A)) . (n3 + 1))) by NAT_1:13;
A19: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A20: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: ( ( k + 1 < n & S1[k + 1] ) or ( k + 1 >= n & S1[k + 1] ) )
per cases ( k + 1 < n or k + 1 >= n ) ;
case A21: k + 1 < n ; :: thesis: S1[k + 1]
then consider p3 being FinSequence of K such that
A22: len p3 = k + 1 and
A23: p3 . 1 = (Path_matrix (p,A)) . 1 and
A24: for n3 being Nat st 0 <> n3 & n3 < k + 1 & n3 < n holds
p3 . (n3 + 1) = the multF of K . ((p3 . n3),((Path_matrix (p,A)) . (n3 + 1))) by A20, NAT_1:12;
defpred S2[ object , object ] means ( ( $1 in Seg (k + 1) implies $2 = p3 . $1 ) & ( not $1 in Seg (k + 1) implies $2 = 0. K ) );
A25: for x being object st x in NAT holds
ex y being object st
( y in the carrier of K & S2[x,y] )
proof
let x be object ; :: thesis: ( x in NAT implies ex y being object st
( y in the carrier of K & S2[x,y] ) )
assume x in NAT ; :: thesis: ex y being object st
( y in the carrier of K & S2[x,y] )
now :: thesis: ( ( x in Seg (k + 1) & ex y being object st
( y in the carrier of K & S2[x,y] ) ) or ( not x in Seg (k + 1) & ex y being object st
( y in the carrier of K & S2[x,y] ) ) )
per cases ( x in Seg (k + 1) or not x in Seg (k + 1) ) ;
case A26: x in Seg (k + 1) ; :: thesis: ex y being object st
( y in the carrier of K & S2[x,y] )
then reconsider nx = x as Nat ;
nx in dom p3 by A22, A26, FINSEQ_1:def 3;
then A27: p3 . nx in rng p3 by FUNCT_1:def 3;
rng p3 c= the carrier of K by FINSEQ_1:def 4;
then reconsider s = p3 . nx as Element of K by A27;
( x in Seg (k + 1) implies s = p3 . x ) ;
hence ex y being object st
( y in the carrier of K & S2[x,y] ) by A26; :: thesis: verum
end;
case not x in Seg (k + 1) ; :: thesis: ex y being object st
( y in the carrier of K & S2[x,y] )
hence ex y being object st
( y in the carrier of K & S2[x,y] ) ; :: thesis: verum
end;
end;
end;
hence ex y being object st
( y in the carrier of K & S2[x,y] ) ; :: thesis: verum
end;
ex f6 being sequence of the carrier of K st
for x being object st x in NAT holds
S2[x,f6 . x] from FUNCT_2:sch 1(A25);
then consider f6 being sequence of the carrier of K such that
A28: for x being object st x in NAT holds
S2[x,f6 . x] ;
( 1 <= (k + 1) + 1 & (k + 1) + 1 <= n ) by A21, NAT_1:12, NAT_1:13;
then (k + 1) + 1 in Seg (len (Path_matrix (p,A))) by A17;
then (k + 1) + 1 in dom (Path_matrix (p,A)) by FINSEQ_1:def 3;
then ( rng (Path_matrix (p,A)) c= the carrier of K & (Path_matrix (p,A)) . ((k + 1) + 1) in rng (Path_matrix (p,A)) ) by FINSEQ_1:def 4, FUNCT_1:def 3;
then [(f6 . (k + 1)),((Path_matrix (p,A)) . ((k + 1) + 1))] in [: the carrier of K, the carrier of K:] by ZFMISC_1:def 2;
then reconsider e = the multF of K . ((f6 . (k + 1)),((Path_matrix (p,A)) . ((k + 1) + 1))) as Element of K by FUNCT_2:5;
reconsider q3 = p3 ^ <*e*> as FinSequence of K ;
A29: len q3 = (len p3) + (len <*e*>) by FINSEQ_1:22
.= (k + 1) + 1 by A22, FINSEQ_1:40 ;
A30: for n3 being Nat st 0 <> n3 & n3 < (k + 1) + 1 & n3 < n holds
q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,A)) . (n3 + 1)))
proof
let n3 be Nat; :: thesis: ( 0 <> n3 & n3 < (k + 1) + 1 & n3 < n implies q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,A)) . (n3 + 1))) )
assume that
A31: 0 <> n3 and
A32: n3 < (k + 1) + 1 and
A33: n3 < n ; :: thesis: q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,A)) . (n3 + 1)))
now :: thesis: ( ( n3 < k + 1 & q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,A)) . (n3 + 1))) ) or ( n3 >= k + 1 & q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,A)) . (n3 + 1))) ) )
per cases ( n3 < k + 1 or n3 >= k + 1 ) ;
case A34: n3 < k + 1 ; :: thesis: q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,A)) . (n3 + 1)))
then ( 1 <= n3 + 1 & n3 + 1 <= k + 1 ) by NAT_1:12, NAT_1:13;
then n3 + 1 in Seg (len p3) by A22;
then n3 + 1 in dom p3 by FINSEQ_1:def 3;
then A35: p3 . (n3 + 1) = q3 . (n3 + 1) by FINSEQ_1:def 7;
0 + 1 <= n3 by A31, NAT_1:13;
then n3 in Seg (len p3) by A22, A34;
then A36: n3 in dom p3 by FINSEQ_1:def 3;
p3 . (n3 + 1) = the multF of K . ((p3 . n3),((Path_matrix (p,A)) . (n3 + 1))) by A24, A31, A33, A34;
hence q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,A)) . (n3 + 1))) by A35, A36, FINSEQ_1:def 7; :: thesis: verum
end;
case A37: n3 >= k + 1 ; :: thesis: q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,A)) . (n3 + 1)))
A38: n3 + 1 <= (k + 1) + 1 by A32, NAT_1:13;
A39: n3 + 1 > k + 1 by A37, NAT_1:13;
then n3 + 1 >= (k + 1) + 1 by NAT_1:13;
then A40: n3 + 1 = (k + 1) + 1 by A38, XXREAL_0:1;
1 <= k + 1 by NAT_1:12;
then A41: k + 1 in Seg (k + 1) ;
then k + 1 in dom p3 by A22, FINSEQ_1:def 3;
then A42: q3 . (k + 1) = p3 . (k + 1) by FINSEQ_1:def 7;
q3 . (n3 + 1) = <*e*> . ((n3 + 1) - (k + 1)) by A22, A29, A39, A38, FINSEQ_1:24
.= e by A40, FINSEQ_1:def 8 ;
hence q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,A)) . (n3 + 1))) by A28, A40, A41, A42; :: thesis: verum
end;
end;
end;
hence q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,A)) . (n3 + 1))) ; :: thesis: verum
end;
1 <= k + 1 by NAT_1:12;
then 1 in Seg (len p3) by A22;
then 1 in dom p3 by FINSEQ_1:def 3;
then q3 . 1 = (Path_matrix (p,A)) . 1 by A23, FINSEQ_1:def 7;
hence S1[k + 1] by A29, A30; :: thesis: verum
end;
case k + 1 >= n ; :: thesis: S1[k + 1]
hence S1[k + 1] ; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
A43: f2 . p = H1(p) by A5
.= 0. K by A15, FUNCOP_1:def 8 ;
n < n + 1 by NAT_1:13;
then A44: n - 1 < (n + 1) - 1 by XREAL_1:14;
A45: dom p = Seg (len (Permutations n)) by FUNCT_2:52;
then A46: dom p = Seg n by MATRIX_1:9;
then dom p = dom (idseq n) by RELAT_1:45;
then consider i0 being object such that
A47: i0 in dom p and
A48: p . i0 <> (idseq n) . i0 by A15, FUNCT_1:2;
A49: i0 in Seg n by A45, A47, MATRIX_1:9;
reconsider i0 = i0 as Nat by A45, A47;
A50: p . i0 <> i0 by A46, A47, A48, FUNCT_1:18;
p is Permutation of (Seg n) by MATRIX_1:def 12;
then A51: p . i0 in Seg n by A46, A47, FUNCT_2:5;
then reconsider j0 = p . i0 as Nat ;
A52: n - 1 = n -' 1 by A1, XREAL_1:233;
( len q3 = 1 & q3 . 1 = (Path_matrix (p,A)) . 1 ) by FINSEQ_1:40;
then A53: S1[ 0 ] by A18;
for k being Nat holds S1[k] from NAT_1:sch 2(A53, A19);
then consider p3 being FinSequence of K such that
A54: len p3 = (n -' 1) + 1 and
A55: p3 . 1 = (Path_matrix (p,A)) . 1 and
A56: for n3 being Nat st 0 <> n3 & n3 < (n -' 1) + 1 & n3 < n holds
p3 . (n3 + 1) = the multF of K . ((p3 . n3),((Path_matrix (p,A)) . (n3 + 1))) by A52, A44;
defpred S2[ set , set ] means ( ( $1 in Seg n implies $2 = p3 . $1 ) & ( not $1 in Seg n implies $2 = 0. K ) );
A57: for x3 being Element of Ab ex y3 being Element of K st S2[x3,y3]
proof
let x3 be Element of Ab; :: thesis: ex y3 being Element of K st S2[x3,y3]
now :: thesis: ( ( x3 in Seg n & ex y3 being Element of K st S2[x3,y3] ) or ( not x3 in Seg n & ex y3 being Element of K st S2[x3,y3] ) )
per cases ( x3 in Seg n or not x3 in Seg n ) ;
case A58: x3 in Seg n ; :: thesis: ex y3 being Element of K st S2[x3,y3]
then x3 in dom p3 by A52, A54, FINSEQ_1:def 3;
then ( rng p3 c= the carrier of K & p3 . x3 in rng p3 ) by FINSEQ_1:def 4, FUNCT_1:def 3;
hence ex y3 being Element of K st S2[x3,y3] by A58; :: thesis: verum
end;
case not x3 in Seg n ; :: thesis: ex y3 being Element of K st S2[x3,y3]
hence ex y3 being Element of K st S2[x3,y3] ; :: thesis: verum
end;
end;
end;
hence ex y3 being Element of K st S2[x3,y3] ; :: thesis: verum
end;
ex f4 being Function of Ab, the carrier of K st
for x2 being Element of Ab holds S2[x2,f4 . x2] from FUNCT_2:sch 3(A57);
then consider f4 being sequence of the carrier of K such that
A59: for x4 being Element of NAT holds
( ( x4 in Seg n implies f4 . x4 = p3 . x4 ) & ( not x4 in Seg n implies f4 . x4 = 0. K ) ) ;
A60: for n3 being Nat st 0 <> n3 & n3 < len (Path_matrix (p,A)) holds
f4 . (n3 + 1) = the multF of K . ((f4 . n3),((Path_matrix (p,A)) . (n3 + 1)))
proof
let n3 be Nat; :: thesis: ( 0 <> n3 & n3 < len (Path_matrix (p,A)) implies f4 . (n3 + 1) = the multF of K . ((f4 . n3),((Path_matrix (p,A)) . (n3 + 1))) )
assume that
A61: 0 <> n3 and
A62: n3 < len (Path_matrix (p,A)) ; :: thesis: f4 . (n3 + 1) = the multF of K . ((f4 . n3),((Path_matrix (p,A)) . (n3 + 1)))
A63: n3 + 1 <= len (Path_matrix (p,A)) by A62, NAT_1:13;
A64: 0 + 1 <= n3 by A61, NAT_1:13;
then A65: n3 in Seg n by A17, A62;
1 < n3 + 1 by A64, NAT_1:13;
then n3 + 1 in Seg n by A17, A63;
then A66: f4 . (n3 + 1) = p3 . (n3 + 1) by A59;
p3 . (n3 + 1) = the multF of K . ((p3 . n3),((Path_matrix (p,A)) . (n3 + 1))) by A17, A52, A56, A61, A62;
hence f4 . (n3 + 1) = the multF of K . ((f4 . n3),((Path_matrix (p,A)) . (n3 + 1))) by A59, A66, A65; :: thesis: verum
end;
A67: i0 <= n by A46, A47, FINSEQ_1:1;
then A68: n -' i0 = n - i0 by XREAL_1:233;
i0 in dom (Path_matrix (p,A)) by A49, A17, FINSEQ_1:def 3;
then A69: (Path_matrix (p,A)) . i0 = A * (i0,j0) by MATRIX_3:def 7;
defpred S3[ Nat] means f4 . (i0 + $1) = 0. K;
A70: 0 < i0 by A45, A47, FINSEQ_1:1;
A71: for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be Nat; :: thesis: ( S3[k] implies S3[k + 1] )
A72: 1 <= 1 + (i0 + k) by NAT_1:12;
assume A73: S3[k] ; :: thesis: S3[k + 1]
now :: thesis: ( ( (i0 + k) + 1 <= n & S3[k + 1] ) or ( (i0 + k) + 1 > n & S3[k + 1] ) )
per cases ( (i0 + k) + 1 <= n or (i0 + k) + 1 > n ) ;
case A74: (i0 + k) + 1 <= n ; :: thesis: S3[k + 1]
1 <= 1 + (i0 + k) by NAT_1:12;
then (i0 + k) + 1 in Seg (len (Path_matrix (p,A))) by A17, A74;
then (i0 + k) + 1 in dom (Path_matrix (p,A)) by FINSEQ_1:def 3;
then A75: (Path_matrix (p,A)) . ((i0 + k) + 1) in rng (Path_matrix (p,A)) by FUNCT_1:def 3;
rng (Path_matrix (p,A)) c= the carrier of K by FINSEQ_1:def 4;
then reconsider b = (Path_matrix (p,A)) . ((i0 + k) + 1) as Element of K by A75;
i0 <= i0 + k by NAT_1:12;
then A76: 0 < i0 + k by A45, A47, FINSEQ_1:1;
A77: i0 + k < n by A74, NAT_1:13;
0 + 1 <= i0 + k by A70, NAT_1:13;
then A78: i0 + k in Seg n by A77;
(i0 + k) + 1 in Seg n by A72, A74;
then f4 . ((i0 + k) + 1) = p3 . ((i0 + k) + 1) by A59
.= the multF of K . ((p3 . (i0 + k)),((Path_matrix (p,A)) . ((i0 + k) + 1))) by A52, A56, A77, A76
.= (0. K) * b by A59, A73, A78
.= 0. K ;
hence S3[k + 1] ; :: thesis: verum
end;
case (i0 + k) + 1 > n ; :: thesis: S3[k + 1]
then not i0 + (k + 1) in Seg n by FINSEQ_1:1;
hence S3[k + 1] by A59; :: thesis: verum
end;
end;
end;
hence S3[k + 1] ; :: thesis: verum
end;
1 in Seg n by A1;
then A79: f4 . 1 = (Path_matrix (p,A)) . 1 by A55, A59;
A80: 1 <= i0 by A45, A47, FINSEQ_1:1;
now :: thesis: ( ( i0 <= 1 & S3[ 0 ] ) or ( i0 > 1 & S3[ 0 ] ) )
per cases ( i0 <= 1 or i0 > 1 ) ;
case A81: i0 > 1 ; :: thesis: S3[ 0 ]
reconsider a = f4 . (i0 -' 1) as Element of K ;
i0 < i0 + 1 by NAT_1:13;
then i0 - 1 < (i0 + 1) - 1 by XREAL_1:14;
then A82: i0 - 1 < len (Path_matrix (p,A)) by A67, A17, XXREAL_0:2;
i0 -' 1 = i0 - 1 by A81, XREAL_1:233;
then A83: (i0 -' 1) + 1 = i0 ;
i0 - 1 > 1 - 1 by A81, XREAL_1:14;
then f4 . i0 = the multF of K . ((f4 . (i0 -' 1)),((Path_matrix (p,A)) . i0)) by A60, A82, A83
.= a * (0. K) by A2, A49, A50, A51, A69
.= 0. K ;
hence S3[ 0 ] ; :: thesis: verum
end;
end;
end;
then A84: S3[ 0 ] ;
for k being Nat holds S3[k] from NAT_1:sch 2(A84, A71);
then S3[n -' i0] ;
hence f2 . p = - (( the multF of K $$ (Path_matrix (p,A))),p) by A1, A8, A43, A17, A79, A60, A68, FINSOP_1:2; :: thesis: verum
end;
end;
end;
hence f2 . p = - (( the multF of K $$ (Path_matrix (p,A))),p) ; :: thesis: verum
end;
hence (Path_product A) . x = f2 . x by MATRIX_3:def 8; :: thesis: verum
end;
deffunc H2( set ) -> object = IFIN ((idseq n),$1,( the multF of K $$ (diagonal_of_Matrix A)),(0. K));
set F = the addF of K;
set f = Path_product A;
set B = In ((Permutations n),(Fin (Permutations n)));
A85: for x being set st x in Fin (Permutations n) holds
H2(x) in the carrier of K
proof
let x be set ; :: thesis: ( x in Fin (Permutations n) implies H2(x) in the carrier of K )
assume x in Fin (Permutations n) ; :: thesis: H2(x) in the carrier of K
per cases ( idseq n in x or not idseq n in x ) ;
suppose idseq n in x ; :: thesis: H2(x) in the carrier of K
then H2(x) = the multF of K $$ (diagonal_of_Matrix A) by Def1;
hence H2(x) in the carrier of K ; :: thesis: verum
end;
suppose not idseq n in x ; :: thesis: H2(x) in the carrier of K
then H2(x) = 0. K by Def1;
hence H2(x) in the carrier of K ; :: thesis: verum
end;
end;
end;
ex f2 being Function of (Fin (Permutations n)), the carrier of K st
for x being set st x in Fin (Permutations n) holds
f2 . x = H2(x) from FUNCT_2:sch 11(A85);
 then consider G0 being Function of (Fin (Permutations n)), the carrier of K such that
A86: for x being set st x in Fin (Permutations n) holds
G0 . x = H2(x) ;
dom f2 = Permutations n by FUNCT_2:def 1;
then A87: dom (Path_product A) = dom f2 by FUNCT_2:def 1;
then A88: Path_product A = f2 by A7, FUNCT_1:2;
A89: for B9 being Element of Fin (Permutations n) st B9 c= In ((Permutations n),(Fin (Permutations n))) & B9 <> {} holds
for x being Element of Permutations n st x in (In ((Permutations n),(Fin (Permutations n)))) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product A) . x))
proof
let B9 be Element of Fin (Permutations n); :: thesis: ( B9 c= In ((Permutations n),(Fin (Permutations n))) & B9 <> {} implies for x being Element of Permutations n st x in (In ((Permutations n),(Fin (Permutations n)))) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product A) . x)) )
assume that
B9 c= In ((Permutations n),(Fin (Permutations n))) and
B9 <> {} ; :: thesis: for x being Element of Permutations n st x in (In ((Permutations n),(Fin (Permutations n)))) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product A) . x))
thus for x being Element of Permutations n st x in (In ((Permutations n),(Fin (Permutations n)))) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product A) . x)) :: thesis: verum
proof
let x be Element of Permutations n; :: thesis: ( x in (In ((Permutations n),(Fin (Permutations n)))) \ B9 implies G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product A) . x)) )
assume A90: x in (In ((Permutations n),(Fin (Permutations n)))) \ B9 ; :: thesis: G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product A) . x))
A91: now :: thesis: ( not idseq n in B9 \/ {x} implies G0 . (B9 \/ {x}) = 0. K )
assume A92: not idseq n in B9 \/ {x} ; :: thesis: G0 . (B9 \/ {x}) = 0. K
thus G0 . (B9 \/ {x}) = IFIN ((idseq n),(B9 \/ {.x.}),( the multF of K $$ (diagonal_of_Matrix A)),(0. K)) by A86
.= 0. K by A92, Def1 ; :: thesis: verum
end;
A93: 0. K is_a_unity_wrt the addF of K by FVSUM_1:6;
A94: now :: thesis: ( not idseq n in B9 implies G0 . B9 = 0. K )
assume A95: not idseq n in B9 ; :: thesis: G0 . B9 = 0. K
thus G0 . B9 = IFIN ((idseq n),B9,( the multF of K $$ (diagonal_of_Matrix A)),(0. K)) by A86
.= 0. K by A95, Def1 ; :: thesis: verum
end;
A96: now :: thesis: ( not idseq n in B9 \/ {x} implies the addF of K . ((G0 . B9),((Path_product A) . x)) = 0. K )
assume A97: not idseq n in B9 \/ {x} ; :: thesis: the addF of K . ((G0 . B9),((Path_product A) . x)) = 0. K
then not idseq n in {x} by XBOOLE_0:def 3;
then A98: not idseq n = x by TARSKI:def 1;
(Path_product A) . x = H1(x) by A5, A88
.= 0. K by A98, FUNCOP_1:def 8 ;
hence the addF of K . ((G0 . B9),((Path_product A) . x)) = 0. K by A94, A93, A97, BINOP_1:3, XBOOLE_0:def 3; :: thesis: verum
end;
A99: now :: thesis: ( idseq n in B9 implies G0 . B9 = the multF of K $$ (diagonal_of_Matrix A) )
assume A100: idseq n in B9 ; :: thesis: G0 . B9 = the multF of K $$ (diagonal_of_Matrix A)
thus G0 . B9 = IFIN ((idseq n),B9,( the multF of K $$ (diagonal_of_Matrix A)),(0. K)) by A86
.= the multF of K $$ (diagonal_of_Matrix A) by A100, Def1 ; :: thesis: verum
end;
A101: now :: thesis: ( idseq n in B9 \/ {x} implies the addF of K . ((G0 . B9),((Path_product A) . x)) = the multF of K $$ (diagonal_of_Matrix A) )
assume idseq n in B9 \/ {x} ; :: thesis: the addF of K . ((G0 . B9),((Path_product A) . x)) = the multF of K $$ (diagonal_of_Matrix A)
then A102: ( idseq n in B9 or idseq n in {x} ) by XBOOLE_0:def 3;
now :: thesis: ( ( idseq n in B9 & the addF of K . ((G0 . B9),((Path_product A) . x)) = the multF of K $$ (diagonal_of_Matrix A) ) or ( idseq n = x & the addF of K . ((G0 . B9),((Path_product A) . x)) = the multF of K $$ (diagonal_of_Matrix A) ) )
per cases ( idseq n in B9 or idseq n = x ) by A102, TARSKI:def 1;
case A103: idseq n in B9 ; :: thesis: the addF of K . ((G0 . B9),((Path_product A) . x)) = the multF of K $$ (diagonal_of_Matrix A)
A104: not x in B9 by A90, XBOOLE_0:def 5;
(Path_product A) . x = H1(x) by A5, A88
.= 0. K by A103, A104, FUNCOP_1:def 8 ;
hence the addF of K . ((G0 . B9),((Path_product A) . x)) = the multF of K $$ (diagonal_of_Matrix A) by A99, A93, A103, BINOP_1:3; :: thesis: verum
end;
case A105: idseq n = x ; :: thesis: the addF of K . ((G0 . B9),((Path_product A) . x)) = the multF of K $$ (diagonal_of_Matrix A)
(Path_product A) . x = H1(x) by A5, A88
.= the multF of K $$ (diagonal_of_Matrix A) by A105, FUNCOP_1:def 8 ;
hence the addF of K . ((G0 . B9),((Path_product A) . x)) = the multF of K $$ (diagonal_of_Matrix A) by A90, A94, A93, A105, BINOP_1:3, XBOOLE_0:def 5; :: thesis: verum
end;
end;
end;
hence the addF of K . ((G0 . B9),((Path_product A) . x)) = the multF of K $$ (diagonal_of_Matrix A) ; :: thesis: verum
end;
now :: thesis: ( idseq n in B9 \/ {x} implies G0 . (B9 \/ {x}) = the multF of K $$ (diagonal_of_Matrix A) )
assume A106: idseq n in B9 \/ {x} ; :: thesis: G0 . (B9 \/ {x}) = the multF of K $$ (diagonal_of_Matrix A)
thus G0 . (B9 \/ {x}) = IFIN ((idseq n),(B9 \/ {.x.}),( the multF of K $$ (diagonal_of_Matrix A)),(0. K)) by A86
.= the multF of K $$ (diagonal_of_Matrix A) by A106, Def1 ; :: thesis: verum
end;
hence G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product A) . x)) by A91, A101, A96; :: thesis: verum
end;
end;
A107: for x being Element of Permutations n holds G0 . {x} = (Path_product A) . x
proof
let x be Element of Permutations n; :: thesis: G0 . {x} = (Path_product A) . x
now :: thesis: ( ( x = idseq n & G0 . {.x.} = f2 . x ) or ( x <> idseq n & G0 . {.x.} = f2 . x ) )
per cases ( x = idseq n or x <> idseq n ) ;
case A108: x = idseq n ; :: thesis: G0 . {.x.} = f2 . x
then idseq n in {x} by TARSKI:def 1;
then A109: IFIN ((idseq n),{x},( the multF of K $$ (diagonal_of_Matrix A)),(0. K)) = the multF of K $$ (diagonal_of_Matrix A) by Def1;
f2 . x = H1(x) by A5
.= the multF of K $$ (diagonal_of_Matrix A) by A108, FUNCOP_1:def 8 ;
hence G0 . {.x.} = f2 . x by A86, A109; :: thesis: verum
end;
case A110: x <> idseq n ; :: thesis: G0 . {.x.} = f2 . x
then not idseq n in {x} by TARSKI:def 1;
then A111: IFIN ((idseq n),{x},( the multF of K $$ (diagonal_of_Matrix A)),(0. K)) = 0. K by Def1;
f2 . x = H1(x) by A5
.= 0. K by A110, FUNCOP_1:def 8 ;
hence G0 . {.x.} = f2 . x by A86, A111; :: thesis: verum
end;
end;
end;
hence G0 . {x} = (Path_product A) . x by A87, A7, FUNCT_1:2; :: thesis: verum
end;
A112: for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
G0 . {} = e
proof
let e be Element of the carrier of K; :: thesis: ( e is_a_unity_wrt the addF of K implies G0 . {} = e )
assume e is_a_unity_wrt the addF of K ; :: thesis: G0 . {} = e
then A113: the addF of K . ((0. K),e) = 0. K by BINOP_1:3;
0. K is_a_unity_wrt the addF of K by FVSUM_1:6;
then A114: the addF of K . ((0. K),e) = e by BINOP_1:3;
IFIN ((idseq n),{},( the multF of K $$ (diagonal_of_Matrix A)),(0. K)) = 0. K by Def1;
hence G0 . {} = e by A86, A113, A114, FINSUB_1:7; :: thesis: verum
end;
A115: now :: thesis: ( idseq n in In ((Permutations n),(Fin (Permutations n))) implies G0 . (In ((Permutations n),(Fin (Permutations n)))) = the multF of K $$ (diagonal_of_Matrix A) )
assume A116: idseq n in In ((Permutations n),(Fin (Permutations n))) ; :: thesis: G0 . (In ((Permutations n),(Fin (Permutations n)))) = the multF of K $$ (diagonal_of_Matrix A)
thus G0 . (In ((Permutations n),(Fin (Permutations n)))) = IFIN ((idseq n),(In ((Permutations n),(Fin (Permutations n)))),( the multF of K $$ (diagonal_of_Matrix A)),(0. K)) by A86
.= the multF of K $$ (diagonal_of_Matrix A) by A116, Def1 ; :: thesis: verum
end;
S: idseq n is Element of (Group_of_Perm n) by MATRIX_1:11;
Permutations n in Fin (Permutations n) by FINSUB_1:def 5;
then ( In ((Permutations n),(Fin (Permutations n))) = Permutations n & idseq n in the carrier of (Group_of_Perm n) ) by S, SUBSET_1:def 8;
then the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product A)) = the multF of K $$ (diagonal_of_Matrix A) by A115, A112, A107, A89, MATRIX_1:def 13, SETWISEO:def 3;
hence Det A = the multF of K $$ (diagonal_of_Matrix A) by MATRIX_3:def 9; :: thesis: verum