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∈Sℋ
Assertion norm1exi ⊢∃x∈Hx≠0ℎ↔∃y∈Hnormℎ⁡y=1

Proof

Step Hyp Ref Expression
1 norm1ex.1 ⊢H∈Sℋ
2 neeq1 ⊢x=z→x≠0ℎ↔z≠0ℎ
3 2 cbvrexvw ⊢∃x∈Hx≠0ℎ↔∃z∈Hz≠0ℎ
4 1 sheli ⊢z∈H→z∈ℋ
5 normcl ⊢z∈ℋ→normℎ⁡z∈ℝ
6 4 5 syl ⊢z∈H→normℎ⁡z∈ℝ
7 6 adantr ⊢z∈H∧z≠0ℎ→normℎ⁡z∈ℝ
8 normne0 ⊢z∈ℋ→normℎ⁡z≠0↔z≠0ℎ
9 4 8 syl ⊢z∈H→normℎ⁡z≠0↔z≠0ℎ
10 9 biimpar ⊢z∈H∧z≠0ℎ→normℎ⁡z≠0
11 7 10 rereccld ⊢z∈H∧z≠0ℎ→1normℎ⁡z∈ℝ
12 11 recnd ⊢z∈H∧z≠0ℎ→1normℎ⁡z∈ℂ
13 simpl ⊢z∈H∧z≠0ℎ→z∈H
14 shmulcl ⊢H∈Sℋ∧1normℎ⁡z∈ℂ∧z∈H→1normℎ⁡z⋅ℎz∈H
15 1 14 mp3an1 ⊢1normℎ⁡z∈ℂ∧z∈H→1normℎ⁡z⋅ℎz∈H
16 12 13 15 syl2anc ⊢z∈H∧z≠0ℎ→1normℎ⁡z⋅ℎz∈H
17 norm1 ⊢z∈ℋ∧z≠0ℎ→normℎ⁡1normℎ⁡z⋅ℎz=1
18 4 17 sylan ⊢z∈H∧z≠0ℎ→normℎ⁡1normℎ⁡z⋅ℎz=1
19 fveqeq2 ⊢y=1normℎ⁡z⋅ℎz→normℎ⁡y=1↔normℎ⁡1normℎ⁡z⋅ℎz=1
20 19 rspcev ⊢1normℎ⁡z⋅ℎz∈H∧normℎ⁡1normℎ⁡z⋅ℎz=1→∃y∈Hnormℎ⁡y=1
21 16 18 20 syl2anc ⊢z∈H∧z≠0ℎ→∃y∈Hnormℎ⁡y=1
22 21 rexlimiva ⊢∃z∈Hz≠0ℎ→∃y∈Hnormℎ⁡y=1
23 ax-1ne0 ⊢1≠0
24 23 neii ⊢¬1=0
25 eqeq1 ⊢normℎ⁡y=1→normℎ⁡y=0↔1=0
26 24 25 mtbiri ⊢normℎ⁡y=1→¬normℎ⁡y=0
27 1 sheli ⊢y∈H→y∈ℋ
28 norm-i ⊢y∈ℋ→normℎ⁡y=0↔y=0ℎ
29 27 28 syl ⊢y∈H→normℎ⁡y=0↔y=0ℎ
30 29 necon3bbid ⊢y∈H→¬normℎ⁡y=0↔y≠0ℎ
31 26 30 imbitrid ⊢y∈H→normℎ⁡y=1→y≠0ℎ
32 31 reximia ⊢∃y∈Hnormℎ⁡y=1→∃y∈Hy≠0ℎ
33 neeq1 ⊢y=z→y≠0ℎ↔z≠0ℎ
34 33 cbvrexvw ⊢∃y∈Hy≠0ℎ↔∃z∈Hz≠0ℎ
35 32 34 sylib ⊢∃y∈Hnormℎ⁡y=1→∃z∈Hz≠0ℎ
36 22 35 impbii ⊢∃z∈Hz≠0ℎ↔∃y∈Hnormℎ⁡y=1
37 3 36 bitri ⊢∃x∈Hx≠0ℎ↔∃y∈Hnormℎ⁡y=1