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	⊢ 𝐶 = ( algSc ‘ 𝑊 )
	rnasclsubrg.w	⊢ ( 𝜑 → 𝑊 ∈ AssAlg )
Assertion	rnasclsubrg	⊢ ( 𝜑 → ran 𝐶 ∈ ( SubRing ‘ 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		rnasclsubrg.c	⊢ 𝐶 = ( algSc ‘ 𝑊 )
2		rnasclsubrg.w	⊢ ( 𝜑 → 𝑊 ∈ AssAlg )
3		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
4	1 3	asclrhm	⊢ ( 𝑊 ∈ AssAlg → 𝐶 ∈ ( ( Scalar ‘ 𝑊 ) RingHom 𝑊 ) )
5		rnrhmsubrg	⊢ ( 𝐶 ∈ ( ( Scalar ‘ 𝑊 ) RingHom 𝑊 ) → ran 𝐶 ∈ ( SubRing ‘ 𝑊 ) )
6	2 4 5	3syl	⊢ ( 𝜑 → ran 𝐶 ∈ ( SubRing ‘ 𝑊 ) )