let K be Field; :: thesis: for a, b, c, d being Element of K holds Det ((a,b) ][ (c,d)) = (a * d) - (b * c)
let a, b, c, d be Element of K; :: thesis: Det ((a,b) ][ (c,d)) = (a * d) - (b * c)
reconsider rid2 = Rev () as Element of Permutations 2 by Th4;
set M = (a,b) ][ (c,d);
reconsider id2 = idseq 2 as Permutation of (Seg 2) ;
reconsider Id2 = idseq 2 as Element of Permutations 2 by MATRIX_1:def 12;
set F = the addF of K;
set f = Path_product ((a,b) ][ (c,d));
A1: ( rid2 = <*2,1*> & len () = 2 ) by ;
A2: (Path_product ((a,b) ][ (c,d))) . rid2 = - (( the multF of K \$\$ (Path_matrix (rid2,((a,b) ][ (c,d))))),rid2) by MATRIX_3:def 8
.= - ( the multF of K \$\$ (Path_matrix (rid2,((a,b) ][ (c,d))))) by
.= - ( the multF of K \$\$ <*b,c*>) by Th10
.= - (b * c) by Th11 ;
len () = 2 by MATRIX_1:9;
then A3: Id2 is even by MATRIX_1:16;
1 in Seg 2 ;
then A4: id2 <> rid2 by ;
A5: (Path_product ((a,b) ][ (c,d))) . id2 = - (( the multF of K \$\$ (Path_matrix (Id2,((a,b) ][ (c,d))))),Id2) by MATRIX_3:def 8
.= the multF of K \$\$ (Path_matrix (Id2,((a,b) ][ (c,d)))) by
.= the multF of K \$\$ <*a,d*> by Th9
.= a * d by Th11 ;
Permutations 2 in Fin () by FINSUB_1:def 5;
then In ((),(Fin ())) = Permutations 2 by SUBSET_1:def 8;
then Det ((a,b) ][ (c,d)) = the addF of K \$\$ ({.Id2,rid2.},(Path_product ((a,b) ][ (c,d)))) by
.= (a * d) - (b * c) by ;
hence Det ((a,b) ][ (c,d)) = (a * d) - (b * c) ; :: thesis: verum