Metamath Proof Explorer

Theorem rngohomcl

Description: Obsolete theorem, use rhmcl instead. Closure law for a ring homomorphism. (Contributed by Jeff Madsen, 3-Jan-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rnghomf.1	$⊢ G = 1^{st} (R)$
	rnghomf.2	$⊢ X = ran G$
	rnghomf.3	$⊢ J = 1^{st} (S)$
	rnghomf.4	$⊢ Y = ran J$
Assertion	rngohomcl	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \land A \in X) \to F (A) \in Y$

Proof

Step	Hyp	Ref	Expression
1		rnghomf.1	$⊢ G = 1^{st} (R)$
2		rnghomf.2	$⊢ X = ran G$
3		rnghomf.3	$⊢ J = 1^{st} (S)$
4		rnghomf.4	$⊢ Y = ran J$
5	1 2 3 4	rngohomf	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \to F : X ⟶ Y$
6	5	ffvelcdmda	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \land A \in X) \to F (A) \in Y$