let K be Field; 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; 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_2:def 9;
reconsider id2 = Id2 as Permutation of (Seg 2) ;
set f = PPath_product ((a,b) ][ (c,d));
1 in Seg 2
;
then A1:
( FinOmega (Permutations 2) = Permutations 2 & id2 <> rid2 )
by Th2, FUNCT_1:18, MATRIX_2:26, MATRIX_2:def 14;
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; verum