Metamath Proof Explorer


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 ffvelrnd ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊𝐽𝐼 ) → ( 𝑈𝐽 ) ∈ 𝐵 )