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 ) ) )