let a, b, c, d, e, f be Real; :: thesis: for u1, u2 being non zero Element of (TOP-REAL 3) st Dir u1 = Dir u2 & qfconic (a,b,c,d,e,f,u1) is negative holds
qfconic (a,b,c,d,e,f,u2) is negative
let u1, u2 be non zero Element of (TOP-REAL 3); :: thesis: ( Dir u1 = Dir u2 & qfconic (a,b,c,d,e,f,u1) is negative implies qfconic (a,b,c,d,e,f,u2) is negative )
assume that
A1: Dir u1 = Dir u2 and
A2: qfconic (a,b,c,d,e,f,u1) is negative ; :: thesis: qfconic (a,b,c,d,e,f,u2) is negative
are_Prop u2,u1 by A1, ANPROJ_1:22;
then consider g being Real such that
A3: g <> 0 and
A4: u2 = g * u1 by ANPROJ_1:1;
A5: ( u2 . 1 = g * (u1 . 1) & u2 . 2 = g * (u1 . 2) & u2 . 3 = g * (u1 . 3) ) by A4, RVSUM_1:44;
0 < g ^2 by A3, SQUARE_1:12;
then reconsider g2 = g * g as positive Real ;
qfconic (a,b,c,d,e,f,u2) = ((((((a * (u2 . 1)) * (u2 . 1)) + ((b * (u2 . 2)) * (u2 . 2))) + ((c * (u2 . 3)) * (u2 . 3))) + ((d * (u2 . 1)) * (u2 . 2))) + ((e * (u2 . 1)) * (u2 . 3))) + ((f * (u2 . 2)) * (u2 . 3)) by PASCAL:def 1
.= g2 * (((((((a * (u1 . 1)) * (u1 . 1)) + ((b * (u1 . 2)) * (u1 . 2))) + ((c * (u1 . 3)) * (u1 . 3))) + ((d * (u1 . 1)) * (u1 . 2))) + ((e * (u1 . 1)) * (u1 . 3))) + ((f * (u1 . 2)) * (u1 . 3))) by A5
.= g2 * (qfconic (a,b,c,d,e,f,u1)) by PASCAL:def 1 ;
hence qfconic (a,b,c,d,e,f,u2) is negative by A2; :: thesis: verum