This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rngogrphom

Description: A ring homomorphism is a group homomorphism. (Contributed by Jeff Madsen, 2-Jan-2011)

		Ref	Expression
	Hypotheses	rnggrphom.1	$⊢ G = 1^{st} (R)$
		rnggrphom.2	$⊢ J = 1^{st} (S)$
	Assertion	rngogrphom	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \to F \in (G GrpOpHom J)$

Proof

Step	Hyp	Ref	Expression
1		rnggrphom.1	$⊢ G = 1^{st} (R)$
2		rnggrphom.2	$⊢ J = 1^{st} (S)$
3		eqid	$⊢ ran G = ran G$
4		eqid	$⊢ ran J = ran J$
5	1 3 2 4	rngohomf	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \to F : ran G ⟶ ran J$
6	1 3 2	rngohomadd	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \land (x \in ran G \land y \in ran G)) \to F (x G y) = F (x) J F (y)$
7	6	eqcomd	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \land (x \in ran G \land y \in ran G)) \to F (x) J F (y) = F (x G y)$
8	7	ralrimivva	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \to \forall x \in ran G \forall y \in ran G F (x) J F (y) = F (x G y)$
9	1	rngogrpo	$⊢ R \in RingOps \to G \in GrpOp$
10	2	rngogrpo	$⊢ S \in RingOps \to J \in GrpOp$
11	3 4	elghomOLD	$⊢ (G \in GrpOp \land J \in GrpOp) \to (F \in (G GrpOpHom J) \leftrightarrow (F : ran G ⟶ ran J \land \forall x \in ran G \forall y \in ran G F (x) J F (y) = F (x G y)))$
12	9 10 11	syl2an	$⊢ (R \in RingOps \land S \in RingOps) \to (F \in (G GrpOpHom J) \leftrightarrow (F : ran G ⟶ ran J \land \forall x \in ran G \forall y \in ran G F (x) J F (y) = F (x G y)))$
13	12	3adant3	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \to (F \in (G GrpOpHom J) \leftrightarrow (F : ran G ⟶ ran J \land \forall x \in ran G \forall y \in ran G F (x) J F (y) = F (x G y)))$
14	5 8 13	mpbir2and	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \to F \in (G GrpOpHom J)$