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	ffvelcdmd	|- ( ( R e. Ring /\ I e. W /\ J e. I ) -> ( U ` J ) e. B )