let e1, e2, e3, f1, f2, f3 be Element of F_Real; for MABE, MACF, MBDF, MCDE being Matrix of 3,F_Real st MABE = <*<*1,0,0*>,<*0,1,0*>,<*e1,e2,e3*>*> & MACF = <*<*1,0,0*>,<*0,0,1*>,<*f1,f2,f3*>*> & MBDF = <*<*0,1,0*>,<*1,1,1*>,<*f1,f2,f3*>*> & MCDE = <*<*0,0,1*>,<*1,1,1*>,<*e1,e2,e3*>*> holds
(((Det MABE) * (Det MACF)) * (Det MBDF)) * (Det MCDE) = ((e3 * f2) * (f1 - f3)) * (e1 - e2)
let MABE, MACF, MBDF, MCDE be Matrix of 3,F_Real; ( MABE = <*<*1,0,0*>,<*0,1,0*>,<*e1,e2,e3*>*> & MACF = <*<*1,0,0*>,<*0,0,1*>,<*f1,f2,f3*>*> & MBDF = <*<*0,1,0*>,<*1,1,1*>,<*f1,f2,f3*>*> & MCDE = <*<*0,0,1*>,<*1,1,1*>,<*e1,e2,e3*>*> implies (((Det MABE) * (Det MACF)) * (Det MBDF)) * (Det MCDE) = ((e3 * f2) * (f1 - f3)) * (e1 - e2) )
assume that
A1:
MABE = <*<*1,0,0*>,<*0,1,0*>,<*e1,e2,e3*>*>
and
A2:
MACF = <*<*1,0,0*>,<*0,0,1*>,<*f1,f2,f3*>*>
and
A3:
MBDF = <*<*0,1,0*>,<*1,1,1*>,<*f1,f2,f3*>*>
and
A4:
MCDE = <*<*0,0,1*>,<*1,1,1*>,<*e1,e2,e3*>*>
; (((Det MABE) * (Det MACF)) * (Det MBDF)) * (Det MCDE) = ((e3 * f2) * (f1 - f3)) * (e1 - e2)
( Det MABE = e3 & Det MACF = - f2 & Det MBDF = f1 - f3 & Det MCDE = e2 - e1 )
by A1, A2, A3, A4, Lm21, Lm23, Lm24, Lm25;
hence
(((Det MABE) * (Det MACF)) * (Det MBDF)) * (Det MCDE) = ((e3 * f2) * (f1 - f3)) * (e1 - e2)
; verum