let n be Nat; :: thesis: for K being Field
for M being Upper_Triangular_Matrix of n,K holds Det M = the multF of K $$ (diagonal_of_Matrix M)
let K be Field; :: thesis: for M being Upper_Triangular_Matrix of n,K holds Det M = the multF of K $$ (diagonal_of_Matrix M)
let M be Upper_Triangular_Matrix of n,K; :: thesis: Det M = the multF of K $$ (diagonal_of_Matrix M)
set aa = the addF of K;
set mm = the multF of K;
set P = Permutations n;
set F = FinOmega (Permutations n);
set PP = Path_product M;
idseq n is Element of (Group_of_Perm n) by MATRIX_2:23;
then reconsider I = idseq n as Element of Permutations n by MATRIX_2:def 13;
len (Permutations n) = n by MATRIX_2:20;
then A1: I is even by MATRIX_2:29;
Permutations n is finite by MATRIX_2:30;
then reconsider II = {I}, PI = (Permutations n) \ {I} as Element of Fin (Permutations n) by FINSUB_1:def 5;
A2: FinOmega (Permutations n) = Permutations n by MATRIX_2:30, MATRIX_2:def 17;

now

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

suppose PI = {} ; :: thesis: the addF of K $$ (FinOmega (Permutations n)),(Path_product M) = the addF of K $$ II,(Path_product M)

then Permutations n c= II by XBOOLE_1:37;
hence the addF of K $$ (FinOmega (Permutations n)),(Path_product M) = the addF of K $$ II,(Path_product M) by A2, XBOOLE_0:def 10; :: thesis: verum

end;

suppose A3: PI <> {} ; :: thesis: the addF of K $$ (FinOmega (Permutations n)),(Path_product M) = the addF of K $$ II,(Path_product M)

A4: (Path_product M) .: PI c= {(0. K)}

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (Path_product M) .: PI or y in {(0. K)} )
assume y in (Path_product M) .: PI ; :: thesis: y in {(0. K)}
then consider x being set such that
A5: x in dom (Path_product M) and
A6: x in PI and
A7: y = (Path_product M) . x by FUNCT_1:def 12;
reconsider f = x as Element of Permutations n by A5;
not f in {I} by A6, XBOOLE_0:def 5;
then f <> I by TARSKI:def 1;
then (Path_product M) . f = 0. K by Th5;
hence y in {(0. K)} by A7, TARSKI:def 1; :: thesis: verum

end;

A8: 0. K = the_unity_wrt the addF of K by FVSUM_1:9;
dom (Path_product M) = Permutations n by FUNCT_2:def 1;
then (Path_product M) .: PI = {(0. K)} by A3, A4, ZFMISC_1:39;
then A9: the addF of K $$ PI,(Path_product M) = 0. K by A8, FVSUM_1:10, SETWOP_2:10;
A10: PI \/ II = II \/ (Permutations n) by XBOOLE_1:39;
A11: II \/ (Permutations n) = Permutations n by XBOOLE_1:12;
PI misses II by XBOOLE_1:79;
hence the addF of K $$ (FinOmega (Permutations n)),(Path_product M) = (the addF of K $$ II,(Path_product M)) + (0. K) by A2, A3, A9, A10, A11, SETWOP_2:6
.= the addF of K $$ II,(Path_product M) by RLVECT_1:def 7 ;
:: thesis: verum

end;

end;

end;

hence Det M = (Path_product M) . I by SETWISEO:26
.= - (the multF of K "**" (Path_matrix I,M)),I by MATRIX_3:def 8
.= the multF of K "**" (Path_matrix I,M) by A1, MATRIX_2:def 16
.= the multF of K "**" (diagonal_of_Matrix M) by Th6 ;
:: thesis: verum