ncvs1

Description: From any nonzero vector of a normed subcomplex vector space, construct a collinear vector whose norm is one. (Contributed by NM, 6-Dec-2007) (Revised by AV, 8-Oct-2021)

	Ref	Expression
Hypotheses	ncvs1.x	$⊢ X = {Base}_{G}$
	ncvs1.n	$⊢ N = norm (G)$
	ncvs1.z	$⊢ \underset{˙}{0} = 0_{G}$
	ncvs1.s	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	ncvs1.f	$⊢ F = Scalar (G)$
	ncvs1.k	$⊢ K = {Base}_{F}$
Assertion	ncvs1	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0}) \land \frac{1}{N (A)} \in K) \to N ((\frac{1}{N (A)}) \underset{˙}{\cdot} A) = 1$

Proof

Step	Hyp	Ref	Expression
1		ncvs1.x	$⊢ X = {Base}_{G}$
2		ncvs1.n	$⊢ N = norm (G)$
3		ncvs1.z	$⊢ \underset{˙}{0} = 0_{G}$
4		ncvs1.s	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
5		ncvs1.f	$⊢ F = Scalar (G)$
6		ncvs1.k	$⊢ K = {Base}_{F}$
7		simp1	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0}) \land \frac{1}{N (A)} \in K) \to G \in (NrmVec \cap ℂVec)$
8		simp3	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0}) \land \frac{1}{N (A)} \in K) \to \frac{1}{N (A)} \in K$
9		elin	$⊢ G \in (NrmVec \cap ℂVec) \leftrightarrow (G \in NrmVec \land G \in ℂVec)$
10		nvcnlm	$⊢ G \in NrmVec \to G \in NrmMod$
11		nlmngp	$⊢ G \in NrmMod \to G \in NrmGrp$
12	10 11	syl	$⊢ G \in NrmVec \to G \in NrmGrp$
13	12	adantr	$⊢ (G \in NrmVec \land G \in ℂVec) \to G \in NrmGrp$
14	9 13	sylbi	$⊢ G \in (NrmVec \cap ℂVec) \to G \in NrmGrp$
15		simpl	$⊢ (A \in X \land A \neq \underset{˙}{0}) \to A \in X$
16	14 15	anim12i	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0})) \to (G \in NrmGrp \land A \in X)$
17	1 2	nmcl	$⊢ (G \in NrmGrp \land A \in X) \to N (A) \in ℝ$
18	16 17	syl	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0})) \to N (A) \in ℝ$
19	1 2 3	nmeq0	$⊢ (G \in NrmGrp \land A \in X) \to (N (A) = 0 \leftrightarrow A = \underset{˙}{0})$
20	19	bicomd	$⊢ (G \in NrmGrp \land A \in X) \to (A = \underset{˙}{0} \leftrightarrow N (A) = 0)$
21	14 20	sylan	$⊢ (G \in (NrmVec \cap ℂVec) \land A \in X) \to (A = \underset{˙}{0} \leftrightarrow N (A) = 0)$
22	21	necon3bid	$⊢ (G \in (NrmVec \cap ℂVec) \land A \in X) \to (A \neq \underset{˙}{0} \leftrightarrow N (A) \neq 0)$
23	22	biimpd	$⊢ (G \in (NrmVec \cap ℂVec) \land A \in X) \to (A \neq \underset{˙}{0} \to N (A) \neq 0)$
24	23	impr	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0})) \to N (A) \neq 0$
25	18 24	rereccld	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0})) \to \frac{1}{N (A)} \in ℝ$
26	25	3adant3	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0}) \land \frac{1}{N (A)} \in K) \to \frac{1}{N (A)} \in ℝ$
27	8 26	elind	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0}) \land \frac{1}{N (A)} \in K) \to \frac{1}{N (A)} \in (K \cap ℝ)$
28		1re	$⊢ 1 \in ℝ$
29		0le1	$⊢ 0 \leq 1$
30	28 29	pm3.2i	$⊢ (1 \in ℝ \land 0 \leq 1)$
31	30	a1i	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0})) \to (1 \in ℝ \land 0 \leq 1)$
32		simprr	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0})) \to A \neq \underset{˙}{0}$
33	1 2 3	nmgt0	$⊢ (G \in NrmGrp \land A \in X) \to (A \neq \underset{˙}{0} \leftrightarrow 0 < N (A))$
34	16 33	syl	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0})) \to (A \neq \underset{˙}{0} \leftrightarrow 0 < N (A))$
35	32 34	mpbid	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0})) \to 0 < N (A)$
36	31 18 35	jca32	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0})) \to ((1 \in ℝ \land 0 \leq 1) \land (N (A) \in ℝ \land 0 < N (A)))$
37	36	3adant3	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0}) \land \frac{1}{N (A)} \in K) \to ((1 \in ℝ \land 0 \leq 1) \land (N (A) \in ℝ \land 0 < N (A)))$
38		divge0	$⊢ ((1 \in ℝ \land 0 \leq 1) \land (N (A) \in ℝ \land 0 < N (A))) \to 0 \leq \frac{1}{N (A)}$
39	37 38	syl	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0}) \land \frac{1}{N (A)} \in K) \to 0 \leq \frac{1}{N (A)}$
40		simp2l	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0}) \land \frac{1}{N (A)} \in K) \to A \in X$
41	1 2 4 5 6	ncvsge0	$⊢ (G \in (NrmVec \cap ℂVec) \land (\frac{1}{N (A)} \in (K \cap ℝ) \land 0 \leq \frac{1}{N (A)}) \land A \in X) \to N ((\frac{1}{N (A)}) \underset{˙}{\cdot} A) = (\frac{1}{N (A)}) N (A)$
42	7 27 39 40 41	syl121anc	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0}) \land \frac{1}{N (A)} \in K) \to N ((\frac{1}{N (A)}) \underset{˙}{\cdot} A) = (\frac{1}{N (A)}) N (A)$
43	16	3adant3	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0}) \land \frac{1}{N (A)} \in K) \to (G \in NrmGrp \land A \in X)$
44	43 17	syl	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0}) \land \frac{1}{N (A)} \in K) \to N (A) \in ℝ$
45	44	recnd	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0}) \land \frac{1}{N (A)} \in K) \to N (A) \in ℂ$
46	24	3adant3	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0}) \land \frac{1}{N (A)} \in K) \to N (A) \neq 0$
47	45 46	recid2d	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0}) \land \frac{1}{N (A)} \in K) \to (\frac{1}{N (A)}) N (A) = 1$
48	42 47	eqtrd	$⊢ (G \in (NrmVec \cap ℂVec) \land (A \in X \land A \neq \underset{˙}{0}) \land \frac{1}{N (A)} \in K) \to N ((\frac{1}{N (A)}) \underset{˙}{\cdot} A) = 1$

Metamath Proof Explorer

Theorem ncvs1

Proof