Theorem subrgccdom

Description: A subring of the complex numbers is a 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	subrgccdom	$$⊢R\in \mathrm{Domn}$$

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	subrgccnzr	$$⊢R\in \mathrm{NzRing}$$
4		subrgccsscc	$$⊢S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to S\subseteq ℂ$$
5	2 4	ax-mp	$$⊢S\subseteq ℂ$$
6	5	sseli	$$⊢x\in S\to x\in ℂ$$
7	5	sseli	$$⊢y\in S\to y\in ℂ$$
8		mul0or	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to \left(xy=0\leftrightarrow \left(x=0\vee y=0\right)\right)$$
9	6 7 8	syl2an	$$⊢\left(x\in S\wedge y\in S\right)\to \left(xy=0\leftrightarrow \left(x=0\vee y=0\right)\right)$$
10	9	biimpd	$$⊢\left(x\in S\wedge y\in S\right)\to \left(xy=0\to \left(x=0\vee y=0\right)\right)$$
11	10	rgen2	$$⊢\forall x\in S\forall y\in S\left(xy=0\to \left(x=0\vee y=0\right)\right)$$
12	1	cnfldsrngbas	$$⊢S\subseteq ℂ\to S={\mathrm{Base}}_R$$
13	5 12	ax-mp	$$⊢S={\mathrm{Base}}_R$$
14		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}S={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}S$$
15	14	cnfldsrngmul	$$⊢S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to \times ={\cdot }_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}S\right)}$$
16	2 15	ax-mp	$$⊢\times ={\cdot }_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}S\right)}$$
17	1	fveq2i	$$⊢{\cdot }_R={\cdot }_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}S\right)}$$
18	16 17	eqtr4i	$$⊢\times ={\cdot }_R$$
19	1 2	subrgcccrng0	$$⊢0=0_R$$
20	13 18 19	isdomn	$$⊢R\in \mathrm{Domn}\leftrightarrow \left(R\in \mathrm{NzRing}\wedge \forall x\in S\forall y\in S\left(xy=0\to \left(x=0\vee y=0\right)\right)\right)$$
21	3 11 20	mpbir2an	$$⊢R\in \mathrm{Domn}$$