Metamath Proof Explorer

Theorem rngoisohom

Description: Obsolete theorem, use rimrhm instead. A ring isomorphism is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	rngoisohom	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsIso S)) \to F \in (R RingOpsHom S)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ 1^{st} (R) = 1^{st} (R)$
2		eqid	$⊢ ran 1^{st} (R) = ran 1^{st} (R)$
3		eqid	$⊢ 1^{st} (S) = 1^{st} (S)$
4		eqid	$⊢ ran 1^{st} (S) = ran 1^{st} (S)$
5	1 2 3 4	isrngoiso	$⊢ (R \in RingOps \land S \in RingOps) \to (F \in (R RingOpsIso S) \leftrightarrow (F \in (R RingOpsHom S) \land F : ran 1^{st} (R) \underset{1-1 onto}{⟶} ran 1^{st} (S)))$
6	5	simprbda	$⊢ ((R \in RingOps \land S \in RingOps) \land F \in (R RingOpsIso S)) \to F \in (R RingOpsHom S)$
7	6	3impa	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsIso S)) \to F \in (R RingOpsHom S)$