let e1, e2, e3, f1, f2, f3 be Element of F_Real; :: thesis: for MABF, MACE, MBDE, MCDF being Matrix of 3,F_Real st MABF = <*<*1,0,0*>,<*0,1,0*>,<*f1,f2,f3*>*> & MACE = <*<*1,0,0*>,<*0,0,1*>,<*e1,e2,e3*>*> & MBDE = <*<*0,1,0*>,<*1,1,1*>,<*e1,e2,e3*>*> & MCDF = <*<*0,0,1*>,<*1,1,1*>,<*f1,f2,f3*>*> holds
(((Det MABF) * (Det MACE)) * (Det MBDE)) * (Det MCDF) = ((f3 * e2) * (e1 - e3)) * (f1 - f2)
let MABF, MACE, MBDE, MCDF be Matrix of 3,F_Real; :: thesis: ( MABF = <*<*1,0,0*>,<*0,1,0*>,<*f1,f2,f3*>*> & MACE = <*<*1,0,0*>,<*0,0,1*>,<*e1,e2,e3*>*> & MBDE = <*<*0,1,0*>,<*1,1,1*>,<*e1,e2,e3*>*> & MCDF = <*<*0,0,1*>,<*1,1,1*>,<*f1,f2,f3*>*> implies (((Det MABF) * (Det MACE)) * (Det MBDE)) * (Det MCDF) = ((f3 * e2) * (e1 - e3)) * (f1 - f2) )
assume that
A1: MABF = <*<*1,0,0*>,<*0,1,0*>,<*f1,f2,f3*>*> and
A2: MACE = <*<*1,0,0*>,<*0,0,1*>,<*e1,e2,e3*>*> and
A3: MBDE = <*<*0,1,0*>,<*1,1,1*>,<*e1,e2,e3*>*> and
A4: MCDF = <*<*0,0,1*>,<*1,1,1*>,<*f1,f2,f3*>*> ; :: thesis: (((Det MABF) * (Det MACE)) * (Det MBDE)) * (Det MCDF) = ((f3 * e2) * (e1 - e3)) * (f1 - f2)
( Det MABF = f3 & Det MACE = - e2 & Det MBDE = e1 - e3 & Det MCDF = f2 - f1 ) by A1, A2, A3, A4, Lm26, Lm27, Lm28, Lm29;
hence (((Det MABF) * (Det MACE)) * (Det MBDE)) * (Det MCDF) = ((f3 * e2) * (e1 - e3)) * (f1 - f2) ; :: thesis: verum