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 e. Ring /\ I e. W /\ J e. I ) -> ( U ` J ) e. 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 e. Ring /\ I e. W ) -> U : I --> B )
5 4 3adant3
 |-  ( ( R e. Ring /\ I e. W /\ J e. I ) -> U : I --> B )
6 simp3
 |-  ( ( R e. Ring /\ I e. W /\ J e. I ) -> J e. I )
7 5 6 ffvelrnd
 |-  ( ( R e. Ring /\ I e. W /\ J e. I ) -> ( U ` J ) e. B )