Metamath Proof Explorer

Theorem rngohomf

Description: Obsolete theorem, use rhmf instead. A ring homomorphism is a function. (Contributed by Jeff Madsen, 19-Jun-2010) (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	rngohomf	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \to F : X ⟶ 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		eqid	$⊢ 2^{nd} (R) = 2^{nd} (R)$
6		eqid	$⊢ GId (2^{nd} (R)) = GId (2^{nd} (R))$
7		eqid	$⊢ 2^{nd} (S) = 2^{nd} (S)$
8		eqid	$⊢ GId (2^{nd} (S)) = GId (2^{nd} (S))$
9	1 5 2 6 3 7 4 8	isrngohom	$⊢ (R \in RingOps \land S \in RingOps) \to (F \in (R RingOpsHom S) \leftrightarrow (F : X ⟶ Y \land F (GId (2^{nd} (R))) = GId (2^{nd} (S)) \land \forall x \in X \forall y \in X (F (x G y) = F (x) J F (y) \land F (x 2^{nd} (R) y) = F (x) 2^{nd} (S) F (y))))$
10	9	biimpa	$⊢ ((R \in RingOps \land S \in RingOps) \land F \in (R RingOpsHom S)) \to (F : X ⟶ Y \land F (GId (2^{nd} (R))) = GId (2^{nd} (S)) \land \forall x \in X \forall y \in X (F (x G y) = F (x) J F (y) \land F (x 2^{nd} (R) y) = F (x) 2^{nd} (S) F (y)))$
11	10	simp1d	$⊢ ((R \in RingOps \land S \in RingOps) \land F \in (R RingOpsHom S)) \to F : X ⟶ Y$
12	11	3impa	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \to F : X ⟶ Y$