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 ) |
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 ) |