Theorem 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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	ncvs1.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
	ncvs1.z	⊢ 0 = ( 0g ‘ 𝐺 )
	ncvs1.s	⊢ · = ( ·𝑠 ‘ 𝐺 )
	ncvs1.f	⊢ 𝐹 = ( Scalar ‘ 𝐺 )
	ncvs1.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	ncvs1	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ∧ ( 1 / ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐾 ) → ( 𝑁 ‘ ( ( 1 / ( 𝑁 ‘ 𝐴 ) ) · 𝐴 ) ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		ncvs1.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		ncvs1.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
3		ncvs1.z	⊢ 0 = ( 0g ‘ 𝐺 )
4		ncvs1.s	⊢ · = ( ·𝑠 ‘ 𝐺 )
5		ncvs1.f	⊢ 𝐹 = ( Scalar ‘ 𝐺 )
6		ncvs1.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
7		simp1	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ∧ ( 1 / ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐾 ) → 𝐺 ∈ ( NrmVec ∩ ℂVec ) )
8		simp3	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ∧ ( 1 / ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐾 ) → ( 1 / ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐾 )
9		elin	⊢ ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ↔ ( 𝐺 ∈ NrmVec ∧ 𝐺 ∈ ℂVec ) )
10		nvcnlm	⊢ ( 𝐺 ∈ NrmVec → 𝐺 ∈ NrmMod )
11		nlmngp	⊢ ( 𝐺 ∈ NrmMod → 𝐺 ∈ NrmGrp )
12	10 11	syl	⊢ ( 𝐺 ∈ NrmVec → 𝐺 ∈ NrmGrp )
13	12	adantr	⊢ ( ( 𝐺 ∈ NrmVec ∧ 𝐺 ∈ ℂVec ) → 𝐺 ∈ NrmGrp )
14	9 13	sylbi	⊢ ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) → 𝐺 ∈ NrmGrp )
15		simpl	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ 𝑋 )
16	14 15	anim12i	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ) → ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) )
17	1 2	nmcl	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
18	16 17	syl	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
19	1 2 3	nmeq0	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )
20	19	bicomd	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 = 0 ↔ ( 𝑁 ‘ 𝐴 ) = 0 ) )
21	14 20	sylan	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 = 0 ↔ ( 𝑁 ‘ 𝐴 ) = 0 ) )
22	21	necon3bid	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ≠ 0 ↔ ( 𝑁 ‘ 𝐴 ) ≠ 0 ) )
23	22	biimpd	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ≠ 0 → ( 𝑁 ‘ 𝐴 ) ≠ 0 ) )
24	23	impr	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ) → ( 𝑁 ‘ 𝐴 ) ≠ 0 )
25	18 24	rereccld	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ) → ( 1 / ( 𝑁 ‘ 𝐴 ) ) ∈ ℝ )
26	25	3adant3	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ∧ ( 1 / ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐾 ) → ( 1 / ( 𝑁 ‘ 𝐴 ) ) ∈ ℝ )
27	8 26	elind	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ∧ ( 1 / ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐾 ) → ( 1 / ( 𝑁 ‘ 𝐴 ) ) ∈ ( 𝐾 ∩ ℝ ) )
28		1re	⊢ 1 ∈ ℝ
29		0le1	⊢ 0 ≤ 1
30	28 29	pm3.2i	⊢ ( 1 ∈ ℝ ∧ 0 ≤ 1 )
31	30	a1i	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ) → ( 1 ∈ ℝ ∧ 0 ≤ 1 ) )
32		simprr	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ) → 𝐴 ≠ 0 )
33	1 2 3	nmgt0	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ≠ 0 ↔ 0 < ( 𝑁 ‘ 𝐴 ) ) )
34	16 33	syl	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ) → ( 𝐴 ≠ 0 ↔ 0 < ( 𝑁 ‘ 𝐴 ) ) )
35	32 34	mpbid	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ) → 0 < ( 𝑁 ‘ 𝐴 ) )
36	31 18 35	jca32	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ) → ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ ( ( 𝑁 ‘ 𝐴 ) ∈ ℝ ∧ 0 < ( 𝑁 ‘ 𝐴 ) ) ) )
37	36	3adant3	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ∧ ( 1 / ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐾 ) → ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ ( ( 𝑁 ‘ 𝐴 ) ∈ ℝ ∧ 0 < ( 𝑁 ‘ 𝐴 ) ) ) )
38		divge0	⊢ ( ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ ( ( 𝑁 ‘ 𝐴 ) ∈ ℝ ∧ 0 < ( 𝑁 ‘ 𝐴 ) ) ) → 0 ≤ ( 1 / ( 𝑁 ‘ 𝐴 ) ) )
39	37 38	syl	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ∧ ( 1 / ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐾 ) → 0 ≤ ( 1 / ( 𝑁 ‘ 𝐴 ) ) )
40		simp2l	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ∧ ( 1 / ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐾 ) → 𝐴 ∈ 𝑋 )
41	1 2 4 5 6	ncvsge0	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( ( 1 / ( 𝑁 ‘ 𝐴 ) ) ∈ ( 𝐾 ∩ ℝ ) ∧ 0 ≤ ( 1 / ( 𝑁 ‘ 𝐴 ) ) ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ ( ( 1 / ( 𝑁 ‘ 𝐴 ) ) · 𝐴 ) ) = ( ( 1 / ( 𝑁 ‘ 𝐴 ) ) · ( 𝑁 ‘ 𝐴 ) ) )
42	7 27 39 40 41	syl121anc	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ∧ ( 1 / ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐾 ) → ( 𝑁 ‘ ( ( 1 / ( 𝑁 ‘ 𝐴 ) ) · 𝐴 ) ) = ( ( 1 / ( 𝑁 ‘ 𝐴 ) ) · ( 𝑁 ‘ 𝐴 ) ) )
43	16	3adant3	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ∧ ( 1 / ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐾 ) → ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) )
44	43 17	syl	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ∧ ( 1 / ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐾 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
45	44	recnd	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ∧ ( 1 / ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐾 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℂ )
46	24	3adant3	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ∧ ( 1 / ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐾 ) → ( 𝑁 ‘ 𝐴 ) ≠ 0 )
47	45 46	recid2d	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ∧ ( 1 / ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐾 ) → ( ( 1 / ( 𝑁 ‘ 𝐴 ) ) · ( 𝑁 ‘ 𝐴 ) ) = 1 )
48	42 47	eqtrd	⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ∧ ( 1 / ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐾 ) → ( 𝑁 ‘ ( ( 1 / ( 𝑁 ‘ 𝐴 ) ) · 𝐴 ) ) = 1 )