Description: An isomorphism of non-unital rings is a homomorphism. (Contributed by AV, 23-Feb-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rnghmf1o.b | ⊢ 𝐵 = ( Base ‘ 𝑅 ) | |
rnghmf1o.c | ⊢ 𝐶 = ( Base ‘ 𝑆 ) | ||
Assertion | rngimrnghm | ⊢ ( 𝐹 ∈ ( 𝑅 RngIsom 𝑆 ) → 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rnghmf1o.b | ⊢ 𝐵 = ( Base ‘ 𝑅 ) | |
2 | rnghmf1o.c | ⊢ 𝐶 = ( Base ‘ 𝑆 ) | |
3 | rngimrcl | ⊢ ( 𝐹 ∈ ( 𝑅 RngIsom 𝑆 ) → ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ) | |
4 | 1 2 | isrngim | ⊢ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → ( 𝐹 ∈ ( 𝑅 RngIsom 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ) ) |
5 | simpl | ⊢ ( ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ) | |
6 | 4 5 | syl6bi | ⊢ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → ( 𝐹 ∈ ( 𝑅 RngIsom 𝑆 ) → 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ) ) |
7 | 3 6 | mpcom | ⊢ ( 𝐹 ∈ ( 𝑅 RngIsom 𝑆 ) → 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ) |