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 𝐻S
Assertion norm1exi ( ∃ 𝑥𝐻 𝑥 ≠ 0 ↔ ∃ 𝑦𝐻 ( norm𝑦 ) = 1 )

Proof

Step Hyp Ref Expression
1 norm1ex.1 𝐻S
2 neeq1 ( 𝑥 = 𝑧 → ( 𝑥 ≠ 0𝑧 ≠ 0 ) )
3 2 cbvrexvw ( ∃ 𝑥𝐻 𝑥 ≠ 0 ↔ ∃ 𝑧𝐻 𝑧 ≠ 0 )
4 1 sheli ( 𝑧𝐻𝑧 ∈ ℋ )
5 normcl ( 𝑧 ∈ ℋ → ( norm𝑧 ) ∈ ℝ )
6 4 5 syl ( 𝑧𝐻 → ( norm𝑧 ) ∈ ℝ )
7 6 adantr ( ( 𝑧𝐻𝑧 ≠ 0 ) → ( norm𝑧 ) ∈ ℝ )
8 normne0 ( 𝑧 ∈ ℋ → ( ( norm𝑧 ) ≠ 0 ↔ 𝑧 ≠ 0 ) )
9 4 8 syl ( 𝑧𝐻 → ( ( norm𝑧 ) ≠ 0 ↔ 𝑧 ≠ 0 ) )
10 9 biimpar ( ( 𝑧𝐻𝑧 ≠ 0 ) → ( norm𝑧 ) ≠ 0 )
11 7 10 rereccld ( ( 𝑧𝐻𝑧 ≠ 0 ) → ( 1 / ( norm𝑧 ) ) ∈ ℝ )
12 11 recnd ( ( 𝑧𝐻𝑧 ≠ 0 ) → ( 1 / ( norm𝑧 ) ) ∈ ℂ )
13 simpl ( ( 𝑧𝐻𝑧 ≠ 0 ) → 𝑧𝐻 )
14 shmulcl ( ( 𝐻S ∧ ( 1 / ( norm𝑧 ) ) ∈ ℂ ∧ 𝑧𝐻 ) → ( ( 1 / ( norm𝑧 ) ) · 𝑧 ) ∈ 𝐻 )
15 1 14 mp3an1 ( ( ( 1 / ( norm𝑧 ) ) ∈ ℂ ∧ 𝑧𝐻 ) → ( ( 1 / ( norm𝑧 ) ) · 𝑧 ) ∈ 𝐻 )
16 12 13 15 syl2anc ( ( 𝑧𝐻𝑧 ≠ 0 ) → ( ( 1 / ( norm𝑧 ) ) · 𝑧 ) ∈ 𝐻 )
17 norm1 ( ( 𝑧 ∈ ℋ ∧ 𝑧 ≠ 0 ) → ( norm ‘ ( ( 1 / ( norm𝑧 ) ) · 𝑧 ) ) = 1 )
18 4 17 sylan ( ( 𝑧𝐻𝑧 ≠ 0 ) → ( norm ‘ ( ( 1 / ( norm𝑧 ) ) · 𝑧 ) ) = 1 )
19 fveqeq2 ( 𝑦 = ( ( 1 / ( norm𝑧 ) ) · 𝑧 ) → ( ( norm𝑦 ) = 1 ↔ ( norm ‘ ( ( 1 / ( norm𝑧 ) ) · 𝑧 ) ) = 1 ) )
20 19 rspcev ( ( ( ( 1 / ( norm𝑧 ) ) · 𝑧 ) ∈ 𝐻 ∧ ( norm ‘ ( ( 1 / ( norm𝑧 ) ) · 𝑧 ) ) = 1 ) → ∃ 𝑦𝐻 ( norm𝑦 ) = 1 )
21 16 18 20 syl2anc ( ( 𝑧𝐻𝑧 ≠ 0 ) → ∃ 𝑦𝐻 ( norm𝑦 ) = 1 )
22 21 rexlimiva ( ∃ 𝑧𝐻 𝑧 ≠ 0 → ∃ 𝑦𝐻 ( norm𝑦 ) = 1 )
23 ax-1ne0 1 ≠ 0
24 23 neii ¬ 1 = 0
25 eqeq1 ( ( norm𝑦 ) = 1 → ( ( norm𝑦 ) = 0 ↔ 1 = 0 ) )
26 24 25 mtbiri ( ( norm𝑦 ) = 1 → ¬ ( norm𝑦 ) = 0 )
27 1 sheli ( 𝑦𝐻𝑦 ∈ ℋ )
28 norm-i ( 𝑦 ∈ ℋ → ( ( norm𝑦 ) = 0 ↔ 𝑦 = 0 ) )
29 27 28 syl ( 𝑦𝐻 → ( ( norm𝑦 ) = 0 ↔ 𝑦 = 0 ) )
30 29 necon3bbid ( 𝑦𝐻 → ( ¬ ( norm𝑦 ) = 0 ↔ 𝑦 ≠ 0 ) )
31 26 30 syl5ib ( 𝑦𝐻 → ( ( norm𝑦 ) = 1 → 𝑦 ≠ 0 ) )
32 31 reximia ( ∃ 𝑦𝐻 ( norm𝑦 ) = 1 → ∃ 𝑦𝐻 𝑦 ≠ 0 )
33 neeq1 ( 𝑦 = 𝑧 → ( 𝑦 ≠ 0𝑧 ≠ 0 ) )
34 33 cbvrexvw ( ∃ 𝑦𝐻 𝑦 ≠ 0 ↔ ∃ 𝑧𝐻 𝑧 ≠ 0 )
35 32 34 sylib ( ∃ 𝑦𝐻 ( norm𝑦 ) = 1 → ∃ 𝑧𝐻 𝑧 ≠ 0 )
36 22 35 impbii ( ∃ 𝑧𝐻 𝑧 ≠ 0 ↔ ∃ 𝑦𝐻 ( norm𝑦 ) = 1 )
37 3 36 bitri ( ∃ 𝑥𝐻 𝑥 ≠ 0 ↔ ∃ 𝑦𝐻 ( norm𝑦 ) = 1 )