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)
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_2:def 11;
reconsider rid2 = Rev (idseq 2) as Element of Permutations 2 by Th4;
set F = the addF of K;
set f = Path_product (a,b ][ c,d);
len (Permutations 2) = 2 by MATRIX_2:20;
then A1: Id2 is even by MATRIX_2:29;
A2: (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 A1, MATRIX_2:def 16
.= the multF of K $$ <*a,d*> by Th9
.= a * d by Th11 ;
A3: 1 in Seg 2 ;
A4: rid2 = <*2,1*> by FINSEQ_2:61, FINSEQ_5:64;
A5: id2 <> rid2 by A3, Th2, FUNCT_1:35;
A6: len (Permutations 2) = 2 by MATRIX_2:20;
A7: (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 A4, A6, Th12, MATRIX_2:def 16
.= - (the multF of K $$ <*b,c*>) by Th10
.= - (b * c) by Th11 ;
FinOmega (Permutations 2) = Permutations 2 by MATRIX_2:30, MATRIX_2:def 17;
then Det (a,b ][ c,d) = the addF of K $$ {.Id2,rid2.},(Path_product (a,b ][ c,d)) by Th6, MATRIX_3:def 9
.= (a * d) - (b * c) by A2, A5, A7, SETWOP_2:3 ;
hence Det (a,b ][ c,d) = (a * d) - (b * c) ; :: thesis: verum