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\in {\mathbf{S}}_{\mathscr{H}}$$
Assertion	norm1exi	$$⊢\exists x\in Hx\ne 0_{ℎ}\leftrightarrow \exists y\in H{norm}_{ℎ}\left(y\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		norm1ex.1	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}$$
2		neeq1	$$⊢x=z\to \left(x\ne 0_{ℎ}\leftrightarrow z\ne 0_{ℎ}\right)$$
3	2	cbvrexvw	$$⊢\exists x\in Hx\ne 0_{ℎ}\leftrightarrow \exists z\in Hz\ne 0_{ℎ}$$
4	1	sheli	$$⊢z\in H\to z\in \mathscr{H}$$
5		normcl	$$⊢z\in \mathscr{H}\to {norm}_{ℎ}\left(z\right)\in ℝ$$
6	4 5	syl	$$⊢z\in H\to {norm}_{ℎ}\left(z\right)\in ℝ$$
7	6	adantr	$$⊢\left(z\in H\wedge z\ne 0_{ℎ}\right)\to {norm}_{ℎ}\left(z\right)\in ℝ$$
8		normne0	$$⊢z\in \mathscr{H}\to \left({norm}_{ℎ}\left(z\right)\ne 0\leftrightarrow z\ne 0_{ℎ}\right)$$
9	4 8	syl	$$⊢z\in H\to \left({norm}_{ℎ}\left(z\right)\ne 0\leftrightarrow z\ne 0_{ℎ}\right)$$
10	9	biimpar	$$⊢\left(z\in H\wedge z\ne 0_{ℎ}\right)\to {norm}_{ℎ}\left(z\right)\ne 0$$
11	7 10	rereccld	$$⊢\left(z\in H\wedge z\ne 0_{ℎ}\right)\to \frac{1}{{norm}_{ℎ}\left(z\right)}\in ℝ$$
12	11	recnd	$$⊢\left(z\in H\wedge z\ne 0_{ℎ}\right)\to \frac{1}{{norm}_{ℎ}\left(z\right)}\in ℂ$$
13		simpl	$$⊢\left(z\in H\wedge z\ne 0_{ℎ}\right)\to z\in H$$
14		shmulcl	$$⊢\left(H\in {\mathbf{S}}_{\mathscr{H}}\wedge \frac{1}{{norm}_{ℎ}\left(z\right)}\in ℂ\wedge z\in H\right)\to \left(\frac{1}{{norm}_{ℎ}\left(z\right)}\right){\cdot }_{ℎ}z\in H$$
15	1 14	mp3an1	$$⊢\left(\frac{1}{{norm}_{ℎ}\left(z\right)}\in ℂ\wedge z\in H\right)\to \left(\frac{1}{{norm}_{ℎ}\left(z\right)}\right){\cdot }_{ℎ}z\in H$$
16	12 13 15	syl2anc	$$⊢\left(z\in H\wedge z\ne 0_{ℎ}\right)\to \left(\frac{1}{{norm}_{ℎ}\left(z\right)}\right){\cdot }_{ℎ}z\in H$$
17		norm1	$$⊢\left(z\in \mathscr{H}\wedge z\ne 0_{ℎ}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left(z\right)}\right){\cdot }_{ℎ}z\right)=1$$
18	4 17	sylan	$$⊢\left(z\in H\wedge z\ne 0_{ℎ}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left(z\right)}\right){\cdot }_{ℎ}z\right)=1$$
19		fveqeq2	$$⊢y=\left(\frac{1}{{norm}_{ℎ}\left(z\right)}\right){\cdot }_{ℎ}z\to \left({norm}_{ℎ}\left(y\right)=1\leftrightarrow {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left(z\right)}\right){\cdot }_{ℎ}z\right)=1\right)$$
20	19	rspcev	$$⊢\left(\left(\frac{1}{{norm}_{ℎ}\left(z\right)}\right){\cdot }_{ℎ}z\in H\wedge {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left(z\right)}\right){\cdot }_{ℎ}z\right)=1\right)\to \exists y\in H{norm}_{ℎ}\left(y\right)=1$$
21	16 18 20	syl2anc	$$⊢\left(z\in H\wedge z\ne 0_{ℎ}\right)\to \exists y\in H{norm}_{ℎ}\left(y\right)=1$$
22	21	rexlimiva	$$⊢\exists z\in Hz\ne 0_{ℎ}\to \exists y\in H{norm}_{ℎ}\left(y\right)=1$$
23		ax-1ne0	$$⊢1\ne 0$$
24	23	neii	$$⊢\neg 1=0$$
25		eqeq1	$$⊢{norm}_{ℎ}\left(y\right)=1\to \left({norm}_{ℎ}\left(y\right)=0\leftrightarrow 1=0\right)$$
26	24 25	mtbiri	$$⊢{norm}_{ℎ}\left(y\right)=1\to \neg {norm}_{ℎ}\left(y\right)=0$$
27	1	sheli	$$⊢y\in H\to y\in \mathscr{H}$$
28		norm-i	$$⊢y\in \mathscr{H}\to \left({norm}_{ℎ}\left(y\right)=0\leftrightarrow y=0_{ℎ}\right)$$
29	27 28	syl	$$⊢y\in H\to \left({norm}_{ℎ}\left(y\right)=0\leftrightarrow y=0_{ℎ}\right)$$
30	29	necon3bbid	$$⊢y\in H\to \left(\neg {norm}_{ℎ}\left(y\right)=0\leftrightarrow y\ne 0_{ℎ}\right)$$
31	26 30	syl5ib	$$⊢y\in H\to \left({norm}_{ℎ}\left(y\right)=1\to y\ne 0_{ℎ}\right)$$
32	31	reximia	$$⊢\exists y\in H{norm}_{ℎ}\left(y\right)=1\to \exists y\in Hy\ne 0_{ℎ}$$
33		neeq1	$$⊢y=z\to \left(y\ne 0_{ℎ}\leftrightarrow z\ne 0_{ℎ}\right)$$
34	33	cbvrexvw	$$⊢\exists y\in Hy\ne 0_{ℎ}\leftrightarrow \exists z\in Hz\ne 0_{ℎ}$$
35	32 34	sylib	$$⊢\exists y\in H{norm}_{ℎ}\left(y\right)=1\to \exists z\in Hz\ne 0_{ℎ}$$
36	22 35	impbii	$$⊢\exists z\in Hz\ne 0_{ℎ}\leftrightarrow \exists y\in H{norm}_{ℎ}\left(y\right)=1$$
37	3 36	bitri	$$⊢\exists x\in Hx\ne 0_{ℎ}\leftrightarrow \exists y\in H{norm}_{ℎ}\left(y\right)=1$$