crngrhmfo

Description: The image of a surjective homomorphism from a commutative ring is commutative. (Contributed by Jeff Madsen, 4-Jan-2011) (Revised by AV, 19-Jul-2026)

		Ref	Expression
	Hypothesis	crngrhmfo.b	$⊢ B = {Base}_{S}$
	Assertion	crngrhmfo	$⊢ (R \in CRing \land F \in (R RingHom S) \land F : dom F \underset{onto}{⟶} B) \to S \in CRing$

Proof

Step	Hyp	Ref	Expression
1		crngrhmfo.b	$⊢ B = {Base}_{S}$
2		rhmrcl2	$⊢ F \in (R RingHom S) \to S \in Ring$
3	2	3ad2ant2	$⊢ (R \in CRing \land F \in (R RingHom S) \land F : dom F \underset{onto}{⟶} B) \to S \in Ring$
4		foelrn	$⊢ (F : dom F \underset{onto}{⟶} B \land x \in B) \to \exists a \in dom F x = F (a)$
5	4	ex	$⊢ F : dom F \underset{onto}{⟶} B \to (x \in B \to \exists a \in dom F x = F (a))$
6		foelrn	$⊢ (F : dom F \underset{onto}{⟶} B \land y \in B) \to \exists b \in dom F y = F (b)$
7	6	ex	$⊢ F : dom F \underset{onto}{⟶} B \to (y \in B \to \exists b \in dom F y = F (b))$
8	5 7	anim12d	$⊢ F : dom F \underset{onto}{⟶} B \to ((x \in B \land y \in B) \to (\exists a \in dom F x = F (a) \land \exists b \in dom F y = F (b)))$
9		reeanv	$⊢ \exists a \in dom F \exists b \in dom F (x = F (a) \land y = F (b)) \leftrightarrow (\exists a \in dom F x = F (a) \land \exists b \in dom F y = F (b))$
10	8 9	imbitrrdi	$⊢ F : dom F \underset{onto}{⟶} B \to ((x \in B \land y \in B) \to \exists a \in dom F \exists b \in dom F (x = F (a) \land y = F (b)))$
11	10	3ad2ant3	$⊢ (R \in CRing \land F \in (R RingHom S) \land F : dom F \underset{onto}{⟶} B) \to ((x \in B \land y \in B) \to \exists a \in dom F \exists b \in dom F (x = F (a) \land y = F (b)))$
12		simpll	$⊢ ((R \in CRing \land F \in (R RingHom S)) \land (a \in dom F \land b \in dom F)) \to R \in CRing$
13		eqid	$⊢ {Base}_{R} = {Base}_{R}$
14		eqid	$⊢ {Base}_{S} = {Base}_{S}$
15	13 14	rhmf	$⊢ F \in (R RingHom S) \to F : {Base}_{R} ⟶ {Base}_{S}$
16	15	fdmd	$⊢ F \in (R RingHom S) \to dom F = {Base}_{R}$
17	16	eleq2d	$⊢ F \in (R RingHom S) \to (a \in dom F \leftrightarrow a \in {Base}_{R})$
18	16	eleq2d	$⊢ F \in (R RingHom S) \to (b \in dom F \leftrightarrow b \in {Base}_{R})$
19	17 18	anbi12d	$⊢ F \in (R RingHom S) \to ((a \in dom F \land b \in dom F) \leftrightarrow (a \in {Base}_{R} \land b \in {Base}_{R}))$
20	19	biimpd	$⊢ F \in (R RingHom S) \to ((a \in dom F \land b \in dom F) \to (a \in {Base}_{R} \land b \in {Base}_{R}))$
21	20	adantl	$⊢ (R \in CRing \land F \in (R RingHom S)) \to ((a \in dom F \land b \in dom F) \to (a \in {Base}_{R} \land b \in {Base}_{R}))$
22	21	imp	$⊢ ((R \in CRing \land F \in (R RingHom S)) \land (a \in dom F \land b \in dom F)) \to (a \in {Base}_{R} \land b \in {Base}_{R})$
23		3anass	$⊢ (R \in CRing \land a \in {Base}_{R} \land b \in {Base}_{R}) \leftrightarrow (R \in CRing \land (a \in {Base}_{R} \land b \in {Base}_{R}))$
24	12 22 23	sylanbrc	$⊢ ((R \in CRing \land F \in (R RingHom S)) \land (a \in dom F \land b \in dom F)) \to (R \in CRing \land a \in {Base}_{R} \land b \in {Base}_{R})$
25		eqid	$⊢ \cdot_{R} = \cdot_{R}$
26	13 25	crngcom	$⊢ (R \in CRing \land a \in {Base}_{R} \land b \in {Base}_{R}) \to a \cdot_{R} b = b \cdot_{R} a$
27	24 26	syl	$⊢ ((R \in CRing \land F \in (R RingHom S)) \land (a \in dom F \land b \in dom F)) \to a \cdot_{R} b = b \cdot_{R} a$
28	27	fveq2d	$⊢ ((R \in CRing \land F \in (R RingHom S)) \land (a \in dom F \land b \in dom F)) \to F (a \cdot_{R} b) = F (b \cdot_{R} a)$
29		simplr	$⊢ ((R \in CRing \land F \in (R RingHom S)) \land (a \in dom F \land b \in dom F)) \to F \in (R RingHom S)$
30		3anass	$⊢ (F \in (R RingHom S) \land a \in {Base}_{R} \land b \in {Base}_{R}) \leftrightarrow (F \in (R RingHom S) \land (a \in {Base}_{R} \land b \in {Base}_{R}))$
31	29 22 30	sylanbrc	$⊢ ((R \in CRing \land F \in (R RingHom S)) \land (a \in dom F \land b \in dom F)) \to (F \in (R RingHom S) \land a \in {Base}_{R} \land b \in {Base}_{R})$
32		eqid	$⊢ \cdot_{S} = \cdot_{S}$
33	13 25 32	rhmmul	$⊢ (F \in (R RingHom S) \land a \in {Base}_{R} \land b \in {Base}_{R}) \to F (a \cdot_{R} b) = F (a) \cdot_{S} F (b)$
34	31 33	syl	$⊢ ((R \in CRing \land F \in (R RingHom S)) \land (a \in dom F \land b \in dom F)) \to F (a \cdot_{R} b) = F (a) \cdot_{S} F (b)$
35	22	ancomd	$⊢ ((R \in CRing \land F \in (R RingHom S)) \land (a \in dom F \land b \in dom F)) \to (b \in {Base}_{R} \land a \in {Base}_{R})$
36		3anass	$⊢ (F \in (R RingHom S) \land b \in {Base}_{R} \land a \in {Base}_{R}) \leftrightarrow (F \in (R RingHom S) \land (b \in {Base}_{R} \land a \in {Base}_{R}))$
37	29 35 36	sylanbrc	$⊢ ((R \in CRing \land F \in (R RingHom S)) \land (a \in dom F \land b \in dom F)) \to (F \in (R RingHom S) \land b \in {Base}_{R} \land a \in {Base}_{R})$
38	13 25 32	rhmmul	$⊢ (F \in (R RingHom S) \land b \in {Base}_{R} \land a \in {Base}_{R}) \to F (b \cdot_{R} a) = F (b) \cdot_{S} F (a)$
39	37 38	syl	$⊢ ((R \in CRing \land F \in (R RingHom S)) \land (a \in dom F \land b \in dom F)) \to F (b \cdot_{R} a) = F (b) \cdot_{S} F (a)$
40	28 34 39	3eqtr3d	$⊢ ((R \in CRing \land F \in (R RingHom S)) \land (a \in dom F \land b \in dom F)) \to F (a) \cdot_{S} F (b) = F (b) \cdot_{S} F (a)$
41		oveq12	$⊢ (x = F (a) \land y = F (b)) \to x \cdot_{S} y = F (a) \cdot_{S} F (b)$
42		oveq12	$⊢ (y = F (b) \land x = F (a)) \to y \cdot_{S} x = F (b) \cdot_{S} F (a)$
43	42	ancoms	$⊢ (x = F (a) \land y = F (b)) \to y \cdot_{S} x = F (b) \cdot_{S} F (a)$
44	41 43	eqeq12d	$⊢ (x = F (a) \land y = F (b)) \to (x \cdot_{S} y = y \cdot_{S} x \leftrightarrow F (a) \cdot_{S} F (b) = F (b) \cdot_{S} F (a))$
45	40 44	syl5ibrcom	$⊢ ((R \in CRing \land F \in (R RingHom S)) \land (a \in dom F \land b \in dom F)) \to ((x = F (a) \land y = F (b)) \to x \cdot_{S} y = y \cdot_{S} x)$
46	45	ex	$⊢ (R \in CRing \land F \in (R RingHom S)) \to ((a \in dom F \land b \in dom F) \to ((x = F (a) \land y = F (b)) \to x \cdot_{S} y = y \cdot_{S} x))$
47	46	3adant3	$⊢ (R \in CRing \land F \in (R RingHom S) \land F : dom F \underset{onto}{⟶} B) \to ((a \in dom F \land b \in dom F) \to ((x = F (a) \land y = F (b)) \to x \cdot_{S} y = y \cdot_{S} x))$
48	47	rexlimdvv	$⊢ (R \in CRing \land F \in (R RingHom S) \land F : dom F \underset{onto}{⟶} B) \to (\exists a \in dom F \exists b \in dom F (x = F (a) \land y = F (b)) \to x \cdot_{S} y = y \cdot_{S} x)$
49	11 48	syld	$⊢ (R \in CRing \land F \in (R RingHom S) \land F : dom F \underset{onto}{⟶} B) \to ((x \in B \land y \in B) \to x \cdot_{S} y = y \cdot_{S} x)$
50	49	ralrimivv	$⊢ (R \in CRing \land F \in (R RingHom S) \land F : dom F \underset{onto}{⟶} B) \to \forall x \in B \forall y \in B x \cdot_{S} y = y \cdot_{S} x$
51	1 32	iscrng2	$⊢ S \in CRing \leftrightarrow (S \in Ring \land \forall x \in B \forall y \in B x \cdot_{S} y = y \cdot_{S} x)$
52	3 50 51	sylanbrc	$⊢ (R \in CRing \land F \in (R RingHom S) \land F : dom F \underset{onto}{⟶} B) \to S \in CRing$

Metamath Proof Explorer

Theorem crngrhmfo

Proof