Database
BASIC ALGEBRAIC STRUCTURES
Rings
Ring homomorphisms
rimrhmOLD
Metamath Proof Explorer
Description: Obsolete version of rimrhm as of 12-Jan-2025. (Contributed by AV , 22-Oct-2019) (Proof modification is discouraged.)
(New usage is discouraged.)
Ref
Expression
Hypotheses
rhmf1o.b
⊢ 𝐵 = ( Base ‘ 𝑅 )
rhmf1o.c
⊢ 𝐶 = ( Base ‘ 𝑆 )
Assertion
rimrhmOLD
⊢ ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
Proof
Step
Hyp
Ref
Expression
1
rhmf1o.b
⊢ 𝐵 = ( Base ‘ 𝑅 )
2
rhmf1o.c
⊢ 𝐶 = ( Base ‘ 𝑆 )
3
1 2
isrim
⊢ ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1 -onto → 𝐶 ) )
4
3
simplbi
⊢ ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )