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 )