This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrid ⊢ ( 𝑦 ∈ 𝐻 → ( ( 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 )