Metamath Proof Explorer

Theorem ricdomn1

Description: A ring isomorphism maps a domain to a domain. (Contributed by Thierry Arnoux, 4-May-2026)

Ref Expression
Assertion ricdomn1 
|- ( ( R ~=r S /\ R e. Domn ) -> S e. Domn )

Proof

Step Hyp Ref Expression
1 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
2 ricnzr1 
 |-  ( ( R ~=r S /\ R e. NzRing ) -> S e. NzRing )
3 1 2 sylan2 
 |-  ( ( R ~=r S /\ R e. Domn ) -> S e. NzRing )
4 ricsym 
 |-  ( R ~=r S -> S ~=r R )
5 brric 
 |-  ( S ~=r R <-> ( S RingIso R ) =/= (/) )
6 4 5 sylib 
 |-  ( R ~=r S -> ( S RingIso R ) =/= (/) )
7 6 ad4antr 
 |-  ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) -> ( S RingIso R ) =/= (/) )
8 simpr 
 |-  ( ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) /\ ( f ` x ) = ( 0g ` R ) ) -> ( f ` x ) = ( 0g ` R ) )
9 8 fveq2d 
 |-  ( ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) /\ ( f ` x ) = ( 0g ` R ) ) -> ( `' f ` ( f ` x ) ) = ( `' f ` ( 0g ` R ) ) )
10 eqid 
 |-  ( Base ` S ) = ( Base ` S )
11 eqid 
 |-  ( Base ` R ) = ( Base ` R )
12 10 11 rimf1o 
 |-  ( f e. ( S RingIso R ) -> f : ( Base ` S ) -1-1-onto-> ( Base ` R ) )
13 12 ad2antlr 
 |-  ( ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) /\ ( f ` x ) = ( 0g ` R ) ) -> f : ( Base ` S ) -1-1-onto-> ( Base ` R ) )
14 simp-4r 
 |-  ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) -> x e. ( Base ` S ) )
15 14 adantr 
 |-  ( ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) /\ ( f ` x ) = ( 0g ` R ) ) -> x e. ( Base ` S ) )
16 f1ocnvfv1 
 |-  ( ( f : ( Base ` S ) -1-1-onto-> ( Base ` R ) /\ x e. ( Base ` S ) ) -> ( `' f ` ( f ` x ) ) = x )
17 13 15 16 syl2anc 
 |-  ( ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) /\ ( f ` x ) = ( 0g ` R ) ) -> ( `' f ` ( f ` x ) ) = x )
18 isrim0 
 |-  ( f e. ( S RingIso R ) <-> ( f e. ( S RingHom R ) /\ `' f e. ( R RingHom S ) ) )
19 18 simprbi 
 |-  ( f e. ( S RingIso R ) -> `' f e. ( R RingHom S ) )
20 19 ad2antlr 
 |-  ( ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) /\ ( f ` x ) = ( 0g ` R ) ) -> `' f e. ( R RingHom S ) )
21 rhmghm 
 |-  ( `' f e. ( R RingHom S ) -> `' f e. ( R GrpHom S ) )
22 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
23 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
24 22 23 ghmid 
 |-  ( `' f e. ( R GrpHom S ) -> ( `' f ` ( 0g ` R ) ) = ( 0g ` S ) )
25 20 21 24 3syl 
 |-  ( ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) /\ ( f ` x ) = ( 0g ` R ) ) -> ( `' f ` ( 0g ` R ) ) = ( 0g ` S ) )
26 9 17 25 3eqtr3d 
 |-  ( ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) /\ ( f ` x ) = ( 0g ` R ) ) -> x = ( 0g ` S ) )
27 simpr 
 |-  ( ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) /\ ( f ` y ) = ( 0g ` R ) ) -> ( f ` y ) = ( 0g ` R ) )
28 27 fveq2d 
 |-  ( ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) /\ ( f ` y ) = ( 0g ` R ) ) -> ( `' f ` ( f ` y ) ) = ( `' f ` ( 0g ` R ) ) )
29 12 ad2antlr 
 |-  ( ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) /\ ( f ` y ) = ( 0g ` R ) ) -> f : ( Base ` S ) -1-1-onto-> ( Base ` R ) )
30 simpllr 
 |-  ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) -> y e. ( Base ` S ) )
31 30 adantr 
 |-  ( ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) /\ ( f ` y ) = ( 0g ` R ) ) -> y e. ( Base ` S ) )
32 f1ocnvfv1 
 |-  ( ( f : ( Base ` S ) -1-1-onto-> ( Base ` R ) /\ y e. ( Base ` S ) ) -> ( `' f ` ( f ` y ) ) = y )
33 29 31 32 syl2anc 
 |-  ( ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) /\ ( f ` y ) = ( 0g ` R ) ) -> ( `' f ` ( f ` y ) ) = y )
34 19 ad2antlr 
 |-  ( ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) /\ ( f ` y ) = ( 0g ` R ) ) -> `' f e. ( R RingHom S ) )
35 34 21 24 3syl 
 |-  ( ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) /\ ( f ` y ) = ( 0g ` R ) ) -> ( `' f ` ( 0g ` R ) ) = ( 0g ` S ) )
36 28 33 35 3eqtr3d 
 |-  ( ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) /\ ( f ` y ) = ( 0g ` R ) ) -> y = ( 0g ` S ) )
37 simp-5r 
 |-  ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) -> R e. Domn )
38 rimrhm 
 |-  ( f e. ( S RingIso R ) -> f e. ( S RingHom R ) )
39 10 11 rhmf 
 |-  ( f e. ( S RingHom R ) -> f : ( Base ` S ) --> ( Base ` R ) )
40 38 39 syl 
 |-  ( f e. ( S RingIso R ) -> f : ( Base ` S ) --> ( Base ` R ) )
41 40 adantl 
 |-  ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) -> f : ( Base ` S ) --> ( Base ` R ) )
42 41 14 ffvelcdmd 
 |-  ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) -> ( f ` x ) e. ( Base ` R ) )
43 41 30 ffvelcdmd 
 |-  ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) -> ( f ` y ) e. ( Base ` R ) )
44 simplr 
 |-  ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) -> ( x ( .r ` S ) y ) = ( 0g ` S ) )
45 44 fveq2d 
 |-  ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) -> ( f ` ( x ( .r ` S ) y ) ) = ( f ` ( 0g ` S ) ) )
46 38 adantl 
 |-  ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) -> f e. ( S RingHom R ) )
47 eqid 
 |-  ( .r ` S ) = ( .r ` S )
48 eqid 
 |-  ( .r ` R ) = ( .r ` R )
49 10 47 48 rhmmul 
 |-  ( ( f e. ( S RingHom R ) /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( f ` ( x ( .r ` S ) y ) ) = ( ( f ` x ) ( .r ` R ) ( f ` y ) ) )
50 46 14 30 49 syl3anc 
 |-  ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) -> ( f ` ( x ( .r ` S ) y ) ) = ( ( f ` x ) ( .r ` R ) ( f ` y ) ) )
51 rhmghm 
 |-  ( f e. ( S RingHom R ) -> f e. ( S GrpHom R ) )
52 23 22 ghmid 
 |-  ( f e. ( S GrpHom R ) -> ( f ` ( 0g ` S ) ) = ( 0g ` R ) )
53 46 51 52 3syl 
 |-  ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) -> ( f ` ( 0g ` S ) ) = ( 0g ` R ) )
54 45 50 53 3eqtr3d 
 |-  ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) -> ( ( f ` x ) ( .r ` R ) ( f ` y ) ) = ( 0g ` R ) )
55 11 48 22 domneq0 
 |-  ( ( R e. Domn /\ ( f ` x ) e. ( Base ` R ) /\ ( f ` y ) e. ( Base ` R ) ) -> ( ( ( f ` x ) ( .r ` R ) ( f ` y ) ) = ( 0g ` R ) <-> ( ( f ` x ) = ( 0g ` R ) \/ ( f ` y ) = ( 0g ` R ) ) ) )
56 55 biimpa 
 |-  ( ( ( R e. Domn /\ ( f ` x ) e. ( Base ` R ) /\ ( f ` y ) e. ( Base ` R ) ) /\ ( ( f ` x ) ( .r ` R ) ( f ` y ) ) = ( 0g ` R ) ) -> ( ( f ` x ) = ( 0g ` R ) \/ ( f ` y ) = ( 0g ` R ) ) )
57 37 42 43 54 56 syl31anc 
 |-  ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) -> ( ( f ` x ) = ( 0g ` R ) \/ ( f ` y ) = ( 0g ` R ) ) )
58 26 36 57 orim12da 
 |-  ( ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) /\ f e. ( S RingIso R ) ) -> ( x = ( 0g ` S ) \/ y = ( 0g ` S ) ) )
59 7 58 n0limd 
 |-  ( ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) /\ ( x ( .r ` S ) y ) = ( 0g ` S ) ) -> ( x = ( 0g ` S ) \/ y = ( 0g ` S ) ) )
60 59 ex 
 |-  ( ( ( ( R ~=r S /\ R e. Domn ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) -> ( ( x ( .r ` S ) y ) = ( 0g ` S ) -> ( x = ( 0g ` S ) \/ y = ( 0g ` S ) ) ) )
61 60 anasss 
 |-  ( ( ( R ~=r S /\ R e. Domn ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( ( x ( .r ` S ) y ) = ( 0g ` S ) -> ( x = ( 0g ` S ) \/ y = ( 0g ` S ) ) ) )
62 61 ralrimivva 
 |-  ( ( R ~=r S /\ R e. Domn ) -> A. x e. ( Base ` S ) A. y e. ( Base ` S ) ( ( x ( .r ` S ) y ) = ( 0g ` S ) -> ( x = ( 0g ` S ) \/ y = ( 0g ` S ) ) ) )
63 10 47 23 isdomn 
 |-  ( S e. Domn <-> ( S e. NzRing /\ A. x e. ( Base ` S ) A. y e. ( Base ` S ) ( ( x ( .r ` S ) y ) = ( 0g ` S ) -> ( x = ( 0g ` S ) \/ y = ( 0g ` S ) ) ) ) )
64 3 62 63 sylanbrc 
 |-  ( ( R ~=r S /\ R e. Domn ) -> S e. Domn )