rngoisohom

Description: A ring isomorphism is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011)

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

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 RngIso S) \leftrightarrow (F \in (R RngHom 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 RngIso S)) \to F \in (R RngHom S)$
7	6	3impa	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngIso S)) \to F \in (R RngHom S)$

Metamath Proof Explorer