Metamath Proof Explorer

Theorem subrdom

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

Ref Expression
Hypotheses subrdom.1 
|- ( ph -> R e. Domn )
subrdom.2 
|- ( ph -> S e. ( SubRing ` R ) )
Assertion subrdom 
|- ( ph -> ( R |`s S ) e. Domn )

Proof

Step Hyp Ref Expression
1 subrdom.1 
 |-  ( ph -> R e. Domn )
2 subrdom.2 
 |-  ( ph -> S e. ( SubRing ` R ) )
3 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
4 1 3 syl 
 |-  ( ph -> R e. NzRing )
5 eqid 
 |-  ( R |`s S ) = ( R |`s S )
6 5 subrgnzr 
 |-  ( ( R e. NzRing /\ S e. ( SubRing ` R ) ) -> ( R |`s S ) e. NzRing )
7 4 2 6 syl2anc 
 |-  ( ph -> ( R |`s S ) e. NzRing )
8 1 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( Base ` ( R |`s S ) ) ) /\ y e. ( Base ` ( R |`s S ) ) ) /\ ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) ) -> R e. Domn )
9 eqid 
 |-  ( Base ` R ) = ( Base ` R )
10 9 subrgss 
 |-  ( S e. ( SubRing ` R ) -> S C_ ( Base ` R ) )
11 2 10 syl 
 |-  ( ph -> S C_ ( Base ` R ) )
12 11 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( Base ` ( R |`s S ) ) ) /\ y e. ( Base ` ( R |`s S ) ) ) /\ ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) ) -> S C_ ( Base ` R ) )
13 simpllr 
 |-  ( ( ( ( ph /\ x e. ( Base ` ( R |`s S ) ) ) /\ y e. ( Base ` ( R |`s S ) ) ) /\ ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) ) -> x e. ( Base ` ( R |`s S ) ) )
14 5 9 ressbas2 
 |-  ( S C_ ( Base ` R ) -> S = ( Base ` ( R |`s S ) ) )
15 11 14 syl 
 |-  ( ph -> S = ( Base ` ( R |`s S ) ) )
16 15 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( Base ` ( R |`s S ) ) ) /\ y e. ( Base ` ( R |`s S ) ) ) /\ ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) ) -> S = ( Base ` ( R |`s S ) ) )
17 13 16 eleqtrrd 
 |-  ( ( ( ( ph /\ x e. ( Base ` ( R |`s S ) ) ) /\ y e. ( Base ` ( R |`s S ) ) ) /\ ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) ) -> x e. S )
18 12 17 sseldd 
 |-  ( ( ( ( ph /\ x e. ( Base ` ( R |`s S ) ) ) /\ y e. ( Base ` ( R |`s S ) ) ) /\ ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) ) -> x e. ( Base ` R ) )
19 simplr 
 |-  ( ( ( ( ph /\ x e. ( Base ` ( R |`s S ) ) ) /\ y e. ( Base ` ( R |`s S ) ) ) /\ ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) ) -> y e. ( Base ` ( R |`s S ) ) )
20 19 16 eleqtrrd 
 |-  ( ( ( ( ph /\ x e. ( Base ` ( R |`s S ) ) ) /\ y e. ( Base ` ( R |`s S ) ) ) /\ ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) ) -> y e. S )
21 12 20 sseldd 
 |-  ( ( ( ( ph /\ x e. ( Base ` ( R |`s S ) ) ) /\ y e. ( Base ` ( R |`s S ) ) ) /\ ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) ) -> y e. ( Base ` R ) )
22 simpr 
 |-  ( ( ( ( ph /\ x e. ( Base ` ( R |`s S ) ) ) /\ y e. ( Base ` ( R |`s S ) ) ) /\ ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) ) -> ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) )
23 2 elexd 
 |-  ( ph -> S e. _V )
24 eqid 
 |-  ( .r ` R ) = ( .r ` R )
25 5 24 ressmulr 
 |-  ( S e. _V -> ( .r ` R ) = ( .r ` ( R |`s S ) ) )
26 23 25 syl 
 |-  ( ph -> ( .r ` R ) = ( .r ` ( R |`s S ) ) )
27 26 oveqd 
 |-  ( ph -> ( x ( .r ` R ) y ) = ( x ( .r ` ( R |`s S ) ) y ) )
28 27 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( Base ` ( R |`s S ) ) ) /\ y e. ( Base ` ( R |`s S ) ) ) /\ ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) ) -> ( x ( .r ` R ) y ) = ( x ( .r ` ( R |`s S ) ) y ) )
29 subrgrcl 
 |-  ( S e. ( SubRing ` R ) -> R e. Ring )
30 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
31 2 29 30 3syl 
 |-  ( ph -> R e. Mnd )
32 subrgsubg 
 |-  ( S e. ( SubRing ` R ) -> S e. ( SubGrp ` R ) )
33 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
34 33 subg0cl 
 |-  ( S e. ( SubGrp ` R ) -> ( 0g ` R ) e. S )
35 2 32 34 3syl 
 |-  ( ph -> ( 0g ` R ) e. S )
36 5 9 33 ress0g 
 |-  ( ( R e. Mnd /\ ( 0g ` R ) e. S /\ S C_ ( Base ` R ) ) -> ( 0g ` R ) = ( 0g ` ( R |`s S ) ) )
37 31 35 11 36 syl3anc 
 |-  ( ph -> ( 0g ` R ) = ( 0g ` ( R |`s S ) ) )
38 37 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( Base ` ( R |`s S ) ) ) /\ y e. ( Base ` ( R |`s S ) ) ) /\ ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) ) -> ( 0g ` R ) = ( 0g ` ( R |`s S ) ) )
39 22 28 38 3eqtr4d 
 |-  ( ( ( ( ph /\ x e. ( Base ` ( R |`s S ) ) ) /\ y e. ( Base ` ( R |`s S ) ) ) /\ ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) ) -> ( x ( .r ` R ) y ) = ( 0g ` R ) )
40 9 24 33 domneq0 
 |-  ( ( R e. Domn /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( ( x ( .r ` R ) y ) = ( 0g ` R ) <-> ( x = ( 0g ` R ) \/ y = ( 0g ` R ) ) ) )
41 40 biimpa 
 |-  ( ( ( R e. Domn /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) = ( 0g ` R ) ) -> ( x = ( 0g ` R ) \/ y = ( 0g ` R ) ) )
42 8 18 21 39 41 syl31anc 
 |-  ( ( ( ( ph /\ x e. ( Base ` ( R |`s S ) ) ) /\ y e. ( Base ` ( R |`s S ) ) ) /\ ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) ) -> ( x = ( 0g ` R ) \/ y = ( 0g ` R ) ) )
43 38 eqeq2d 
 |-  ( ( ( ( ph /\ x e. ( Base ` ( R |`s S ) ) ) /\ y e. ( Base ` ( R |`s S ) ) ) /\ ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) ) -> ( x = ( 0g ` R ) <-> x = ( 0g ` ( R |`s S ) ) ) )
44 38 eqeq2d 
 |-  ( ( ( ( ph /\ x e. ( Base ` ( R |`s S ) ) ) /\ y e. ( Base ` ( R |`s S ) ) ) /\ ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) ) -> ( y = ( 0g ` R ) <-> y = ( 0g ` ( R |`s S ) ) ) )
45 43 44 orbi12d 
 |-  ( ( ( ( ph /\ x e. ( Base ` ( R |`s S ) ) ) /\ y e. ( Base ` ( R |`s S ) ) ) /\ ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) ) -> ( ( x = ( 0g ` R ) \/ y = ( 0g ` R ) ) <-> ( x = ( 0g ` ( R |`s S ) ) \/ y = ( 0g ` ( R |`s S ) ) ) ) )
46 42 45 mpbid 
 |-  ( ( ( ( ph /\ x e. ( Base ` ( R |`s S ) ) ) /\ y e. ( Base ` ( R |`s S ) ) ) /\ ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) ) -> ( x = ( 0g ` ( R |`s S ) ) \/ y = ( 0g ` ( R |`s S ) ) ) )
47 46 ex 
 |-  ( ( ( ph /\ x e. ( Base ` ( R |`s S ) ) ) /\ y e. ( Base ` ( R |`s S ) ) ) -> ( ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) -> ( x = ( 0g ` ( R |`s S ) ) \/ y = ( 0g ` ( R |`s S ) ) ) ) )
48 47 anasss 
 |-  ( ( ph /\ ( x e. ( Base ` ( R |`s S ) ) /\ y e. ( Base ` ( R |`s S ) ) ) ) -> ( ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) -> ( x = ( 0g ` ( R |`s S ) ) \/ y = ( 0g ` ( R |`s S ) ) ) ) )
49 48 ralrimivva 
 |-  ( ph -> A. x e. ( Base ` ( R |`s S ) ) A. y e. ( Base ` ( R |`s S ) ) ( ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) -> ( x = ( 0g ` ( R |`s S ) ) \/ y = ( 0g ` ( R |`s S ) ) ) ) )
50 eqid 
 |-  ( Base ` ( R |`s S ) ) = ( Base ` ( R |`s S ) )
51 eqid 
 |-  ( .r ` ( R |`s S ) ) = ( .r ` ( R |`s S ) )
52 eqid 
 |-  ( 0g ` ( R |`s S ) ) = ( 0g ` ( R |`s S ) )
53 50 51 52 isdomn 
 |-  ( ( R |`s S ) e. Domn <-> ( ( R |`s S ) e. NzRing /\ A. x e. ( Base ` ( R |`s S ) ) A. y e. ( Base ` ( R |`s S ) ) ( ( x ( .r ` ( R |`s S ) ) y ) = ( 0g ` ( R |`s S ) ) -> ( x = ( 0g ` ( R |`s S ) ) \/ y = ( 0g ` ( R |`s S ) ) ) ) ) )
54 7 49 53 sylanbrc 
 |-  ( ph -> ( R |`s S ) e. Domn )