ricdomn1

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

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

Proof

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

Metamath Proof Explorer

Theorem ricdomn1

Proof