Theorem uvccl

Description: A unit vector is a vector. (Contributed by Steven Nguyen, 16-Jul-2023)

	Ref	Expression
Hypotheses	uvccl.u	⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
	uvccl.y	⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
	uvccl.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
Assertion	uvccl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) → ( 𝑈 ‘ 𝐽 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		uvccl.u	⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
2		uvccl.y	⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
3		uvccl.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
4	1 2 3	uvcff	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝑈 : 𝐼 ⟶ 𝐵 )
5	4	3adant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) → 𝑈 : 𝐼 ⟶ 𝐵 )
6		simp3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) → 𝐽 ∈ 𝐼 )
7	5 6	ffvelcdmd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) → ( 𝑈 ‘ 𝐽 ) ∈ 𝐵 )