Metamath Proof Explorer

Theorem isrim0

Description: An isomorphism of rings is a homomorphism whose converse is also a homomorphism . (Contributed by AV, 22-Oct-2019)

Ref Expression
Assertion isrim0 ⊢ R ∈ V ∧ S ∈ W → F ∈ R RingIso S ↔ F ∈ R RingHom S ∧ F -1 ∈ S RingHom R

Proof

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