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	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
	subridom.2	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
Assertion	subridom	⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ IDomn )

Proof

Step	Hyp	Ref	Expression
1		subridom.1	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
2		subridom.2	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
3	1	idomcringd	⊢ ( 𝜑 → 𝑅 ∈ CRing )
4		eqid	⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
5	4	subrgcrng	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ) → ( 𝑅 ↾s 𝑆 ) ∈ CRing )
6	3 2 5	syl2anc	⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ CRing )
7	1	idomdomd	⊢ ( 𝜑 → 𝑅 ∈ Domn )
8	7 2	subrdom	⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ Domn )
9		isidom	⊢ ( ( 𝑅 ↾s 𝑆 ) ∈ IDomn ↔ ( ( 𝑅 ↾s 𝑆 ) ∈ CRing ∧ ( 𝑅 ↾s 𝑆 ) ∈ Domn ) )
10	6 8 9	sylanbrc	⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ IDomn )