crngohomfo

Description: The image of a homomorphism from a commutative ring is commutative. (Contributed by Jeff Madsen, 4-Jan-2011)

	Ref	Expression
Hypotheses	crnghomfo.1	$⊢ G = 1^{st} (R)$
	crnghomfo.2	$⊢ X = ran G$
	crnghomfo.3	$⊢ J = 1^{st} (S)$
	crnghomfo.4	$⊢ Y = ran J$
Assertion	crngohomfo	$⊢ ((R \in CRingOps \land S \in RingOps) \land (F \in (R RngHom S) \land F : X \underset{onto}{⟶} Y)) \to S \in CRingOps$

Proof

Step	Hyp	Ref	Expression
1		crnghomfo.1	$⊢ G = 1^{st} (R)$
2		crnghomfo.2	$⊢ X = ran G$
3		crnghomfo.3	$⊢ J = 1^{st} (S)$
4		crnghomfo.4	$⊢ Y = ran J$
5		simplr	$⊢ ((R \in CRingOps \land S \in RingOps) \land (F \in (R RngHom S) \land F : X \underset{onto}{⟶} Y)) \to S \in RingOps$
6		foelrn	$⊢ (F : X \underset{onto}{⟶} Y \land y \in Y) \to \exists w \in X y = F (w)$
7	6	ex	$⊢ F : X \underset{onto}{⟶} Y \to (y \in Y \to \exists w \in X y = F (w))$
8		foelrn	$⊢ (F : X \underset{onto}{⟶} Y \land z \in Y) \to \exists x \in X z = F (x)$
9	8	ex	$⊢ F : X \underset{onto}{⟶} Y \to (z \in Y \to \exists x \in X z = F (x))$
10	7 9	anim12d	$⊢ F : X \underset{onto}{⟶} Y \to ((y \in Y \land z \in Y) \to (\exists w \in X y = F (w) \land \exists x \in X z = F (x)))$
11		reeanv	$⊢ \exists w \in X \exists x \in X (y = F (w) \land z = F (x)) \leftrightarrow (\exists w \in X y = F (w) \land \exists x \in X z = F (x))$
12	10 11	syl6ibr	$⊢ F : X \underset{onto}{⟶} Y \to ((y \in Y \land z \in Y) \to \exists w \in X \exists x \in X (y = F (w) \land z = F (x)))$
13	12	ad2antll	$⊢ ((R \in CRingOps \land S \in RingOps) \land (F \in (R RngHom S) \land F : X \underset{onto}{⟶} Y)) \to ((y \in Y \land z \in Y) \to \exists w \in X \exists x \in X (y = F (w) \land z = F (x)))$
14		eqid	$⊢ 2^{nd} (R) = 2^{nd} (R)$
15	1 14 2	crngocom	$⊢ (R \in CRingOps \land w \in X \land x \in X) \to w 2^{nd} (R) x = x 2^{nd} (R) w$
16	15	3expb	$⊢ (R \in CRingOps \land (w \in X \land x \in X)) \to w 2^{nd} (R) x = x 2^{nd} (R) w$
17	16	3ad2antl1	$⊢ ((R \in CRingOps \land S \in RingOps \land F \in (R RngHom S)) \land (w \in X \land x \in X)) \to w 2^{nd} (R) x = x 2^{nd} (R) w$
18	17	fveq2d	$⊢ ((R \in CRingOps \land S \in RingOps \land F \in (R RngHom S)) \land (w \in X \land x \in X)) \to F (w 2^{nd} (R) x) = F (x 2^{nd} (R) w)$
19		crngorngo	$⊢ R \in CRingOps \to R \in RingOps$
20		eqid	$⊢ 2^{nd} (S) = 2^{nd} (S)$
21	1 2 14 20	rngohommul	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (w \in X \land x \in X)) \to F (w 2^{nd} (R) x) = F (w) 2^{nd} (S) F (x)$
22	19 21	syl3anl1	$⊢ ((R \in CRingOps \land S \in RingOps \land F \in (R RngHom S)) \land (w \in X \land x \in X)) \to F (w 2^{nd} (R) x) = F (w) 2^{nd} (S) F (x)$
23	1 2 14 20	rngohommul	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in X \land w \in X)) \to F (x 2^{nd} (R) w) = F (x) 2^{nd} (S) F (w)$
24	23	ancom2s	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (w \in X \land x \in X)) \to F (x 2^{nd} (R) w) = F (x) 2^{nd} (S) F (w)$
25	19 24	syl3anl1	$⊢ ((R \in CRingOps \land S \in RingOps \land F \in (R RngHom S)) \land (w \in X \land x \in X)) \to F (x 2^{nd} (R) w) = F (x) 2^{nd} (S) F (w)$
26	18 22 25	3eqtr3d	$⊢ ((R \in CRingOps \land S \in RingOps \land F \in (R RngHom S)) \land (w \in X \land x \in X)) \to F (w) 2^{nd} (S) F (x) = F (x) 2^{nd} (S) F (w)$
27		oveq12	$⊢ (y = F (w) \land z = F (x)) \to y 2^{nd} (S) z = F (w) 2^{nd} (S) F (x)$
28		oveq12	$⊢ (z = F (x) \land y = F (w)) \to z 2^{nd} (S) y = F (x) 2^{nd} (S) F (w)$
29	28	ancoms	$⊢ (y = F (w) \land z = F (x)) \to z 2^{nd} (S) y = F (x) 2^{nd} (S) F (w)$
30	27 29	eqeq12d	$⊢ (y = F (w) \land z = F (x)) \to (y 2^{nd} (S) z = z 2^{nd} (S) y \leftrightarrow F (w) 2^{nd} (S) F (x) = F (x) 2^{nd} (S) F (w))$
31	26 30	syl5ibrcom	$⊢ ((R \in CRingOps \land S \in RingOps \land F \in (R RngHom S)) \land (w \in X \land x \in X)) \to ((y = F (w) \land z = F (x)) \to y 2^{nd} (S) z = z 2^{nd} (S) y)$
32	31	ex	$⊢ (R \in CRingOps \land S \in RingOps \land F \in (R RngHom S)) \to ((w \in X \land x \in X) \to ((y = F (w) \land z = F (x)) \to y 2^{nd} (S) z = z 2^{nd} (S) y))$
33	32	3expa	$⊢ ((R \in CRingOps \land S \in RingOps) \land F \in (R RngHom S)) \to ((w \in X \land x \in X) \to ((y = F (w) \land z = F (x)) \to y 2^{nd} (S) z = z 2^{nd} (S) y))$
34	33	adantrr	$⊢ ((R \in CRingOps \land S \in RingOps) \land (F \in (R RngHom S) \land F : X \underset{onto}{⟶} Y)) \to ((w \in X \land x \in X) \to ((y = F (w) \land z = F (x)) \to y 2^{nd} (S) z = z 2^{nd} (S) y))$
35	34	rexlimdvv	$⊢ ((R \in CRingOps \land S \in RingOps) \land (F \in (R RngHom S) \land F : X \underset{onto}{⟶} Y)) \to (\exists w \in X \exists x \in X (y = F (w) \land z = F (x)) \to y 2^{nd} (S) z = z 2^{nd} (S) y)$
36	13 35	syld	$⊢ ((R \in CRingOps \land S \in RingOps) \land (F \in (R RngHom S) \land F : X \underset{onto}{⟶} Y)) \to ((y \in Y \land z \in Y) \to y 2^{nd} (S) z = z 2^{nd} (S) y)$
37	36	ralrimivv	$⊢ ((R \in CRingOps \land S \in RingOps) \land (F \in (R RngHom S) \land F : X \underset{onto}{⟶} Y)) \to \forall y \in Y \forall z \in Y y 2^{nd} (S) z = z 2^{nd} (S) y$
38	3 20 4	iscrngo2	$⊢ S \in CRingOps \leftrightarrow (S \in RingOps \land \forall y \in Y \forall z \in Y y 2^{nd} (S) z = z 2^{nd} (S) y)$
39	5 37 38	sylanbrc	$⊢ ((R \in CRingOps \land S \in RingOps) \land (F \in (R RngHom S) \land F : X \underset{onto}{⟶} Y)) \to S \in CRingOps$

Metamath Proof Explorer

Theorem crngohomfo

Proof