This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )