Metamath Proof Explorer

Theorem hiidge0

Description: Inner product with self is not negative. (Contributed by NM, 29-May-1999) (New usage is discouraged.)

Ref Expression
Assertion hiidge0 
|- ( A e. ~H -> 0 <_ ( A .ih A ) )

Proof

Step Hyp Ref Expression
1 pm2.1 
 |-  ( -. A = 0h \/ A = 0h )
2 df-ne 
 |-  ( A =/= 0h <-> -. A = 0h )
3 ax-his4 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( A .ih A ) )
4 2 3 sylan2br 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> 0 < ( A .ih A ) )
5 4 ex 
 |-  ( A e. ~H -> ( -. A = 0h -> 0 < ( A .ih A ) ) )
6 oveq1 
 |-  ( A = 0h -> ( A .ih A ) = ( 0h .ih A ) )
7 hi01 
 |-  ( A e. ~H -> ( 0h .ih A ) = 0 )
8 6 7 sylan9eqr 
 |-  ( ( A e. ~H /\ A = 0h ) -> ( A .ih A ) = 0 )
9 8 eqcomd 
 |-  ( ( A e. ~H /\ A = 0h ) -> 0 = ( A .ih A ) )
10 9 ex 
 |-  ( A e. ~H -> ( A = 0h -> 0 = ( A .ih A ) ) )
11 5 10 orim12d 
 |-  ( A e. ~H -> ( ( -. A = 0h \/ A = 0h ) -> ( 0 < ( A .ih A ) \/ 0 = ( A .ih A ) ) ) )
12 1 11 mpi 
 |-  ( A e. ~H -> ( 0 < ( A .ih A ) \/ 0 = ( A .ih A ) ) )
13 0re 
 |-  0 e. RR
14 hiidrcl 
 |-  ( A e. ~H -> ( A .ih A ) e. RR )
15 leloe 
 |-  ( ( 0 e. RR /\ ( A .ih A ) e. RR ) -> ( 0 <_ ( A .ih A ) <-> ( 0 < ( A .ih A ) \/ 0 = ( A .ih A ) ) ) )
16 13 14 15 sylancr 
 |-  ( A e. ~H -> ( 0 <_ ( A .ih A ) <-> ( 0 < ( A .ih A ) \/ 0 = ( A .ih A ) ) ) )
17 12 16 mpbird 
 |-  ( A e. ~H -> 0 <_ ( A .ih A ) )