let a, a' be Scalar of TernaryFieldEx ; :: thesis: ( a <> a' implies for b, b' being Scalar of TernaryFieldEx ex u, v being Scalar of TernaryFieldEx st
( Tern u,a,v = b & Tern u,a',v = b' ) )
assume A1: a <> a' ; :: thesis: for b, b' being Scalar of TernaryFieldEx ex u, v being Scalar of TernaryFieldEx st
( Tern u,a,v = b & Tern u,a',v = b' )
let b, b' be Scalar of TernaryFieldEx ; :: thesis: ex u, v being Scalar of TernaryFieldEx st
( Tern u,a,v = b & Tern u,a',v = b' )
reconsider x = a, x' = a', y = b, y' = b' as Real ;
set s = (y' - y) / (x' - x);
set t = y - (x * ((y' - y) / (x' - x)));
reconsider u = (y' - y) / (x' - x), v = y - (x * ((y' - y) / (x' - x))) as Scalar of TernaryFieldEx ;
take u ; :: thesis: ex v being Scalar of TernaryFieldEx st
( Tern u,a,v = b & Tern u,a',v = b' )
take v ; :: thesis: ( Tern u,a,v = b & Tern u,a',v = b' )
thus Tern u,a,v = (((y' - y) / (x' - x)) * x) + ((- (((y' - y) / (x' - x)) * x)) + y) by Def4
.= b ; :: thesis: Tern u,a',v = b'
A2: x' - x <> 0 by A1;
thus Tern u,a',v = (((y' - y) / (x' - x)) * x') + ((- (x * ((y' - y) / (x' - x)))) + y) by Def4
.= (((y' - y) / (x' - x)) * (x' - x)) + y
.= (y' - y) + y by A2, XCMPLX_1:88
.= b' ; :: thesis: verum