let u, v, w be non zero Element of (TOP-REAL 3); :: thesis: ( |{u,v,w}| = 0 implies ex p being non zero Element of (TOP-REAL 3) st
( |(p,u)| = 0 & |(p,v)| = 0 & |(p,w)| = 0 ) )
assume A1: |{u,v,w}| = 0 ; :: thesis: ex p being non zero Element of (TOP-REAL 3) st
( |(p,u)| = 0 & |(p,v)| = 0 & |(p,w)| = 0 )
reconsider p = |[(u `1),(v `1),(w `1)]|, q = |[(u `2),(v `2),(w `2)]|, r = |[(u `3),(v `3),(w `3)]| as Element of (TOP-REAL 3) ;
A2: ( p `1 = u `1 & p `2 = v `1 & p `3 = w `1 & q `1 = u `2 & q `2 = v `2 & q `3 = w `2 & r `1 = u `3 & r `2 = v `3 & r `3 = w `3 ) by EUCLID_5:2;
A3: |{p,q,r}| = (((((((p `1) * (q `2)) * (r `3)) - (((p `3) * (q `2)) * (r `1))) - (((p `1) * (q `3)) * (r `2))) + (((p `2) * (q `3)) * (r `1))) - (((p `2) * (q `1)) * (r `3))) + (((p `3) * (q `1)) * (r `2)) by ANPROJ_8:27;
|{u,v,w}| = (((((((u `1) * (v `2)) * (w `3)) - (((u `3) * (v `2)) * (w `1))) - (((u `1) * (v `3)) * (w `2))) + (((u `2) * (v `3)) * (w `1))) - (((u `2) * (v `1)) * (w `3))) + (((u `3) * (v `1)) * (w `2)) by ANPROJ_8:27;
then consider a, b, c being Real such that
A4: ((a * p) + (b * q)) + (c * r) = 0. (TOP-REAL 3) and
A5: ( a <> 0 or b <> 0 or c <> 0 ) by A1, A2, A3, ANPROJ_8:42;
A6: |[0,0,0]| = (|[(a * (p `1)),(a * (p `2)),(a * (p `3))]| + (b * q)) + (c * r) by A4, EUCLID_5:4, EUCLID_5:7
.= (|[(a * (p `1)),(a * (p `2)),(a * (p `3))]| + |[(b * (q `1)),(b * (q `2)),(b * (q `3))]|) + (c * r) by EUCLID_5:7
.= (|[(a * (p `1)),(a * (p `2)),(a * (p `3))]| + |[(b * (q `1)),(b * (q `2)),(b * (q `3))]|) + |[(c * (r `1)),(c * (r `2)),(c * (r `3))]| by EUCLID_5:7
.= |[((a * (p `1)) + (b * (q `1))),((a * (p `2)) + (b * (q `2))),((a * (p `3)) + (b * (q `3)))]| + |[(c * (r `1)),(c * (r `2)),(c * (r `3))]| by EUCLID_5:6
.= |[(((a * (p `1)) + (b * (q `1))) + (c * (r `1))),(((a * (p `2)) + (b * (q `2))) + (c * (r `2))),(((a * (p `3)) + (b * (q `3))) + (c * (r `3)))]| by EUCLID_5:6 ;
reconsider p = |[a,b,c]| as non zero Element of (TOP-REAL 3) by A5;
take p ; :: thesis: ( |(p,u)| = 0 & |(p,v)| = 0 & |(p,w)| = 0 )
thus |(p,u)| = (((p `1) * (u `1)) + ((p `2) * (u `2))) + ((p `3) * (u `3)) by EUCLID_5:29
.= ((a * (u `1)) + ((p `2) * (u `2))) + ((p `3) * (u `3)) by EUCLID_5:2
.= ((a * (u `1)) + (b * (u `2))) + ((p `3) * (u `3)) by EUCLID_5:2
.= ((a * (u `1)) + (b * (u `2))) + (c * (u `3)) by EUCLID_5:2
.= 0 by A6, A2, FINSEQ_1:78 ; :: thesis: ( |(p,v)| = 0 & |(p,w)| = 0 )
thus |(p,v)| = (((p `1) * (v `1)) + ((p `2) * (v `2))) + ((p `3) * (v `3)) by EUCLID_5:29
.= ((a * (v `1)) + ((p `2) * (v `2))) + ((p `3) * (v `3)) by EUCLID_5:2
.= ((a * (v `1)) + (b * (v `2))) + ((p `3) * (v `3)) by EUCLID_5:2
.= ((a * (v `1)) + (b * (v `2))) + (c * (v `3)) by EUCLID_5:2
.= 0 by A6, A2, FINSEQ_1:78 ; :: thesis: |(p,w)| = 0
thus |(p,w)| = (((p `1) * (w `1)) + ((p `2) * (w `2))) + ((p `3) * (w `3)) by EUCLID_5:29
.= ((a * (w `1)) + ((p `2) * (w `2))) + ((p `3) * (w `3)) by EUCLID_5:2
.= ((a * (w `1)) + (b * (w `2))) + ((p `3) * (w `3)) by EUCLID_5:2
.= ((a * (w `1)) + (b * (w `2))) + (c * (w `3)) by EUCLID_5:2
.= 0 by A6, A2, FINSEQ_1:78 ; :: thesis: verum