Metamath Proof Explorer

Theorem norm1

Description: From any nonzero Hilbert space vector, construct a vector whose norm is 1. (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion norm1 
|- ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) = 1 )

Proof

Step Hyp Ref Expression
1 normcl 
 |-  ( A e. ~H -> ( normh ` A ) e. RR )
2 1 adantr 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` A ) e. RR )
3 normne0 
 |-  ( A e. ~H -> ( ( normh ` A ) =/= 0 <-> A =/= 0h ) )
4 3 biimpar 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` A ) =/= 0 )
5 2 4 rereccld 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( 1 / ( normh ` A ) ) e. RR )
6 5 recnd 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( 1 / ( normh ` A ) ) e. CC )
7 simpl 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> A e. ~H )
8 norm-iii 
 |-  ( ( ( 1 / ( normh ` A ) ) e. CC /\ A e. ~H ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) = ( ( abs ` ( 1 / ( normh ` A ) ) ) x. ( normh ` A ) ) )
9 6 7 8 syl2anc 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) = ( ( abs ` ( 1 / ( normh ` A ) ) ) x. ( normh ` A ) ) )
10 normgt0 
 |-  ( A e. ~H -> ( A =/= 0h <-> 0 < ( normh ` A ) ) )
11 10 biimpa 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( normh ` A ) )
12 1re 
 |-  1 e. RR
13 0le1 
 |-  0 <_ 1
14 divge0 
 |-  ( ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( ( normh ` A ) e. RR /\ 0 < ( normh ` A ) ) ) -> 0 <_ ( 1 / ( normh ` A ) ) )
15 12 13 14 mpanl12 
 |-  ( ( ( normh ` A ) e. RR /\ 0 < ( normh ` A ) ) -> 0 <_ ( 1 / ( normh ` A ) ) )
16 2 11 15 syl2anc 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> 0 <_ ( 1 / ( normh ` A ) ) )
17 5 16 absidd 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( abs ` ( 1 / ( normh ` A ) ) ) = ( 1 / ( normh ` A ) ) )
18 17 oveq1d 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( ( abs ` ( 1 / ( normh ` A ) ) ) x. ( normh ` A ) ) = ( ( 1 / ( normh ` A ) ) x. ( normh ` A ) ) )
19 1 recnd 
 |-  ( A e. ~H -> ( normh ` A ) e. CC )
20 19 adantr 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` A ) e. CC )
21 20 4 recid2d 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( ( 1 / ( normh ` A ) ) x. ( normh ` A ) ) = 1 )
22 9 18 21 3eqtrd 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) = 1 )