let K be Field; :: thesis: for a, b, c, d being Element of K holds Per ((a,b) ][ (c,d)) = (a * d) + (b * c)

let a, b, c, d be Element of K; :: thesis: Per ((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 Element of Permutations 2 by MATRIX_1:def 12;

reconsider id2 = Id2 as Permutation of (Seg 2) ;

set f = PPath_product ((a,b) ][ (c,d));

A0: 1 in Seg 2 ;

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

then A1: ( In ((Permutations 2),(Fin (Permutations 2))) = Permutations 2 & id2 <> rid2 ) by A0, Th2, FUNCT_1:18, SUBSET_1:def 8;

A2: (PPath_product ((a,b) ][ (c,d))) . rid2 = the multF of K $$ (Path_matrix (rid2,((a,b) ][ (c,d)))) by Def1

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

.= b * c by Th11 ;

(PPath_product ((a,b) ][ (c,d))) . id2 = the multF of K $$ (Path_matrix (Id2,((a,b) ][ (c,d)))) by Def1

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

.= a * d by Th11 ;

hence Per ((a,b) ][ (c,d)) = (a * d) + (b * c) by A2, A1, Th6, SETWOP_2:1; :: thesis: verum

let a, b, c, d be Element of K; :: thesis: Per ((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 Element of Permutations 2 by MATRIX_1:def 12;

reconsider id2 = Id2 as Permutation of (Seg 2) ;

set f = PPath_product ((a,b) ][ (c,d));

A0: 1 in Seg 2 ;

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

then A1: ( In ((Permutations 2),(Fin (Permutations 2))) = Permutations 2 & id2 <> rid2 ) by A0, Th2, FUNCT_1:18, SUBSET_1:def 8;

A2: (PPath_product ((a,b) ][ (c,d))) . rid2 = the multF of K $$ (Path_matrix (rid2,((a,b) ][ (c,d)))) by Def1

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

.= b * c by Th11 ;

(PPath_product ((a,b) ][ (c,d))) . id2 = the multF of K $$ (Path_matrix (Id2,((a,b) ][ (c,d)))) by Def1

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

.= a * d by Th11 ;

hence Per ((a,b) ][ (c,d)) = (a * d) + (b * c) by A2, A1, Th6, SETWOP_2:1; :: thesis: verum