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	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsIso 𝑆 ) ) → 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 1^st ‘ 𝑅 ) = ( 1^st ‘ 𝑅 )
2		eqid	⊢ ran ( 1^st ‘ 𝑅 ) = ran ( 1^st ‘ 𝑅 )
3		eqid	⊢ ( 1^st ‘ 𝑆 ) = ( 1^st ‘ 𝑆 )
4		eqid	⊢ ran ( 1^st ‘ 𝑆 ) = ran ( 1^st ‘ 𝑆 )
5	1 2 3 4	isrngoiso	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝐹 ∈ ( 𝑅 RingOpsIso 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) )
6	5	simprbda	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 ∈ ( 𝑅 RingOpsIso 𝑆 ) ) → 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) )
7	6	3impa	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsIso 𝑆 ) ) → 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) )