Theorem subridom

Description: A subring of an integral domain is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	subridom.1	$$⊢\phi \to R\in \mathrm{IDomn}$$
	subridom.2	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
Assertion	subridom	$$⊢\phi \to R{\upharpoonright }_{𝑠}S\in \mathrm{IDomn}$$

Proof

Step	Hyp	Ref	Expression
1		subridom.1	$$⊢\phi \to R\in \mathrm{IDomn}$$
2		subridom.2	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
3	1	idomcringd	$$⊢\phi \to R\in \mathrm{CRing}$$
4		eqid	$$⊢R{\upharpoonright }_{𝑠}S=R{\upharpoonright }_{𝑠}S$$
5	4	subrgcrng	$$⊢\left(R\in \mathrm{CRing}\wedge S\in \mathrm{SubRing}\left(R\right)\right)\to R{\upharpoonright }_{𝑠}S\in \mathrm{CRing}$$
6	3 2 5	syl2anc	$$⊢\phi \to R{\upharpoonright }_{𝑠}S\in \mathrm{CRing}$$
7	1	idomdomd	$$⊢\phi \to R\in \mathrm{Domn}$$
8	7 2	subrdom	$$⊢\phi \to R{\upharpoonright }_{𝑠}S\in \mathrm{Domn}$$
9		isidom	$$⊢R{\upharpoonright }_{𝑠}S\in \mathrm{IDomn}\leftrightarrow \left(R{\upharpoonright }_{𝑠}S\in \mathrm{CRing}\wedge R{\upharpoonright }_{𝑠}S\in \mathrm{Domn}\right)$$
10	6 8 9	sylanbrc	$$⊢\phi \to R{\upharpoonright }_{𝑠}S\in \mathrm{IDomn}$$