Theorem subrgcccrng

Description: A subring of the complex numbers is a commutative ring. (Contributed by AV, 26-Oct-2026)

	Ref	Expression
Hypotheses	subrgcccrng.r	$$⊢R={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}S$$
	subrgcccrng.s	$$⊢S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	subrgcccrng	$$⊢R\in \mathrm{CRing}$$

Proof

Step	Hyp	Ref	Expression
1		subrgcccrng.r	$$⊢R={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}S$$
2		subrgcccrng.s	$$⊢S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
3		cncrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CRing}$$
4	1	subrgcrng	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{CRing}\wedge S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)\to R\in \mathrm{CRing}$$
5	3 2 4	mp2an	$$⊢R\in \mathrm{CRing}$$