Metamath Proof Explorer

Theorem rngohom0

Description: Obsolete theorem, use rhm0 instead. A ring homomorphism preserves 0 . (Contributed by Jeff Madsen, 2-Jan-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	rnghom0.1	$⊢ G = 1^{st} (R)$
		rnghom0.2	$⊢ Z = GId (G)$
		rnghom0.3	$⊢ J = 1^{st} (S)$
		rnghom0.4	$⊢ W = GId (J)$
	Assertion	rngohom0	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \to F (Z) = W$

Proof

Step	Hyp	Ref	Expression
1		rnghom0.1	$⊢ G = 1^{st} (R)$
2		rnghom0.2	$⊢ Z = GId (G)$
3		rnghom0.3	$⊢ J = 1^{st} (S)$
4		rnghom0.4	$⊢ W = GId (J)$
5	1	rngogrpo	$⊢ R \in RingOps \to G \in GrpOp$
6	5	3ad2ant1	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \to G \in GrpOp$
7	3	rngogrpo	$⊢ S \in RingOps \to J \in GrpOp$
8	7	3ad2ant2	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \to J \in GrpOp$
9	1 3	rngogrphom	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \to F \in (G GrpOpHom J)$
10	2 4	ghomidOLD	$⊢ (G \in GrpOp \land J \in GrpOp \land F \in (G GrpOpHom J)) \to F (Z) = W$
11	6 8 9 10	syl3anc	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \to F (Z) = W$