Metamath Proof Explorer

Theorem isrngim

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 isrngim ⊢ R ∈ V ∧ S ∈ W → F ∈ R RngIsom S ↔ F ∈ R RngHomo 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 isrngisom ⊢ R ∈ V ∧ S ∈ W → F ∈ R RngIsom S ↔ F ∈ R RngHomo S ∧ F -1 ∈ S RngHomo R
4 1 2 rnghmf1o ⊢ F ∈ R RngHomo S → F : B ⟶ 1-1 onto C ↔ F -1 ∈ S RngHomo R
5 4 bicomd ⊢ F ∈ R RngHomo S → F -1 ∈ S RngHomo R ↔ F : B ⟶ 1-1 onto C
6 5 a1i ⊢ R ∈ V ∧ S ∈ W → F ∈ R RngHomo S → F -1 ∈ S RngHomo R ↔ F : B ⟶ 1-1 onto C
7 6 pm5.32d ⊢ R ∈ V ∧ S ∈ W → F ∈ R RngHomo S ∧ F -1 ∈ S RngHomo R ↔ F ∈ R RngHomo S ∧ F : B ⟶ 1-1 onto C
8 3 7 bitrd ⊢ R ∈ V ∧ S ∈ W → F ∈ R RngIsom S ↔ F ∈ R RngHomo S ∧ F : B ⟶ 1-1 onto C