let a, b, c, d be Real; :: thesis: for u, v being non zero Element of (TOP-REAL 3) st u = |[a,b,1]| & v = |[c,d,0]| holds
Dir u <> Dir v
let u, v be non zero Element of (TOP-REAL 3); :: thesis: ( u = |[a,b,1]| & v = |[c,d,0]| implies Dir u <> Dir v )
assume that
A1: u = |[a,b,1]| and
A2: v = |[c,d,0]| ; :: thesis: Dir u <> Dir v
assume Dir u = Dir v ; :: thesis: contradiction
then are_Prop u,v by ANPROJ_1:22;
then consider x being Real such that
x <> 0 and
A3: u = x * v by ANPROJ_1:1;
1 = (x * v) `3 by A3, A1, EUCLID_5:2
.= |[(x * (v `1)),(x * (v `2)),(x * (v `3))]| `3 by EUCLID_5:7
.= x * (v `3) by EUCLID_5:2
.= x * 0 by A2, EUCLID_5:2
.= 0 ;
hence contradiction ; :: thesis: verum