ricnzr1

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

		Ref	Expression
	Assertion	ricnzr1	$⊢ (R ≃_{𝑟} S \land R \in NzRing) \to S \in NzRing$

Proof

Step	Hyp	Ref	Expression
1		brric	$⊢ R ≃_{𝑟} S \leftrightarrow R RingIso S \neq \emptyset$
2	1	biimpi	$⊢ R ≃_{𝑟} S \to R RingIso S \neq \emptyset$
3	2	adantr	$⊢ (R ≃_{𝑟} S \land R \in NzRing) \to R RingIso S \neq \emptyset$
4		rimrcl2	$⊢ f \in (R RingIso S) \to S \in Ring$
5	4	adantl	$⊢ ((R ≃_{𝑟} S \land R \in NzRing) \land f \in (R RingIso S)) \to S \in Ring$
6	3 5	n0limd	$⊢ (R ≃_{𝑟} S \land R \in NzRing) \to S \in Ring$
7		eqid	$⊢ 1_{R} = 1_{R}$
8		eqid	$⊢ 0_{R} = 0_{R}$
9	7 8	nzrnz	$⊢ R \in NzRing \to 1_{R} \neq 0_{R}$
10	9	ad2antlr	$⊢ ((R ≃_{𝑟} S \land R \in NzRing) \land f \in (R RingIso S)) \to 1_{R} \neq 0_{R}$
11		isrim0	$⊢ f \in (R RingIso S) \leftrightarrow (f \in (R RingHom S) \land f^{-1} \in (S RingHom R))$
12	11	simprbi	$⊢ f \in (R RingIso S) \to f^{-1} \in (S RingHom R)$
13	12	adantl	$⊢ ((R ≃_{𝑟} S \land R \in NzRing) \land f \in (R RingIso S)) \to f^{-1} \in (S RingHom R)$
14		eqid	$⊢ 1_{S} = 1_{S}$
15	14 7	rhm1	$⊢ f^{-1} \in (S RingHom R) \to f^{-1} (1_{S}) = 1_{R}$
16	13 15	syl	$⊢ ((R ≃_{𝑟} S \land R \in NzRing) \land f \in (R RingIso S)) \to f^{-1} (1_{S}) = 1_{R}$
17		rhmghm	$⊢ f^{-1} \in (S RingHom R) \to f^{-1} \in (S GrpHom R)$
18		eqid	$⊢ 0_{S} = 0_{S}$
19	18 8	ghmid	$⊢ f^{-1} \in (S GrpHom R) \to f^{-1} (0_{S}) = 0_{R}$
20	13 17 19	3syl	$⊢ ((R ≃_{𝑟} S \land R \in NzRing) \land f \in (R RingIso S)) \to f^{-1} (0_{S}) = 0_{R}$
21	10 16 20	3netr4d	$⊢ ((R ≃_{𝑟} S \land R \in NzRing) \land f \in (R RingIso S)) \to f^{-1} (1_{S}) \neq f^{-1} (0_{S})$
22		fveq2	$⊢ 1_{S} = 0_{S} \to f^{-1} (1_{S}) = f^{-1} (0_{S})$
23	22	necon3i	$⊢ f^{-1} (1_{S}) \neq f^{-1} (0_{S}) \to 1_{S} \neq 0_{S}$
24	21 23	syl	$⊢ ((R ≃_{𝑟} S \land R \in NzRing) \land f \in (R RingIso S)) \to 1_{S} \neq 0_{S}$
25	3 24	n0limd	$⊢ (R ≃_{𝑟} S \land R \in NzRing) \to 1_{S} \neq 0_{S}$
26	14 18	isnzr	$⊢ S \in NzRing \leftrightarrow (S \in Ring \land 1_{S} \neq 0_{S})$
27	6 25 26	sylanbrc	$⊢ (R ≃_{𝑟} S \land R \in NzRing) \to S \in NzRing$

Metamath Proof Explorer

Theorem ricnzr1

Proof