Metamath Proof Explorer

Theorem isrngim2

Description: An isomorphism of non-unital rings is a bijective homomorphism. (Contributed by AV, 23-Feb-2020)

Ref Expression
Hypotheses rnghmf1o.b ⊢ B = Base R
rnghmf1o.c ⊢ C = Base S
Assertion isrngim2 ⊢ R ∈ V ∧ S ∈ W → F ∈ R RngIso S ↔ F ∈ R RngHom S ∧ F : B ⟶ 1-1 onto C

Proof

Step Hyp Ref Expression
1 rnghmf1o.b ⊢ B = Base R
2 rnghmf1o.c ⊢ C = Base S
3 isrngim ⊢ R ∈ V ∧ S ∈ W → F ∈ R RngIso S ↔ F ∈ R RngHom S ∧ F -1 ∈ S RngHom R
4 1 2 rnghmf1o ⊢ F ∈ R RngHom S → F : B ⟶ 1-1 onto C ↔ F -1 ∈ S RngHom R
5 4 bicomd ⊢ F ∈ R RngHom S → F -1 ∈ S RngHom R ↔ F : B ⟶ 1-1 onto C
6 5 a1i ⊢ R ∈ V ∧ S ∈ W → F ∈ R RngHom S → F -1 ∈ S RngHom R ↔ F : B ⟶ 1-1 onto C
7 6 pm5.32d ⊢ R ∈ V ∧ S ∈ W → F ∈ R RngHom S ∧ F -1 ∈ S RngHom R ↔ F ∈ R RngHom S ∧ F : B ⟶ 1-1 onto C
8 3 7 bitrd ⊢ R ∈ V ∧ S ∈ W → F ∈ R RngIso S ↔ F ∈ R RngHom S ∧ F : B ⟶ 1-1 onto C