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

Metamath Proof Explorer

Theorem ricnzr1

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

Ref Expression
Assertion ricnzr1 ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ NzRing ) → 𝑆 ∈ NzRing )

Proof

Step Hyp Ref Expression
1 brric ⊢ ( 𝑅 ≃𝑟 𝑆 ↔ ( 𝑅 RingIso 𝑆 ) ≠ ∅ )
2 1 biimpi ⊢ ( 𝑅 ≃𝑟 𝑆 → ( 𝑅 RingIso 𝑆 ) ≠ ∅ )
3 2 adantr ⊢ ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ NzRing ) → ( 𝑅 RingIso 𝑆 ) ≠ ∅ )
4 rimrcl2 ⊢ ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → 𝑆 ∈ Ring )
5 4 adantl ⊢ ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ NzRing ) ∧ 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ) → 𝑆 ∈ Ring )
6 3 5 n0limd ⊢ ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ NzRing ) → 𝑆 ∈ Ring )
7 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
8 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
9 7 8 nzrnz ⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
10 9 ad2antlr ⊢ ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ NzRing ) ∧ 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ) → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
11 isrim0 ⊢ ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ↔ ( 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ◡ 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) ) )
12 11 simprbi ⊢ ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → ◡ 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) )
13 12 adantl ⊢ ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ NzRing ) ∧ 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ) → ◡ 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) )
14 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
15 14 7 rhm1 ⊢ ( ◡ 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) → ( ◡ 𝑓 ‘ ( 1r ‘ 𝑆 ) ) = ( 1r ‘ 𝑅 ) )
16 13 15 syl ⊢ ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ NzRing ) ∧ 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ) → ( ◡ 𝑓 ‘ ( 1r ‘ 𝑆 ) ) = ( 1r ‘ 𝑅 ) )
17 rhmghm ⊢ ( ◡ 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) → ◡ 𝑓 ∈ ( 𝑆 GrpHom 𝑅 ) )
18 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
19 18 8 ghmid ⊢ ( ◡ 𝑓 ∈ ( 𝑆 GrpHom 𝑅 ) → ( ◡ 𝑓 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑅 ) )
20 13 17 19 3syl ⊢ ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ NzRing ) ∧ 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ) → ( ◡ 𝑓 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑅 ) )
21 10 16 20 3netr4d ⊢ ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ NzRing ) ∧ 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ) → ( ◡ 𝑓 ‘ ( 1r ‘ 𝑆 ) ) ≠ ( ◡ 𝑓 ‘ ( 0g ‘ 𝑆 ) ) )
22 fveq2 ⊢ ( ( 1r ‘ 𝑆 ) = ( 0g ‘ 𝑆 ) → ( ◡ 𝑓 ‘ ( 1r ‘ 𝑆 ) ) = ( ◡ 𝑓 ‘ ( 0g ‘ 𝑆 ) ) )
23 22 necon3i ⊢ ( ( ◡ 𝑓 ‘ ( 1r ‘ 𝑆 ) ) ≠ ( ◡ 𝑓 ‘ ( 0g ‘ 𝑆 ) ) → ( 1r ‘ 𝑆 ) ≠ ( 0g ‘ 𝑆 ) )
24 21 23 syl ⊢ ( ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ NzRing ) ∧ 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ) → ( 1r ‘ 𝑆 ) ≠ ( 0g ‘ 𝑆 ) )
25 3 24 n0limd ⊢ ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ NzRing ) → ( 1r ‘ 𝑆 ) ≠ ( 0g ‘ 𝑆 ) )
26 14 18 isnzr ⊢ ( 𝑆 ∈ NzRing ↔ ( 𝑆 ∈ Ring ∧ ( 1r ‘ 𝑆 ) ≠ ( 0g ‘ 𝑆 ) ) )
27 6 25 26 sylanbrc ⊢ ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ NzRing ) → 𝑆 ∈ NzRing )