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 = In ((Permutations n),(Fin (Permutations n)));
set PP = Path_product M;
idseq n is Element of (Group_of_Perm n) by MATRIX_1:11;
then reconsider I = idseq n as Element of Permutations n by MATRIX_1:def 13;
len (Permutations n) = n by MATRIX_1:9;
then A1: I is even by MATRIX_1:16;
reconsider II = {I}, PI = (Permutations n) \ {I} as Element of Fin (Permutations n) by FINSUB_1:def 5;
Permutations n in Fin (Permutations n) by FINSUB_1:def 5;
then A2: In ((Permutations n),(Fin (Permutations n))) = Permutations n by SUBSET_1:def 8;

now :: thesis: the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product M)) = the addF of K $$ (II,(Path_product M))

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

suppose PI = {} ; :: thesis: the addF of K $$ ((In ((Permutations n),(Fin (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 $$ ((In ((Permutations n),(Fin (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 $$ ((In ((Permutations n),(Fin (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 object ; :: 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 object 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 6;
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:7;
dom (Path_product M) = Permutations n by FUNCT_2:def 1;
then (Path_product M) .: PI = {(0. K)} by A3, A4, ZFMISC_1:33;
then A9: the addF of K $$ (PI,(Path_product M)) = 0. K by A8, FVSUM_1:8, SETWOP_2:8;
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 $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product M)) = ( the addF of K $$ (II,(Path_product M))) + (0. K) by A2, A3, A9, A10, A11, SETWOP_2:4
.= the addF of K $$ (II,(Path_product M)) by RLVECT_1:def 4 ;
:: thesis: verum

end;

end;

end;

hence Det M = (Path_product M) . I by SETWISEO:17
.= - (( 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_1:def 16
.= the multF of K "**" (diagonal_of_Matrix M) by Th6 ;
:: thesis: verum