rngohom0

Description: A ring homomorphism preserves 0 . (Contributed by Jeff Madsen, 2-Jan-2011)

	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 RngHom S)) \to F (Z) = W$

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 RngHom 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 RngHom S)) \to J \in GrpOp$
9	1 3	rngogrphom	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom 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 RngHom S)) \to F (Z) = W$

Metamath Proof Explorer