rngohomsub

Description: Ring homomorphisms preserve subtraction. (Contributed by Jeff Madsen, 15-Jun-2011)

	Ref	Expression
Hypotheses	rnghomsub.1	$⊢ G = 1^{st} (R)$
	rnghomsub.2	$⊢ X = ran G$
	rnghomsub.3	$⊢ H = /_{g} (G)$
	rnghomsub.4	$⊢ J = 1^{st} (S)$
	rnghomsub.5	$⊢ K = /_{g} (J)$
Assertion	rngohomsub	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \land (A \in X \land B \in X)) \to F (A H B) = F (A) K F (B)$

Step	Hyp	Ref	Expression
1		rnghomsub.1	$⊢ G = 1^{st} (R)$
2		rnghomsub.2	$⊢ X = ran G$
3		rnghomsub.3	$⊢ H = /_{g} (G)$
4		rnghomsub.4	$⊢ J = 1^{st} (S)$
5		rnghomsub.5	$⊢ K = /_{g} (J)$
6	1	rngogrpo	$⊢ R \in RingOps \to G \in GrpOp$
7	6	3ad2ant1	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \to G \in GrpOp$
8	4	rngogrpo	$⊢ S \in RingOps \to J \in GrpOp$
9	8	3ad2ant2	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \to J \in GrpOp$
10	1 4	rngogrphom	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \to F \in (G GrpOpHom J)$
11	7 9 10	3jca	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \to (G \in GrpOp \land J \in GrpOp \land F \in (G GrpOpHom J))$
12	2 3 5	ghomdiv	$⊢ ((G \in GrpOp \land J \in GrpOp \land F \in (G GrpOpHom J)) \land (A \in X \land B \in X)) \to F (A H B) = F (A) K F (B)$
13	11 12	sylan	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \land (A \in X \land B \in X)) \to F (A H B) = F (A) K F (B)$

Metamath Proof Explorer