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 (idseq 2) 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 (Permutations 2) = 2 ) by FINSEQ_2:52, FINSEQ_5:61, MATRIX_1:9;

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 A1, Th12, MATRIX_1:def 16

.= - ( the multF of K $$ <*b,c*>) by Th10

.= - (b * c) by Th11 ;

len (Permutations 2) = 2 by MATRIX_1:9;

then A3: Id2 is even by MATRIX_1:16;

1 in Seg 2 ;

then A4: id2 <> rid2 by Th2, FUNCT_1:18;

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 A3, MATRIX_1:def 16

.= the multF of K $$ <*a,d*> by Th9

.= a * d by Th11 ;

Permutations 2 in Fin (Permutations 2) by FINSUB_1:def 5;

then In ((Permutations 2),(Fin (Permutations 2))) = 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 Th6, MATRIX_3:def 9

.= (a * d) - (b * c) by A5, A4, A2, SETWOP_2:1 ;

hence Det ((a,b) ][ (c,d)) = (a * d) - (b * c) ; :: thesis: verum

let a, b, c, d be Element of K; :: thesis: Det ((a,b) ][ (c,d)) = (a * d) - (b * c)

reconsider rid2 = Rev (idseq 2) 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 (Permutations 2) = 2 ) by FINSEQ_2:52, FINSEQ_5:61, MATRIX_1:9;

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 A1, Th12, MATRIX_1:def 16

.= - ( the multF of K $$ <*b,c*>) by Th10

.= - (b * c) by Th11 ;

len (Permutations 2) = 2 by MATRIX_1:9;

then A3: Id2 is even by MATRIX_1:16;

1 in Seg 2 ;

then A4: id2 <> rid2 by Th2, FUNCT_1:18;

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 A3, MATRIX_1:def 16

.= the multF of K $$ <*a,d*> by Th9

.= a * d by Th11 ;

Permutations 2 in Fin (Permutations 2) by FINSUB_1:def 5;

then In ((Permutations 2),(Fin (Permutations 2))) = 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 Th6, MATRIX_3:def 9

.= (a * d) - (b * c) by A5, A4, A2, SETWOP_2:1 ;

hence Det ((a,b) ][ (c,d)) = (a * d) - (b * c) ; :: thesis: verum