let a, a9 be Scalar of TernaryFieldEx; :: thesis: ( a <> a9 implies for b, b9 being Scalar of TernaryFieldEx ex u, v being Scalar of TernaryFieldEx st
( Tern (u,a,v) = b & Tern (u,a9,v) = b9 ) )
assume A1: a <> a9 ; :: thesis: for b, b9 being Scalar of TernaryFieldEx ex u, v being Scalar of TernaryFieldEx st
( Tern (u,a,v) = b & Tern (u,a9,v) = b9 )
let b, b9 be Scalar of TernaryFieldEx; :: thesis: ex u, v being Scalar of TernaryFieldEx st
( Tern (u,a,v) = b & Tern (u,a9,v) = b9 )
reconsider x = a, x9 = a9, y = b, y9 = b9 as Real ;
A2: x9 - x <> 0 by A1;
set s = (y9 - y) / (x9 - x);
set t = y - (x * ((y9 - y) / (x9 - x)));
reconsider u = (y9 - y) / (x9 - x), v = y - (x * ((y9 - y) / (x9 - x))) as Scalar of TernaryFieldEx by XREAL_0:def 1;
take u ; :: thesis: ex v being Scalar of TernaryFieldEx st
( Tern (u,a,v) = b & Tern (u,a9,v) = b9 )
take v ; :: thesis: ( Tern (u,a,v) = b & Tern (u,a9,v) = b9 )
thus Tern (u,a,v) = (((y9 - y) / (x9 - x)) * x) + ((- (((y9 - y) / (x9 - x)) * x)) + y) by Def2
.= b ; :: thesis: Tern (u,a9,v) = b9
thus Tern (u,a9,v) = (((y9 - y) / (x9 - x)) * x9) + ((- (x * ((y9 - y) / (x9 - x)))) + y) by Def2
.= (((y9 - y) / (x9 - x)) * (x9 - x)) + y
.= (y9 - y) + y by A2, XCMPLX_1:87
.= b9 ; :: thesis: verum