Theorem subrgccidom

Description: A subring of the complex numbers is an integral domain. (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	subrgccidom	$$⊢R\in \mathrm{IDomn}$$

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	1 2	subrgcccrng	$$⊢R\in \mathrm{CRing}$$
4	1 2	subrgccdom	$$⊢R\in \mathrm{Domn}$$
5		isidom	$$⊢R\in \mathrm{IDomn}\leftrightarrow \left(R\in \mathrm{CRing}\wedge R\in \mathrm{Domn}\right)$$
6	3 4 5	mpbir2an	$$⊢R\in \mathrm{IDomn}$$