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

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 ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) → 𝑆 ∈ Domn )

Proof

Step Hyp Ref Expression
1 domnnzr ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
2 ricnzr1 ⊢ ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ NzRing ) → 𝑆 ∈ NzRing )
3 1 2 sylan2 ⊢ ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) → 𝑆 ∈ NzRing )
4 ricsym ⊢ ( 𝑅 ≃𝑟 𝑆 → 𝑆 ≃𝑟 𝑅 )
5 brric ⊢ ( 𝑆 ≃𝑟 𝑅 ↔ ( 𝑆 RingIso 𝑅 ) ≠ ∅ )
6 4 5 sylib ⊢ ( 𝑅 ≃𝑟 𝑆 → ( 𝑆 RingIso 𝑅 ) ≠ ∅ )
7 6 ad4antr ⊢ ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) → ( 𝑆 RingIso 𝑅 ) ≠ ∅ )
8 simpr ⊢ ( ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) ∧ ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) )
9 8 fveq2d ⊢ ( ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) ∧ ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) → ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑥 ) ) = ( ◡ 𝑓 ‘ ( 0g ‘ 𝑅 ) ) )
10 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
11 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
12 10 11 rimf1o ⊢ ( 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) → 𝑓 : ( Base ‘ 𝑆 ) –1-1-onto→ ( Base ‘ 𝑅 ) )
13 12 ad2antlr ⊢ ( ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) ∧ ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) → 𝑓 : ( Base ‘ 𝑆 ) –1-1-onto→ ( Base ‘ 𝑅 ) )
14 simp-4r ⊢ ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
15 14 adantr ⊢ ( ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) ∧ ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
16 f1ocnvfv1 ⊢ ( ( 𝑓 : ( Base ‘ 𝑆 ) –1-1-onto→ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 )
17 13 15 16 syl2anc ⊢ ( ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) ∧ ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) → ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 )
18 isrim0 ⊢ ( 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ↔ ( 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) ∧ ◡ 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) ) )
19 18 simprbi ⊢ ( 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) → ◡ 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) )
20 19 ad2antlr ⊢ ( ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) ∧ ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) → ◡ 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) )
21 rhmghm ⊢ ( ◡ 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) → ◡ 𝑓 ∈ ( 𝑅 GrpHom 𝑆 ) )
22 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
23 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
24 22 23 ghmid ⊢ ( ◡ 𝑓 ∈ ( 𝑅 GrpHom 𝑆 ) → ( ◡ 𝑓 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) )
25 20 21 24 3syl ⊢ ( ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) ∧ ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) → ( ◡ 𝑓 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) )
26 9 17 25 3eqtr3d ⊢ ( ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) ∧ ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) → 𝑥 = ( 0g ‘ 𝑆 ) )
27 simpr ⊢ ( ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) ∧ ( 𝑓 ‘ 𝑦 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑓 ‘ 𝑦 ) = ( 0g ‘ 𝑅 ) )
28 27 fveq2d ⊢ ( ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) ∧ ( 𝑓 ‘ 𝑦 ) = ( 0g ‘ 𝑅 ) ) → ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑦 ) ) = ( ◡ 𝑓 ‘ ( 0g ‘ 𝑅 ) ) )
29 12 ad2antlr ⊢ ( ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) ∧ ( 𝑓 ‘ 𝑦 ) = ( 0g ‘ 𝑅 ) ) → 𝑓 : ( Base ‘ 𝑆 ) –1-1-onto→ ( Base ‘ 𝑅 ) )
30 simpllr ⊢ ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) )
31 30 adantr ⊢ ( ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) ∧ ( 𝑓 ‘ 𝑦 ) = ( 0g ‘ 𝑅 ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) )
32 f1ocnvfv1 ⊢ ( ( 𝑓 : ( Base ‘ 𝑆 ) –1-1-onto→ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑦 ) ) = 𝑦 )
33 29 31 32 syl2anc ⊢ ( ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) ∧ ( 𝑓 ‘ 𝑦 ) = ( 0g ‘ 𝑅 ) ) → ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑦 ) ) = 𝑦 )
34 19 ad2antlr ⊢ ( ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) ∧ ( 𝑓 ‘ 𝑦 ) = ( 0g ‘ 𝑅 ) ) → ◡ 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) )
35 34 21 24 3syl ⊢ ( ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) ∧ ( 𝑓 ‘ 𝑦 ) = ( 0g ‘ 𝑅 ) ) → ( ◡ 𝑓 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) )
36 28 33 35 3eqtr3d ⊢ ( ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) ∧ ( 𝑓 ‘ 𝑦 ) = ( 0g ‘ 𝑅 ) ) → 𝑦 = ( 0g ‘ 𝑆 ) )
37 simp-5r ⊢ ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) → 𝑅 ∈ Domn )
38 rimrhm ⊢ ( 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) → 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) )
39 10 11 rhmf ⊢ ( 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) → 𝑓 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑅 ) )
40 38 39 syl ⊢ ( 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) → 𝑓 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑅 ) )
41 40 adantl ⊢ ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) → 𝑓 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑅 ) )
42 41 14 ffvelcdmd ⊢ ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
43 41 30 ffvelcdmd ⊢ ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) → ( 𝑓 ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
44 simplr ⊢ ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) )
45 44 fveq2d ⊢ ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) → ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) ) = ( 𝑓 ‘ ( 0g ‘ 𝑆 ) ) )
46 38 adantl ⊢ ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) → 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) )
47 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
48 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
49 10 47 48 rhmmul ⊢ ( ( 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑓 ‘ 𝑦 ) ) )
50 46 14 30 49 syl3anc ⊢ ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) → ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑓 ‘ 𝑦 ) ) )
51 rhmghm ⊢ ( 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) → 𝑓 ∈ ( 𝑆 GrpHom 𝑅 ) )
52 23 22 ghmid ⊢ ( 𝑓 ∈ ( 𝑆 GrpHom 𝑅 ) → ( 𝑓 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑅 ) )
53 46 51 52 3syl ⊢ ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) → ( 𝑓 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑅 ) )
54 45 50 53 3eqtr3d ⊢ ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) → ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑓 ‘ 𝑦 ) ) = ( 0g ‘ 𝑅 ) )
55 11 48 22 domneq0 ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑓 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑓 ‘ 𝑦 ) ) = ( 0g ‘ 𝑅 ) ↔ ( ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∨ ( 𝑓 ‘ 𝑦 ) = ( 0g ‘ 𝑅 ) ) ) )
56 55 biimpa ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑓 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) ∧ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑓 ‘ 𝑦 ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∨ ( 𝑓 ‘ 𝑦 ) = ( 0g ‘ 𝑅 ) ) )
57 37 42 43 54 56 syl31anc ⊢ ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) → ( ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∨ ( 𝑓 ‘ 𝑦 ) = ( 0g ‘ 𝑅 ) ) )
58 26 36 57 orim12da ⊢ ( ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) ) → ( 𝑥 = ( 0g ‘ 𝑆 ) ∨ 𝑦 = ( 0g ‘ 𝑆 ) ) )
59 7 58 n0limd ⊢ ( ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) ) → ( 𝑥 = ( 0g ‘ 𝑆 ) ∨ 𝑦 = ( 0g ‘ 𝑆 ) ) )
60 59 ex ⊢ ( ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) → ( 𝑥 = ( 0g ‘ 𝑆 ) ∨ 𝑦 = ( 0g ‘ 𝑆 ) ) ) )
61 60 anasss ⊢ ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) → ( 𝑥 = ( 0g ‘ 𝑆 ) ∨ 𝑦 = ( 0g ‘ 𝑆 ) ) ) )
62 61 ralrimivva ⊢ ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) → ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) → ( 𝑥 = ( 0g ‘ 𝑆 ) ∨ 𝑦 = ( 0g ‘ 𝑆 ) ) ) )
63 10 47 23 isdomn ⊢ ( 𝑆 ∈ Domn ↔ ( 𝑆 ∈ NzRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 0g ‘ 𝑆 ) → ( 𝑥 = ( 0g ‘ 𝑆 ) ∨ 𝑦 = ( 0g ‘ 𝑆 ) ) ) ) )
64 3 62 63 sylanbrc ⊢ ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) → 𝑆 ∈ Domn )