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