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 = ( algSc ` W )
	rnasclsubrg.w	|- ( ph -> W e. AssAlg )
Assertion	rnasclsubrg	|- ( ph -> ran C e. ( SubRing ` W ) )

Proof

Step	Hyp	Ref	Expression
1		rnasclsubrg.c	|- C = ( algSc ` W )
2		rnasclsubrg.w	|- ( ph -> W e. AssAlg )
3		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
4	1 3	asclrhm	|- ( W e. AssAlg -> C e. ( ( Scalar ` W ) RingHom W ) )
5		rnrhmsubrg	|- ( C e. ( ( Scalar ` W ) RingHom W ) -> ran C e. ( SubRing ` W ) )
6	2 4 5	3syl	|- ( ph -> ran C e. ( SubRing ` W ) )