let e1, e2, e3, f1, f2, f3 be Element of F_Real; for r1, r2 being Real
for p1, p2, p3, p4, p5, p6, p7, p8, p9 being Point of (TOP-REAL 3) st p1 = <*1,0,0*> & p2 = <*0,1,0*> & p3 = <*0,0,1*> & p4 = <*1,1,1*> & p5 = <*e1,e2,e3*> & p6 = <*f1,f2,f3*> & |{p1,p2,p5}| <> 0 & |{p1,p3,p6}| <> 0 & |{p2,p4,p6}| <> 0 & |{p3,p4,p5}| <> 0 & |{p1,p2,p6}| <> 0 & |{p1,p3,p5}| <> 0 & |{p2,p4,p5}| <> 0 & |{p3,p4,p6}| <> 0 & |{p1,p5,p7}| <> 0 & |{p2,p5,p9}| <> 0 & |{p5,p9,p7}| <> 0 & |{p3,p6,p8}| <> 0 & |{p2,p6,p8}| <> 0 & |{p2,p9,p7}| <> 0 & |{p2,p4,p7}| <> 0 & |{p2,p8,p7}| <> 0 & |{p3,p5,p8}| <> 0 & |{p5,p8,p7}| <> 0 & ( r1 <> 0 or r2 <> 0 ) & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p5) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p6) = 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 holds
|{p2,p8,p7}| * |{p5,p9,p7}| = |{p2,p9,p7}| * |{p5,p8,p7}|
let r1, r2 be Real; for p1, p2, p3, p4, p5, p6, p7, p8, p9 being Point of (TOP-REAL 3) st p1 = <*1,0,0*> & p2 = <*0,1,0*> & p3 = <*0,0,1*> & p4 = <*1,1,1*> & p5 = <*e1,e2,e3*> & p6 = <*f1,f2,f3*> & |{p1,p2,p5}| <> 0 & |{p1,p3,p6}| <> 0 & |{p2,p4,p6}| <> 0 & |{p3,p4,p5}| <> 0 & |{p1,p2,p6}| <> 0 & |{p1,p3,p5}| <> 0 & |{p2,p4,p5}| <> 0 & |{p3,p4,p6}| <> 0 & |{p1,p5,p7}| <> 0 & |{p2,p5,p9}| <> 0 & |{p5,p9,p7}| <> 0 & |{p3,p6,p8}| <> 0 & |{p2,p6,p8}| <> 0 & |{p2,p9,p7}| <> 0 & |{p2,p4,p7}| <> 0 & |{p2,p8,p7}| <> 0 & |{p3,p5,p8}| <> 0 & |{p5,p8,p7}| <> 0 & ( r1 <> 0 or r2 <> 0 ) & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p5) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p6) = 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 holds
|{p2,p8,p7}| * |{p5,p9,p7}| = |{p2,p9,p7}| * |{p5,p8,p7}|
let p1, p2, p3, p4, p5, p6, p7, p8, p9 be Point of (TOP-REAL 3); ( p1 = <*1,0,0*> & p2 = <*0,1,0*> & p3 = <*0,0,1*> & p4 = <*1,1,1*> & p5 = <*e1,e2,e3*> & p6 = <*f1,f2,f3*> & |{p1,p2,p5}| <> 0 & |{p1,p3,p6}| <> 0 & |{p2,p4,p6}| <> 0 & |{p3,p4,p5}| <> 0 & |{p1,p2,p6}| <> 0 & |{p1,p3,p5}| <> 0 & |{p2,p4,p5}| <> 0 & |{p3,p4,p6}| <> 0 & |{p1,p5,p7}| <> 0 & |{p2,p5,p9}| <> 0 & |{p5,p9,p7}| <> 0 & |{p3,p6,p8}| <> 0 & |{p2,p6,p8}| <> 0 & |{p2,p9,p7}| <> 0 & |{p2,p4,p7}| <> 0 & |{p2,p8,p7}| <> 0 & |{p3,p5,p8}| <> 0 & |{p5,p8,p7}| <> 0 & ( r1 <> 0 or r2 <> 0 ) & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p5) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p6) = 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 implies |{p2,p8,p7}| * |{p5,p9,p7}| = |{p2,p9,p7}| * |{p5,p8,p7}| )
assume that
A1:
p1 = <*1,0,0*>
and
A2:
p2 = <*0,1,0*>
and
A3:
p3 = <*0,0,1*>
and
A4:
p4 = <*1,1,1*>
and
A5:
p5 = <*e1,e2,e3*>
and
A6:
p6 = <*f1,f2,f3*>
and
A7:
|{p1,p2,p5}| <> 0
and
A8:
|{p1,p3,p6}| <> 0
and
A9:
|{p2,p4,p6}| <> 0
and
A10:
|{p3,p4,p5}| <> 0
and
A11:
|{p1,p2,p6}| <> 0
and
A12:
|{p1,p3,p5}| <> 0
and
A13:
|{p2,p4,p5}| <> 0
and
A14:
|{p3,p4,p6}| <> 0
and
A15:
|{p1,p5,p7}| <> 0
and
A16:
|{p2,p5,p9}| <> 0
and
A17:
|{p5,p9,p7}| <> 0
and
A18:
|{p3,p6,p8}| <> 0
and
A19:
|{p2,p6,p8}| <> 0
and
A20:
|{p2,p9,p7}| <> 0
and
A21:
|{p2,p4,p7}| <> 0
and
A22:
|{p2,p8,p7}| <> 0
and
A23:
|{p3,p5,p8}| <> 0
and
A24:
|{p5,p8,p7}| <> 0
and
A25:
( r1 <> 0 or r2 <> 0 )
and
A26:
qfconic (0,0,0,r1,r2,(- (r1 + r2)),p5) = 0
and
A27:
qfconic (0,0,0,r1,r2,(- (r1 + r2)),p6) = 0
and
A28:
|{p1,p5,p9}| = 0
and
A29:
|{p1,p6,p8}| = 0
and
A30:
|{p2,p4,p9}| = 0
and
A31:
|{p2,p6,p7}| = 0
and
A32:
|{p3,p4,p8}| = 0
and
A33:
|{p3,p5,p7}| = 0
; |{p2,p8,p7}| * |{p5,p9,p7}| = |{p2,p9,p7}| * |{p5,p8,p7}|
reconsider r125 = |{p1,p2,p5}|, r136 = |{p1,p3,p6}|, r246 = |{p2,p4,p6}|, r345 = |{p3,p4,p5}|, r126 = |{p1,p2,p6}|, r135 = |{p1,p3,p5}|, r245 = |{p2,p4,p5}|, r346 = |{p3,p4,p6}|, r157 = |{p1,p5,p7}|, r259 = |{p2,p5,p9}|, r597 = |{p5,p9,p7}|, r368 = |{p3,p6,p8}|, r268 = |{p2,p6,p8}|, r297 = |{p2,p9,p7}|, r247 = |{p2,p4,p7}|, r287 = |{p2,p8,p7}|, r358 = |{p3,p5,p8}|, r587 = |{p5,p8,p7}| as non zero Real by A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, A22, A23, A24;
( p1 = <*(p1 `1),(p1 `2),(p1 `3)*> & p2 = <*(p2 `1),(p2 `2),(p2 `3)*> & p3 = <*(p3 `1),(p3 `2),(p3 `3)*> & p4 = <*(p4 `1),(p4 `2),(p4 `3)*> & p5 = <*(p5 `1),(p5 `2),(p5 `3)*> & p6 = <*(p6 `1),(p6 `2),(p6 `3)*> )
by EUCLID_5:3;
then reconsider MABE = <*p1,p2,p5*>, MACF = <*p1,p3,p6*>, MBDF = <*p2,p4,p6*>, MCDE = <*p3,p4,p5*>, MABF = <*p1,p2,p6*>, MACE = <*p1,p3,p5*>, MBDE = <*p2,p4,p5*>, MCDF = <*p3,p4,p6*> as Matrix of 3,F_Real by ANPROJ_8:19;
( p1 = <*1,0,0*> & p2 = <*0,1,0*> & p3 = <*0,0,1*> & p4 = <*1,1,1*> & p5 = <*e1,e2,e3*> & p6 = <*f1,f2,f3*> & MABE = <*p1,p2,p5*> & MACF = <*p1,p3,p6*> & MBDF = <*p2,p4,p6*> & MCDE = <*p3,p4,p5*> & MABF = <*p1,p2,p6*> & MACE = <*p1,p3,p5*> & MBDE = <*p2,p4,p5*> & MCDF = <*p3,p4,p6*> )
by A1, A2, A3, A4, A5, A6;
then A34:
( Det MABE = |{p1,p2,p5}| & Det MACF = |{p1,p3,p6}| & Det MBDF = |{p2,p4,p6}| & Det MCDE = |{p3,p4,p5}| & Det MABF = |{p1,p2,p6}| & Det MACE = |{p1,p3,p5}| & Det MBDE = |{p2,p4,p5}| & Det MCDF = |{p3,p4,p6}| )
by Th20;
now ( ((r125 * r136) * r246) * r345 = ((r126 * r135) * r245) * r346 & r157 * r259 = - (r125 * r597) & r126 * r368 = r136 * r268 & r245 * r297 = - (r247 * r259) & r247 * r268 = - (r246 * r287) & r346 * r358 = r345 * r368 & r135 * r587 = - (r157 * r358) )
(
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 )
by A1, A2, A3, A4, A5, A6, A25, A26, A27, Th28;
then
(((Det MABE) * (Det MACF)) * (Det MBDF)) * (Det MCDE) = (((Det MABF) * (Det MACE)) * (Det MBDE)) * (Det MCDF)
by Th19;
hence
((r125 * r136) * r246) * r345 = ((r126 * r135) * r245) * r346
by A34;
( r157 * r259 = - (r125 * r597) & r126 * r368 = r136 * r268 & r245 * r297 = - (r247 * r259) & r247 * r268 = - (r246 * r287) & r346 * r358 = r345 * r368 & r135 * r587 = - (r157 * r358) )thus
(
r157 * r259 = - (r125 * r597) &
r126 * r368 = r136 * r268 &
r245 * r297 = - (r247 * r259) &
r247 * r268 = - (r246 * r287) &
r346 * r358 = r345 * r368 &
r135 * r587 = - (r157 * r358) )
by A28, A29, A30, A31, A32, A33, Th21, Th22, Th23, Th24, Th25, Th26;
verum
hence
|{p2,p8,p7}| * |{p5,p9,p7}| = |{p2,p9,p7}| * |{p5,p8,p7}|
by Th27; verum