Theorem uvccl

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

	Ref	Expression
Hypotheses	uvccl.u	$$⊢U=R\mathrm{unitVec}I$$
	uvccl.y	$$⊢Y=R\mathrm{freeLMod}I$$
	uvccl.b	$$⊢B={\mathrm{Base}}_Y$$
Assertion	uvccl	$$⊢\left(R\in \mathrm{Ring}\wedge I\in W\wedge J\in I\right)\to U\left(J\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		uvccl.u	$$⊢U=R\mathrm{unitVec}I$$
2		uvccl.y	$$⊢Y=R\mathrm{freeLMod}I$$
3		uvccl.b	$$⊢B={\mathrm{Base}}_Y$$
4	1 2 3	uvcff	$$⊢\left(R\in \mathrm{Ring}\wedge I\in W\right)\to U:I⟶B$$
5	4	3adant3	$$⊢\left(R\in \mathrm{Ring}\wedge I\in W\wedge J\in I\right)\to U:I⟶B$$
6		simp3	$$⊢\left(R\in \mathrm{Ring}\wedge I\in W\wedge J\in I\right)\to J\in I$$
7	5 6	ffvelcdmd	$$⊢\left(R\in \mathrm{Ring}\wedge I\in W\wedge J\in I\right)\to U\left(J\right)\in B$$