Metamath Proof Explorer

Theorem rngohomsub

Description: Obsolete theorem, use rhmsub instead. Ring homomorphisms preserve subtraction. (Contributed by Jeff Madsen, 15-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		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)$

Proof

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)$