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

Per M = ((((((a * e) * i) + ((c * e) * g)) + ((a * f) * h)) + ((b * f) * g)) + ((b * d) * i)) + ((c * d) * h)

reconsider rid3 = Rev (idseq 3) as Element of Permutations 3 by Th4;

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

Per 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 Per 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: Per M = ((((((a * e) * i) + ((c * e) * g)) + ((a * f) * h)) + ((b * f) * g)) + ((b * d) * i)) + ((c * d) * h)

reconsider a3 = <*1,3,2*>, a4 = <*2,3,1*>, a5 = <*2,1,3*>, a6 = <*3,1,2*> as Element of Permutations 3 by Th27;

reconsider id3 = idseq 3 as Permutation of (Seg 3) ;

reconsider Id3 = idseq 3 as Element of Permutations 3 by MATRIX_1:def 12;

reconsider B1 = {.Id3,rid3,a3.}, B2 = {.a4,a5,a6.} as Element of Fin (Permutations 3) ;

set r = PPath_product M;

A2: (PPath_product M) . id3 = the multF of K $$ (Path_matrix (Id3,M)) by Def1

.= the multF of K $$ <*a,e,i*> by A1, Th20, FINSEQ_2:53

.= (a * e) * i by Th26 ;

A3: (PPath_product M) . a6 = the multF of K $$ (Path_matrix (a6,M)) by Def1

.= the multF of K $$ <*c,d,h*> by A1, Th25

.= (c * d) * h by Th26 ;

A4: (PPath_product M) . a5 = the multF of K $$ (Path_matrix (a5,M)) by Def1

.= the multF of K $$ <*b,d,i*> by A1, Th24

.= (b * d) * i by Th26 ;

A5: (PPath_product M) . a4 = the multF of K $$ (Path_matrix (a4,M)) by Def1

.= the multF of K $$ <*b,f,g*> by A1, Th23

.= (b * f) * g by Th26 ;

for x being object st x in B1 \ B2 holds

x in B1 by XBOOLE_0:def 5;

then B1 \ B2 c= B1 by TARSKI:def 3;

then B1 \ B2 = B1 by A7, XBOOLE_0:def 10;

then A8: B1 misses B2 by XBOOLE_1:83;

set F = the addF of K;

id3 in Permutations 3 by MATRIX_1:def 12;

then reconsider r1 = (PPath_product M) . id3, r2 = (PPath_product M) . rid3, r3 = (PPath_product M) . a3, r4 = (PPath_product M) . a4, r5 = (PPath_product M) . a5, r6 = (PPath_product M) . a6 as Element of K by FUNCT_2:5;

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

then In ((Permutations 3),(Fin (Permutations 3))) = Permutations 3 by SUBSET_1:def 8;

then reconsider X = {Id3,rid3,a3,a4,a5,a6} as Element of Fin (Permutations 3) by Th15, Th19, FINSEQ_2:53;

A9: ( the addF of K $$ (B1,(PPath_product M)) = (r1 + r2) + r3 & the addF of K $$ (B2,(PPath_product M)) = (r4 + r5) + r6 ) by Lm3, Lm4, Lm10, Lm11, Th15, FINSEQ_2:53, SETWOP_2:3;

A10: (PPath_product M) . rid3 = the multF of K $$ (Path_matrix (rid3,M)) by Def1

.= the multF of K $$ <*c,e,g*> by A1, Th15, Th21

.= (c * e) * g by Th26 ;

A11: (PPath_product M) . a3 = the multF of K $$ (Path_matrix (a3,M)) by Def1

.= the multF of K $$ <*a,f,h*> by A1, Th22

.= (a * f) * h by Th26 ;

( In ((Permutations 3),(Fin (Permutations 3))) = X & X = {Id3,rid3,a3} \/ {a4,a5,a6} ) by Th15, Th19, ENUMSET1:13, FINSEQ_2:53;

then Per M = the addF of K . (( the addF of K $$ (B1,(PPath_product M))),( the addF of K $$ (B2,(PPath_product M)))) by A8, SETWOP_2:4

.= ((r1 + r2) + r3) + (r4 + (r5 + r6)) by A9, RLVECT_1:def 3

.= (((r1 + r2) + r3) + r4) + (r5 + r6) by RLVECT_1:def 3

.= ((((((a * e) * i) + ((c * e) * g)) + ((a * f) * h)) + ((b * f) * g)) + ((b * d) * i)) + ((c * d) * h) by A2, A10, A11, A5, A4, A3, RLVECT_1:def 3 ;

hence Per M = ((((((a * e) * i) + ((c * e) * g)) + ((a * f) * h)) + ((b * f) * g)) + ((b * d) * i)) + ((c * d) * h) ; :: thesis: verum

for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds

Per M = ((((((a * e) * i) + ((c * e) * g)) + ((a * f) * h)) + ((b * f) * g)) + ((b * d) * i)) + ((c * d) * h)

reconsider rid3 = Rev (idseq 3) as Element of Permutations 3 by Th4;

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

Per 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 Per 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: Per M = ((((((a * e) * i) + ((c * e) * g)) + ((a * f) * h)) + ((b * f) * g)) + ((b * d) * i)) + ((c * d) * h)

reconsider a3 = <*1,3,2*>, a4 = <*2,3,1*>, a5 = <*2,1,3*>, a6 = <*3,1,2*> as Element of Permutations 3 by Th27;

reconsider id3 = idseq 3 as Permutation of (Seg 3) ;

reconsider Id3 = idseq 3 as Element of Permutations 3 by MATRIX_1:def 12;

reconsider B1 = {.Id3,rid3,a3.}, B2 = {.a4,a5,a6.} as Element of Fin (Permutations 3) ;

set r = PPath_product M;

A2: (PPath_product M) . id3 = the multF of K $$ (Path_matrix (Id3,M)) by Def1

.= the multF of K $$ <*a,e,i*> by A1, Th20, FINSEQ_2:53

.= (a * e) * i by Th26 ;

A3: (PPath_product M) . a6 = the multF of K $$ (Path_matrix (a6,M)) by Def1

.= the multF of K $$ <*c,d,h*> by A1, Th25

.= (c * d) * h by Th26 ;

A4: (PPath_product M) . a5 = the multF of K $$ (Path_matrix (a5,M)) by Def1

.= the multF of K $$ <*b,d,i*> by A1, Th24

.= (b * d) * i by Th26 ;

A5: (PPath_product M) . a4 = the multF of K $$ (Path_matrix (a4,M)) by Def1

.= the multF of K $$ <*b,f,g*> by A1, Th23

.= (b * f) * g by Th26 ;

now :: thesis: for x being object st x in B1 holds

x in B1 \ B2

then A7:
B1 c= B1 \ B2
by TARSKI:def 3;x in B1 \ B2

let x be object ; :: thesis: ( x in B1 implies x in B1 \ B2 )

assume A6: x in B1 ; :: thesis: x in B1 \ B2

then ( x = Id3 or x = rid3 or x = a3 ) by ENUMSET1:def 1;

then not x in B2 by Lm5, Lm6, Lm7, Lm8, Lm9, Th15, ENUMSET1:def 1, FINSEQ_2:53;

hence x in B1 \ B2 by A6, XBOOLE_0:def 5; :: thesis: verum

end;assume A6: x in B1 ; :: thesis: x in B1 \ B2

then ( x = Id3 or x = rid3 or x = a3 ) by ENUMSET1:def 1;

then not x in B2 by Lm5, Lm6, Lm7, Lm8, Lm9, Th15, ENUMSET1:def 1, FINSEQ_2:53;

hence x in B1 \ B2 by A6, XBOOLE_0:def 5; :: thesis: verum

for x being object st x in B1 \ B2 holds

x in B1 by XBOOLE_0:def 5;

then B1 \ B2 c= B1 by TARSKI:def 3;

then B1 \ B2 = B1 by A7, XBOOLE_0:def 10;

then A8: B1 misses B2 by XBOOLE_1:83;

set F = the addF of K;

id3 in Permutations 3 by MATRIX_1:def 12;

then reconsider r1 = (PPath_product M) . id3, r2 = (PPath_product M) . rid3, r3 = (PPath_product M) . a3, r4 = (PPath_product M) . a4, r5 = (PPath_product M) . a5, r6 = (PPath_product M) . a6 as Element of K by FUNCT_2:5;

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

then In ((Permutations 3),(Fin (Permutations 3))) = Permutations 3 by SUBSET_1:def 8;

then reconsider X = {Id3,rid3,a3,a4,a5,a6} as Element of Fin (Permutations 3) by Th15, Th19, FINSEQ_2:53;

A9: ( the addF of K $$ (B1,(PPath_product M)) = (r1 + r2) + r3 & the addF of K $$ (B2,(PPath_product M)) = (r4 + r5) + r6 ) by Lm3, Lm4, Lm10, Lm11, Th15, FINSEQ_2:53, SETWOP_2:3;

A10: (PPath_product M) . rid3 = the multF of K $$ (Path_matrix (rid3,M)) by Def1

.= the multF of K $$ <*c,e,g*> by A1, Th15, Th21

.= (c * e) * g by Th26 ;

A11: (PPath_product M) . a3 = the multF of K $$ (Path_matrix (a3,M)) by Def1

.= the multF of K $$ <*a,f,h*> by A1, Th22

.= (a * f) * h by Th26 ;

( In ((Permutations 3),(Fin (Permutations 3))) = X & X = {Id3,rid3,a3} \/ {a4,a5,a6} ) by Th15, Th19, ENUMSET1:13, FINSEQ_2:53;

then Per M = the addF of K . (( the addF of K $$ (B1,(PPath_product M))),( the addF of K $$ (B2,(PPath_product M)))) by A8, SETWOP_2:4

.= ((r1 + r2) + r3) + (r4 + (r5 + r6)) by A9, RLVECT_1:def 3

.= (((r1 + r2) + r3) + r4) + (r5 + r6) by RLVECT_1:def 3

.= ((((((a * e) * i) + ((c * e) * g)) + ((a * f) * h)) + ((b * f) * g)) + ((b * d) * i)) + ((c * d) * h) by A2, A10, A11, A5, A4, A3, RLVECT_1:def 3 ;

hence Per M = ((((((a * e) * i) + ((c * e) * g)) + ((a * f) * h)) + ((b * f) * g)) + ((b * d) * i)) + ((c * d) * h) ; :: thesis: verum