Metamath Proof Explorer

Theorem uvccl

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

Ref Expression
Hypotheses uvccl.u ⊢ U = R unitVec I
uvccl.y ⊢ Y = R freeLMod I
uvccl.b ⊢ B = Base Y
Assertion uvccl ⊢ R ∈ Ring ∧ I ∈ W ∧ J ∈ I → U ⁡ J ∈ B

Proof

Step Hyp Ref Expression
1 uvccl.u ⊢ U = R unitVec I
2 uvccl.y ⊢ Y = R freeLMod I
3 uvccl.b ⊢ B = Base Y
4 1 2 3 uvcff ⊢ R ∈ Ring ∧ I ∈ W → U : I ⟶ B
5 4 3adant3 ⊢ R ∈ Ring ∧ I ∈ W ∧ J ∈ I → U : I ⟶ B
6 simp3 ⊢ R ∈ Ring ∧ I ∈ W ∧ J ∈ I → J ∈ I
7 5 6 ffvelrnd ⊢ R ∈ Ring ∧ I ∈ W ∧ J ∈ I → U ⁡ J ∈ B