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 S_{ℋ}$
	Assertion	norm1exi	$⊢ \exists x \in H x \neq 0_{ℎ} \leftrightarrow \exists y \in H {norm}_{ℎ} (y) = 1$

Proof

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

Metamath Proof Explorer

Theorem norm1exi

Proof