let e1, e2, e3, f1, f2, f3 be Element of F_Real; :: thesis: for MABF, MABE, MACF, MBDF, MCDE, MACE, MBDE, MCDF being Matrix of 3,F_Real
for r1, r2 being 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*>*> & 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*>*> & ( r1 <> 0 or r2 <> 0 ) & ((r1 * e1) * e2) + ((r2 * e1) * e3) = ((r1 + r2) * e2) * e3 & ((r1 * f1) * f2) + ((r2 * f1) * f3) = ((r1 + r2) * f2) * f3 holds
(((Det MABE) * (Det MACF)) * (Det MBDF)) * (Det MCDE) = (((Det MABF) * (Det MACE)) * (Det MBDE)) * (Det MCDF)
let MABF, MABE, MACF, MBDF, MCDE, MACE, MBDE, MCDF be Matrix of 3,F_Real; :: thesis: for r1, r2 being 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*>*> & 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*>*> & ( r1 <> 0 or r2 <> 0 ) & ((r1 * e1) * e2) + ((r2 * e1) * e3) = ((r1 + r2) * e2) * e3 & ((r1 * f1) * f2) + ((r2 * f1) * f3) = ((r1 + r2) * f2) * f3 holds
(((Det MABE) * (Det MACF)) * (Det MBDF)) * (Det MCDE) = (((Det MABF) * (Det MACE)) * (Det MBDE)) * (Det MCDF)
let r1, r2 be Real; :: thesis: ( 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*>*> & 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*>*> & ( r1 <> 0 or r2 <> 0 ) & ((r1 * e1) * e2) + ((r2 * e1) * e3) = ((r1 + r2) * e2) * e3 & ((r1 * f1) * f2) + ((r2 * f1) * f3) = ((r1 + r2) * f2) * f3 implies (((Det MABE) * (Det MACF)) * (Det MBDF)) * (Det MCDE) = (((Det MABF) * (Det MACE)) * (Det MBDE)) * (Det MCDF) )
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*>*> and
A5: MABF = <*<*1,0,0*>,<*0,1,0*>,<*f1,f2,f3*>*> and
A6: MACE = <*<*1,0,0*>,<*0,0,1*>,<*e1,e2,e3*>*> and
A7: MBDE = <*<*0,1,0*>,<*1,1,1*>,<*e1,e2,e3*>*> and
A8: MCDF = <*<*0,0,1*>,<*1,1,1*>,<*f1,f2,f3*>*> and
A9: ( r1 <> 0 or r2 <> 0 ) and
A10: ((r1 * e1) * e2) + ((r2 * e1) * e3) = ((r1 + r2) * e2) * e3 and
A11: ((r1 * f1) * f2) + ((r2 * f1) * f3) = ((r1 + r2) * f2) * f3 ; :: thesis: (((Det MABE) * (Det MACF)) * (Det MBDF)) * (Det MCDE) = (((Det MABF) * (Det MACE)) * (Det MBDE)) * (Det MCDF)
reconsider d = e1, e = e2, f = e3, g = f1, h = f2, i = f3 as Real ;
A12: (((Det MABE) * (Det MACF)) * (Det MBDF)) * (Det MCDE) = ((e3 * f2) * (f1 - f3)) * (e1 - e2) by A1, A2, A3, A4, Lm30;
((e3 * f2) * (f1 - f3)) * (e1 - e2) = ((f3 * e2) * (e1 - e3)) * (f1 - f2) by A9, A10, A11, Lm22;
hence (((Det MABE) * (Det MACF)) * (Det MBDF)) * (Det MCDE) = (((Det MABF) * (Det MACE)) * (Det MBDE)) * (Det MCDF) by A12, A5, A6, A7, A8, Lm31; :: thesis: verum