subridom

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

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

Metamath Proof Explorer