let K be Field; :: thesis: for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h)
let a, b, c, d, e, f, g, h, i be Element of K; :: thesis: for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h)
let M be Matrix of 3,K; :: thesis: ( M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h) )
assume A1: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> ; :: thesis: Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h)
reconsider id3 = idseq 3 as Permutation of (Seg 3) ;
reconsider Id3 = idseq 3 as Element of Permutations 3 by MATRIX_2:def 11;
reconsider rid3 = Rev (idseq 3) as Element of Permutations 3 by Th4;
reconsider a3 = <*1,3,2*>, a4 = <*2,3,1*>, a5 = <*2,1,3*>, a6 = <*3,1,2*> as Element of Permutations 3 by Th27;
set F = the addF of K;
set r = Path_product M;
A2: id3 is even by MATRIX_2:29;
A3: 3 = len (Permutations 3) by MATRIX_2:20;
then A4: Id3 is even by MATRIX_2:29;
A5: (Path_product M) . id3 = - (the multF of K $$ (Path_matrix Id3,M)),Id3 by MATRIX_3:def 8
.= the multF of K $$ (Path_matrix Id3,M) by A2, A3, MATRIX_2:def 16
.= the multF of K $$ <*a,e,i*> by A1, Th20, FINSEQ_2:62
.= (a * e) * i by Th26 ;
A6: (Path_product M) . rid3 = - (the multF of K $$ (Path_matrix rid3,M)),rid3 by MATRIX_3:def 8
.= - (the multF of K $$ (Path_matrix rid3,M)) by A3, Th15, Th42, MATRIX_2:def 16
.= - (the multF of K $$ <*c,e,g*>) by A1, Th15, Th21
.= - ((c * e) * g) by Th26 ;
A7: (Path_product M) . a3 = - (the multF of K $$ (Path_matrix a3,M)),a3 by MATRIX_3:def 8
.= - (the multF of K $$ (Path_matrix a3,M)) by A3, Th44, MATRIX_2:def 16
.= - (the multF of K $$ <*a,f,h*>) by A1, Th22
.= - ((a * f) * h) by Th26 ;
A8: (Path_product M) . a4 = - (the multF of K $$ (Path_matrix a4,M)),a4 by MATRIX_3:def 8
.= the multF of K $$ (Path_matrix a4,M) by A3, Lm6, MATRIX_2:def 16
.= the multF of K $$ <*b,f,g*> by A1, Th23
.= (b * f) * g by Th26 ;
A9: (Path_product M) . a5 = - (the multF of K $$ (Path_matrix a5,M)),a5 by MATRIX_3:def 8
.= - (the multF of K $$ (Path_matrix a5,M)) by A3, Th43, MATRIX_2:def 16
.= - (the multF of K $$ <*b,d,i*>) by A1, Th24
.= - ((b * d) * i) by Th26 ;
A10: (Path_product M) . a6 = - (the multF of K $$ (Path_matrix a6,M)),a6 by MATRIX_3:def 8
.= the multF of K $$ (Path_matrix a6,M) by A3, Lm7, MATRIX_2:def 16
.= the multF of K $$ <*c,d,h*> by A1, Th25
.= (c * d) * h by Th26 ;
A11: FinOmega (Permutations 3) = Permutations 3 by MATRIX_2:30, MATRIX_2:def 17;
reconsider r1 = (Path_product M) . id3, r2 = (Path_product M) . rid3, r3 = (Path_product M) . a3, r4 = (Path_product M) . a4, r5 = (Path_product M) . a5, r6 = (Path_product M) . a6 as Element of K by A4, FUNCT_2:7;
reconsider X = {Id3,rid3,a3,a4,a5,a6} as Element of Fin (Permutations 3) by A11, Th15, Th19, FINSEQ_2:62;
A12: FinOmega (Permutations 3) = X by Th15, Th19, FINSEQ_2:62, MATRIX_2:def 17;
A13: X = {Id3,rid3,a3} \/ {a4,a5,a6} by ENUMSET1:53;
reconsider B1 = {.Id3,rid3,a3.}, B2 = {.a4,a5,a6.} as Element of Fin (Permutations 3) ;
A14: ( B1 <> {} & B2 <> {} & B1 misses B2 )

proof

B1 \ B2 = B1

proof

for x being set st x in B1 \ B2 holds
x in B1 by XBOOLE_0:def 5;
then A15: B1 \ B2 c= B1 by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in B1 implies x in B1 \ B2 )
assume x in B1 ; :: thesis: x in B1 \ B2
then ( x = Id3 or x = rid3 or x = a3 ) by ENUMSET1:def 1;
then ( x in B1 & not x in B2 ) by Lm4, Th15, ENUMSET1:def 1, FINSEQ_2:62;
hence x in B1 \ B2 by XBOOLE_0:def 5; :: thesis: verum

end;

then B1 c= B1 \ B2 by TARSKI:def 3;
hence B1 \ B2 = B1 by A15, XBOOLE_0:def 10; :: thesis: verum

end;

hence ( B1 <> {} & B2 <> {} & B1 misses B2 ) by XBOOLE_1:83; :: thesis: verum

end;

A16: the addF of K $$ B1,(Path_product M) = (r1 + r2) + r3 by Lm4, Th15, FINSEQ_2:62, SETWOP_2:5;
A17: the addF of K $$ B2,(Path_product M) = (r4 + r5) + r6 by Lm4, SETWOP_2:5;
Det M = the addF of K $$ (FinOmega (Permutations 3)),(Path_product M) by MATRIX_3:def 9
.= the addF of K . (the addF of K $$ B1,(Path_product M)),(the addF of K $$ B2,(Path_product M)) by A12, A13, A14, SETWOP_2:6
.= ((r1 + r2) + r3) + (r4 + (r5 + r6)) by A16, A17, RLVECT_1:def 6
.= (((r1 + r2) + r3) + r4) + (r5 + r6) by RLVECT_1:def 6
.= ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h) by A5, A6, A7, A8, A9, A10, RLVECT_1:def 6 ;
hence Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h) ; :: thesis: verum