Metamath Proof Explorer

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 φ W AssAlg
Assertion rnasclsubrg φ ran C SubRing W


Step Hyp Ref Expression
1 rnasclsubrg.c C = algSc W
2 rnasclsubrg.w φ W AssAlg
3 eqid Scalar W = Scalar W
4 1 3 asclrhm W AssAlg C Scalar W RingHom W
5 rnrhmsubrg C Scalar W RingHom W ran C SubRing W
6 2 4 5 3syl φ ran C SubRing W