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 )