rngohommul

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

	Ref	Expression
Hypotheses	rnghommul.1	$⊢ G = 1^{st} (R)$
	rnghommul.2	$⊢ X = ran G$
	rnghommul.3	$⊢ H = 2^{nd} (R)$
	rnghommul.4	$⊢ K = 2^{nd} (S)$
Assertion	rngohommul	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (A \in X \land B \in X)) \to F (A H B) = F (A) K F (B)$

Proof

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

Metamath Proof Explorer

Theorem rngohommul

Proof