Metamath Proof Explorer


Theorem norm1exi

Description: A normalized vector exists in a subspace iff the subspace has a nonzero vector. (Contributed by NM, 9-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypothesis norm1ex.1
|- H e. SH
Assertion norm1exi
|- ( E. x e. H x =/= 0h <-> E. y e. H ( normh ` y ) = 1 )

Proof

Step Hyp Ref Expression
1 norm1ex.1
 |-  H e. SH
2 neeq1
 |-  ( x = z -> ( x =/= 0h <-> z =/= 0h ) )
3 2 cbvrexvw
 |-  ( E. x e. H x =/= 0h <-> E. z e. H z =/= 0h )
4 1 sheli
 |-  ( z e. H -> z e. ~H )
5 normcl
 |-  ( z e. ~H -> ( normh ` z ) e. RR )
6 4 5 syl
 |-  ( z e. H -> ( normh ` z ) e. RR )
7 6 adantr
 |-  ( ( z e. H /\ z =/= 0h ) -> ( normh ` z ) e. RR )
8 normne0
 |-  ( z e. ~H -> ( ( normh ` z ) =/= 0 <-> z =/= 0h ) )
9 4 8 syl
 |-  ( z e. H -> ( ( normh ` z ) =/= 0 <-> z =/= 0h ) )
10 9 biimpar
 |-  ( ( z e. H /\ z =/= 0h ) -> ( normh ` z ) =/= 0 )
11 7 10 rereccld
 |-  ( ( z e. H /\ z =/= 0h ) -> ( 1 / ( normh ` z ) ) e. RR )
12 11 recnd
 |-  ( ( z e. H /\ z =/= 0h ) -> ( 1 / ( normh ` z ) ) e. CC )
13 simpl
 |-  ( ( z e. H /\ z =/= 0h ) -> z e. H )
14 shmulcl
 |-  ( ( H e. SH /\ ( 1 / ( normh ` z ) ) e. CC /\ z e. H ) -> ( ( 1 / ( normh ` z ) ) .h z ) e. H )
15 1 14 mp3an1
 |-  ( ( ( 1 / ( normh ` z ) ) e. CC /\ z e. H ) -> ( ( 1 / ( normh ` z ) ) .h z ) e. H )
16 12 13 15 syl2anc
 |-  ( ( z e. H /\ z =/= 0h ) -> ( ( 1 / ( normh ` z ) ) .h z ) e. H )
17 norm1
 |-  ( ( z e. ~H /\ z =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` z ) ) .h z ) ) = 1 )
18 4 17 sylan
 |-  ( ( z e. H /\ z =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` z ) ) .h z ) ) = 1 )
19 fveqeq2
 |-  ( y = ( ( 1 / ( normh ` z ) ) .h z ) -> ( ( normh ` y ) = 1 <-> ( normh ` ( ( 1 / ( normh ` z ) ) .h z ) ) = 1 ) )
20 19 rspcev
 |-  ( ( ( ( 1 / ( normh ` z ) ) .h z ) e. H /\ ( normh ` ( ( 1 / ( normh ` z ) ) .h z ) ) = 1 ) -> E. y e. H ( normh ` y ) = 1 )
21 16 18 20 syl2anc
 |-  ( ( z e. H /\ z =/= 0h ) -> E. y e. H ( normh ` y ) = 1 )
22 21 rexlimiva
 |-  ( E. z e. H z =/= 0h -> E. y e. H ( normh ` y ) = 1 )
23 ax-1ne0
 |-  1 =/= 0
24 23 neii
 |-  -. 1 = 0
25 eqeq1
 |-  ( ( normh ` y ) = 1 -> ( ( normh ` y ) = 0 <-> 1 = 0 ) )
26 24 25 mtbiri
 |-  ( ( normh ` y ) = 1 -> -. ( normh ` y ) = 0 )
27 1 sheli
 |-  ( y e. H -> y e. ~H )
28 norm-i
 |-  ( y e. ~H -> ( ( normh ` y ) = 0 <-> y = 0h ) )
29 27 28 syl
 |-  ( y e. H -> ( ( normh ` y ) = 0 <-> y = 0h ) )
30 29 necon3bbid
 |-  ( y e. H -> ( -. ( normh ` y ) = 0 <-> y =/= 0h ) )
31 26 30 syl5ib
 |-  ( y e. H -> ( ( normh ` y ) = 1 -> y =/= 0h ) )
32 31 reximia
 |-  ( E. y e. H ( normh ` y ) = 1 -> E. y e. H y =/= 0h )
33 neeq1
 |-  ( y = z -> ( y =/= 0h <-> z =/= 0h ) )
34 33 cbvrexvw
 |-  ( E. y e. H y =/= 0h <-> E. z e. H z =/= 0h )
35 32 34 sylib
 |-  ( E. y e. H ( normh ` y ) = 1 -> E. z e. H z =/= 0h )
36 22 35 impbii
 |-  ( E. z e. H z =/= 0h <-> E. y e. H ( normh ` y ) = 1 )
37 3 36 bitri
 |-  ( E. x e. H x =/= 0h <-> E. y e. H ( normh ` y ) = 1 )