let a, b, c be Real; :: thesis: for p, q, r being Point of (TOP-REAL 3) st ((a * p) + (b * q)) + (c * r) = 0. (TOP-REAL 3) & ( a <> 0 or b <> 0 or c <> 0 ) holds
|{p,q,r}| = 0
let p, q, r be Point of (TOP-REAL 3); :: thesis: ( ((a * p) + (b * q)) + (c * r) = 0. (TOP-REAL 3) & ( a <> 0 or b <> 0 or c <> 0 ) implies |{p,q,r}| = 0 )
assume ( ((a * p) + (b * q)) + (c * r) = 0. (TOP-REAL 3) & ( a <> 0 or b <> 0 or c <> 0 ) ) ; :: thesis: |{p,q,r}| = 0
then consider a, b, c being Real such that
A1: ((a * p) + (b * q)) + (c * r) = 0. (TOP-REAL 3) and
A2: ( a <> 0 or b <> 0 or c <> 0 ) ;
per cases ( a <> 0 or b <> 0 or c <> 0 ) by A2;
suppose a <> 0 ; :: thesis: |{p,q,r}| = 0
hence |{p,q,r}| = 0 by A1, Th12; :: thesis: verum
end;
suppose b <> 0 ; :: thesis: |{p,q,r}| = 0
then A3: |{q,p,r}| = 0 by A1, Th12;
|{p,q,r}| = - |{q,p,r}| by Th25;
hence |{p,q,r}| = 0 by A3; :: thesis: verum
end;
suppose A4: c <> 0 ; :: thesis: |{p,q,r}| = 0
((c * r) + (a * p)) + (b * q) = 0. (TOP-REAL 3) by A1, RLVECT_1:def 3;
then |{r,p,q}| = 0 by A4, Th12;
hence |{p,q,r}| = 0 by EUCLID_5:33; :: thesis: verum
end;
end;