rngohomadd

Description: Ring homomorphisms preserve addition. (Contributed by Jeff Madsen, 3-Jan-2011)

	Ref	Expression
Hypotheses	rnghomadd.1	$⊢ G = 1^{st} (R)$
	rnghomadd.2	$⊢ X = ran G$
	rnghomadd.3	$⊢ J = 1^{st} (S)$
Assertion	rngohomadd	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \land (A \in X \land B \in X)) \to F (A G B) = F (A) J F (B)$

Proof

Step	Hyp	Ref	Expression
1		rnghomadd.1	$⊢ G = 1^{st} (R)$
2		rnghomadd.2	$⊢ X = ran G$
3		rnghomadd.3	$⊢ J = 1^{st} (S)$
4		eqid	$⊢ 2^{nd} (R) = 2^{nd} (R)$
5		eqid	$⊢ GId (2^{nd} (R)) = GId (2^{nd} (R))$
6		eqid	$⊢ 2^{nd} (S) = 2^{nd} (S)$
7		eqid	$⊢ ran J = ran J$
8		eqid	$⊢ GId (2^{nd} (S)) = GId (2^{nd} (S))$
9	1 4 2 5 3 6 7 8	isrngohom	$⊢ (R \in RingOps \land S \in RingOps) \to (F \in (R RingOpsHom S) \leftrightarrow (F : X ⟶ ran J \land F (GId (2^{nd} (R))) = GId (2^{nd} (S)) \land \forall x \in X \forall y \in X (F (x G y) = F (x) J F (y) \land F (x 2^{nd} (R) y) = F (x) 2^{nd} (S) F (y))))$
10	9	biimpa	$⊢ ((R \in RingOps \land S \in RingOps) \land F \in (R RingOpsHom S)) \to (F : X ⟶ ran J \land F (GId (2^{nd} (R))) = GId (2^{nd} (S)) \land \forall x \in X \forall y \in X (F (x G y) = F (x) J F (y) \land F (x 2^{nd} (R) y) = F (x) 2^{nd} (S) F (y)))$
11	10	simp3d	$⊢ ((R \in RingOps \land S \in RingOps) \land F \in (R RingOpsHom S)) \to \forall x \in X \forall y \in X (F (x G y) = F (x) J F (y) \land F (x 2^{nd} (R) y) = F (x) 2^{nd} (S) F (y))$
12	11	3impa	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \to \forall x \in X \forall y \in X (F (x G y) = F (x) J F (y) \land F (x 2^{nd} (R) y) = F (x) 2^{nd} (S) F (y))$
13		simpl	$⊢ (F (x G y) = F (x) J F (y) \land F (x 2^{nd} (R) y) = F (x) 2^{nd} (S) F (y)) \to F (x G y) = F (x) J F (y)$
14	13	2ralimi	$⊢ \forall x \in X \forall y \in X (F (x G y) = F (x) J F (y) \land F (x 2^{nd} (R) y) = F (x) 2^{nd} (S) F (y)) \to \forall x \in X \forall y \in X F (x G y) = F (x) J F (y)$
15	12 14	syl	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \to \forall x \in X \forall y \in X F (x G y) = F (x) J F (y)$
16		fvoveq1	$⊢ x = A \to F (x G y) = F (A G y)$
17		fveq2	$⊢ x = A \to F (x) = F (A)$
18	17	oveq1d	$⊢ x = A \to F (x) J F (y) = F (A) J F (y)$
19	16 18	eqeq12d	$⊢ x = A \to (F (x G y) = F (x) J F (y) \leftrightarrow F (A G y) = F (A) J F (y))$
20		oveq2	$⊢ y = B \to A G y = A G B$
21	20	fveq2d	$⊢ y = B \to F (A G y) = F (A G B)$
22		fveq2	$⊢ y = B \to F (y) = F (B)$
23	22	oveq2d	$⊢ y = B \to F (A) J F (y) = F (A) J F (B)$
24	21 23	eqeq12d	$⊢ y = B \to (F (A G y) = F (A) J F (y) \leftrightarrow F (A G B) = F (A) J F (B))$
25	19 24	rspc2v	$⊢ (A \in X \land B \in X) \to (\forall x \in X \forall y \in X F (x G y) = F (x) J F (y) \to F (A G B) = F (A) J F (B))$
26	15 25	mpan9	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \land (A \in X \land B \in X)) \to F (A G B) = F (A) J F (B)$

Metamath Proof Explorer

Theorem rngohomadd

Proof