Theorem rnasclsubrg

Description: The scalar multiples of the unit vector form a subring of the vectors. (Contributed by SN, 5-Nov-2023)

	Ref	Expression
Hypotheses	rnasclsubrg.c	$$⊢C=\mathrm{algSc}\left(W\right)$$
	rnasclsubrg.w	$$⊢\phi \to W\in \mathrm{AssAlg}$$
Assertion	rnasclsubrg	$$⊢\phi \to \mathrm{ran}C\in \mathrm{SubRing}\left(W\right)$$

Proof

Step	Hyp	Ref	Expression
1		rnasclsubrg.c	$$⊢C=\mathrm{algSc}\left(W\right)$$
2		rnasclsubrg.w	$$⊢\phi \to W\in \mathrm{AssAlg}$$
3		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
4	1 3	asclrhm	$$⊢W\in \mathrm{AssAlg}\to C\in \left(\mathrm{Scalar}\left(W\right)\mathrm{RingHom}W\right)$$
5		rnrhmsubrg	$$⊢C\in \left(\mathrm{Scalar}\left(W\right)\mathrm{RingHom}W\right)\to \mathrm{ran}C\in \mathrm{SubRing}\left(W\right)$$
6	2 4 5	3syl	$$⊢\phi \to \mathrm{ran}C\in \mathrm{SubRing}\left(W\right)$$