Metamath Proof Explorer

Theorem isrngim

Description: An isomorphism of non-unital rings is a homomorphism whose converse is also a homomorphism. (Contributed by AV, 22-Feb-2020)

Ref Expression
Assertion isrngim ⊢ R ∈ V ∧ S ∈ W → F ∈ R RngIso S ↔ F ∈ R RngHom S ∧ F -1 ∈ S RngHom R

Proof

Step Hyp Ref Expression
1 df-rngim ⊢ RngIso = r ∈ V , s ∈ V ⟼ f ∈ r RngHom s | f -1 ∈ s RngHom r
2 1 a1i ⊢ R ∈ V ∧ S ∈ W → RngIso = r ∈ V , s ∈ V ⟼ f ∈ r RngHom s | f -1 ∈ s RngHom r
3 oveq12 ⊢ r = R ∧ s = S → r RngHom s = R RngHom S
4 3 adantl ⊢ R ∈ V ∧ S ∈ W ∧ r = R ∧ s = S → r RngHom s = R RngHom S
5 oveq12 ⊢ s = S ∧ r = R → s RngHom r = S RngHom R
6 5 ancoms ⊢ r = R ∧ s = S → s RngHom r = S RngHom R
7 6 adantl ⊢ R ∈ V ∧ S ∈ W ∧ r = R ∧ s = S → s RngHom r = S RngHom R
8 7 eleq2d ⊢ R ∈ V ∧ S ∈ W ∧ r = R ∧ s = S → f -1 ∈ s RngHom r ↔ f -1 ∈ S RngHom R
9 4 8 rabeqbidv ⊢ R ∈ V ∧ S ∈ W ∧ r = R ∧ s = S → f ∈ r RngHom s | f -1 ∈ s RngHom r = f ∈ R RngHom S | f -1 ∈ S RngHom R
10 elex ⊢ R ∈ V → R ∈ V
11 10 adantr ⊢ R ∈ V ∧ S ∈ W → R ∈ V
12 elex ⊢ S ∈ W → S ∈ V
13 12 adantl ⊢ R ∈ V ∧ S ∈ W → S ∈ V
14 ovex ⊢ R RngHom S ∈ V
15 14 rabex ⊢ f ∈ R RngHom S | f -1 ∈ S RngHom R ∈ V
16 15 a1i ⊢ R ∈ V ∧ S ∈ W → f ∈ R RngHom S | f -1 ∈ S RngHom R ∈ V
17 2 9 11 13 16 ovmpod ⊢ R ∈ V ∧ S ∈ W → R RngIso S = f ∈ R RngHom S | f -1 ∈ S RngHom R
18 17 eleq2d ⊢ R ∈ V ∧ S ∈ W → F ∈ R RngIso S ↔ F ∈ f ∈ R RngHom S | f -1 ∈ S RngHom R
19 cnveq ⊢ f = F → f -1 = F -1
20 19 eleq1d ⊢ f = F → f -1 ∈ S RngHom R ↔ F -1 ∈ S RngHom R
21 20 elrab ⊢ F ∈ f ∈ R RngHom S | f -1 ∈ S RngHom R ↔ F ∈ R RngHom S ∧ F -1 ∈ S RngHom R
22 18 21 bitrdi ⊢ R ∈ V ∧ S ∈ W → F ∈ R RngIso S ↔ F ∈ R RngHom S ∧ F -1 ∈ S RngHom R