Metamath Proof Explorer

Theorem normgt0

Description: The norm of nonzero vector is positive. (Contributed by NM, 10-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion normgt0 
|- ( A e. ~H -> ( A =/= 0h <-> 0 < ( normh ` A ) ) )

Proof

Step Hyp Ref Expression
1 hiidrcl 
 |-  ( A e. ~H -> ( A .ih A ) e. RR )
2 1 adantr 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( A .ih A ) e. RR )
3 ax-his4 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( A .ih A ) )
4 sqrtgt0 
 |-  ( ( ( A .ih A ) e. RR /\ 0 < ( A .ih A ) ) -> 0 < ( sqrt ` ( A .ih A ) ) )
5 2 3 4 syl2anc 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( sqrt ` ( A .ih A ) ) )
6 5 ex 
 |-  ( A e. ~H -> ( A =/= 0h -> 0 < ( sqrt ` ( A .ih A ) ) ) )
7 oveq1 
 |-  ( A = 0h -> ( A .ih A ) = ( 0h .ih A ) )
8 hi01 
 |-  ( A e. ~H -> ( 0h .ih A ) = 0 )
9 7 8 sylan9eqr 
 |-  ( ( A e. ~H /\ A = 0h ) -> ( A .ih A ) = 0 )
10 9 fveq2d 
 |-  ( ( A e. ~H /\ A = 0h ) -> ( sqrt ` ( A .ih A ) ) = ( sqrt ` 0 ) )
11 sqrt0 
 |-  ( sqrt ` 0 ) = 0
12 10 11 eqtrdi 
 |-  ( ( A e. ~H /\ A = 0h ) -> ( sqrt ` ( A .ih A ) ) = 0 )
13 12 ex 
 |-  ( A e. ~H -> ( A = 0h -> ( sqrt ` ( A .ih A ) ) = 0 ) )
14 hiidge0 
 |-  ( A e. ~H -> 0 <_ ( A .ih A ) )
15 1 14 resqrtcld 
 |-  ( A e. ~H -> ( sqrt ` ( A .ih A ) ) e. RR )
16 0re 
 |-  0 e. RR
17 lttri3 
 |-  ( ( ( sqrt ` ( A .ih A ) ) e. RR /\ 0 e. RR ) -> ( ( sqrt ` ( A .ih A ) ) = 0 <-> ( -. ( sqrt ` ( A .ih A ) ) < 0 /\ -. 0 < ( sqrt ` ( A .ih A ) ) ) ) )
18 15 16 17 sylancl 
 |-  ( A e. ~H -> ( ( sqrt ` ( A .ih A ) ) = 0 <-> ( -. ( sqrt ` ( A .ih A ) ) < 0 /\ -. 0 < ( sqrt ` ( A .ih A ) ) ) ) )
19 simpr 
 |-  ( ( -. ( sqrt ` ( A .ih A ) ) < 0 /\ -. 0 < ( sqrt ` ( A .ih A ) ) ) -> -. 0 < ( sqrt ` ( A .ih A ) ) )
20 18 19 syl6bi 
 |-  ( A e. ~H -> ( ( sqrt ` ( A .ih A ) ) = 0 -> -. 0 < ( sqrt ` ( A .ih A ) ) ) )
21 13 20 syld 
 |-  ( A e. ~H -> ( A = 0h -> -. 0 < ( sqrt ` ( A .ih A ) ) ) )
22 21 necon2ad 
 |-  ( A e. ~H -> ( 0 < ( sqrt ` ( A .ih A ) ) -> A =/= 0h ) )
23 6 22 impbid 
 |-  ( A e. ~H -> ( A =/= 0h <-> 0 < ( sqrt ` ( A .ih A ) ) ) )
24 normval 
 |-  ( A e. ~H -> ( normh ` A ) = ( sqrt ` ( A .ih A ) ) )
25 24 breq2d 
 |-  ( A e. ~H -> ( 0 < ( normh ` A ) <-> 0 < ( sqrt ` ( A .ih A ) ) ) )
26 23 25 bitr4d 
 |-  ( A e. ~H -> ( A =/= 0h <-> 0 < ( normh ` A ) ) )