Metamath Proof Explorer

Theorem isrngisom

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 isrngisom ⊢ R ∈ V ∧ S ∈ W → F ∈ R RngIsom S ↔ F ∈ R RngHomo S ∧ F -1 ∈ S RngHomo R

Proof

Step Hyp Ref Expression
1 df-rngisom ⊢ RngIsom = r ∈ V , s ∈ V ⟼ f ∈ r RngHomo s | f -1 ∈ s RngHomo r
2 1 a1i ⊢ R ∈ V ∧ S ∈ W → RngIsom = r ∈ V , s ∈ V ⟼ f ∈ r RngHomo s | f -1 ∈ s RngHomo r
3 oveq12 ⊢ r = R ∧ s = S → r RngHomo s = R RngHomo S
4 3 adantl ⊢ R ∈ V ∧ S ∈ W ∧ r = R ∧ s = S → r RngHomo s = R RngHomo S
5 oveq12 ⊢ s = S ∧ r = R → s RngHomo r = S RngHomo R
6 5 ancoms ⊢ r = R ∧ s = S → s RngHomo r = S RngHomo R
7 6 adantl ⊢ R ∈ V ∧ S ∈ W ∧ r = R ∧ s = S → s RngHomo r = S RngHomo R
8 7 eleq2d ⊢ R ∈ V ∧ S ∈ W ∧ r = R ∧ s = S → f -1 ∈ s RngHomo r ↔ f -1 ∈ S RngHomo R
9 4 8 rabeqbidv ⊢ R ∈ V ∧ S ∈ W ∧ r = R ∧ s = S → f ∈ r RngHomo s | f -1 ∈ s RngHomo r = f ∈ R RngHomo S | f -1 ∈ S RngHomo 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 RngHomo S ∈ V
15 14 rabex ⊢ f ∈ R RngHomo S | f -1 ∈ S RngHomo R ∈ V
16 15 a1i ⊢ R ∈ V ∧ S ∈ W → f ∈ R RngHomo S | f -1 ∈ S RngHomo R ∈ V
17 2 9 11 13 16 ovmpod ⊢ R ∈ V ∧ S ∈ W → R RngIsom S = f ∈ R RngHomo S | f -1 ∈ S RngHomo R
18 17 eleq2d ⊢ R ∈ V ∧ S ∈ W → F ∈ R RngIsom S ↔ F ∈ f ∈ R RngHomo S | f -1 ∈ S RngHomo R
19 cnveq ⊢ f = F → f -1 = F -1
20 19 eleq1d ⊢ f = F → f -1 ∈ S RngHomo R ↔ F -1 ∈ S RngHomo R
21 20 elrab ⊢ F ∈ f ∈ R RngHomo S | f -1 ∈ S RngHomo R ↔ F ∈ R RngHomo S ∧ F -1 ∈ S RngHomo R
22 18 21 bitrdi ⊢ R ∈ V ∧ S ∈ W → F ∈ R RngIsom S ↔ F ∈ R RngHomo S ∧ F -1 ∈ S RngHomo R