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	|- ( ph -> R e. IDomn )
	subridom.2	|- ( ph -> S e. ( SubRing ` R ) )
Assertion	subridom	|- ( ph -> ( R |`s S ) e. IDomn )

Proof

Step	Hyp	Ref	Expression
1		subridom.1	|- ( ph -> R e. IDomn )
2		subridom.2	|- ( ph -> S e. ( SubRing ` R ) )
3	1	idomcringd	|- ( ph -> R e. CRing )
4		eqid	|- ( R |`s S ) = ( R |`s S )
5	4	subrgcrng	|- ( ( R e. CRing /\ S e. ( SubRing ` R ) ) -> ( R |`s S ) e. CRing )
6	3 2 5	syl2anc	|- ( ph -> ( R |`s S ) e. CRing )
7	1	idomdomd	|- ( ph -> R e. Domn )
8	7 2	subrdom	|- ( ph -> ( R |`s S ) e. Domn )
9		isidom	|- ( ( R |`s S ) e. IDomn <-> ( ( R |`s S ) e. CRing /\ ( R |`s S ) e. Domn ) )
10	6 8 9	sylanbrc	|- ( ph -> ( R |`s S ) e. IDomn )