let a, b, c, d, e, f be Real; 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); ( 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
; 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; verum