# Metamath Proof Explorer

## Theorem isocnv

Description: Converse law for isomorphism. Proposition 6.30(2) of TakeutiZaring p. 33. (Contributed by NM, 27-Apr-2004)

Ref Expression
Assertion isocnv ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)\to {{H}}^{-1}{Isom}_{{S},{R}}\left({B},{A}\right)$

### Proof

Step Hyp Ref Expression
1 f1ocnv ${⊢}{H}:{A}\underset{1-1 onto}{⟶}{B}\to {{H}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}$
2 1 adantr ${⊢}\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)\right)\to {{H}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}$
3 f1ocnvfv2 ${⊢}\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge {z}\in {B}\right)\to {H}\left({{H}}^{-1}\left({z}\right)\right)={z}$
4 3 adantrr ${⊢}\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\to {H}\left({{H}}^{-1}\left({z}\right)\right)={z}$
5 f1ocnvfv2 ${⊢}\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge {w}\in {B}\right)\to {H}\left({{H}}^{-1}\left({w}\right)\right)={w}$
6 5 adantrl ${⊢}\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\to {H}\left({{H}}^{-1}\left({w}\right)\right)={w}$
7 4 6 breq12d ${⊢}\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\to \left({H}\left({{H}}^{-1}\left({z}\right)\right){S}{H}\left({{H}}^{-1}\left({w}\right)\right)↔{z}{S}{w}\right)$
8 7 adantlr ${⊢}\left(\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)\right)\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\to \left({H}\left({{H}}^{-1}\left({z}\right)\right){S}{H}\left({{H}}^{-1}\left({w}\right)\right)↔{z}{S}{w}\right)$
9 f1of ${⊢}{{H}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}\to {{H}}^{-1}:{B}⟶{A}$
10 1 9 syl ${⊢}{H}:{A}\underset{1-1 onto}{⟶}{B}\to {{H}}^{-1}:{B}⟶{A}$
11 ffvelrn ${⊢}\left({{H}}^{-1}:{B}⟶{A}\wedge {z}\in {B}\right)\to {{H}}^{-1}\left({z}\right)\in {A}$
12 ffvelrn ${⊢}\left({{H}}^{-1}:{B}⟶{A}\wedge {w}\in {B}\right)\to {{H}}^{-1}\left({w}\right)\in {A}$
13 11 12 anim12dan ${⊢}\left({{H}}^{-1}:{B}⟶{A}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\to \left({{H}}^{-1}\left({z}\right)\in {A}\wedge {{H}}^{-1}\left({w}\right)\in {A}\right)$
14 breq1 ${⊢}{x}={{H}}^{-1}\left({z}\right)\to \left({x}{R}{y}↔{{H}}^{-1}\left({z}\right){R}{y}\right)$
15 fveq2 ${⊢}{x}={{H}}^{-1}\left({z}\right)\to {H}\left({x}\right)={H}\left({{H}}^{-1}\left({z}\right)\right)$
16 15 breq1d ${⊢}{x}={{H}}^{-1}\left({z}\right)\to \left({H}\left({x}\right){S}{H}\left({y}\right)↔{H}\left({{H}}^{-1}\left({z}\right)\right){S}{H}\left({y}\right)\right)$
17 14 16 bibi12d ${⊢}{x}={{H}}^{-1}\left({z}\right)\to \left(\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)↔\left({{H}}^{-1}\left({z}\right){R}{y}↔{H}\left({{H}}^{-1}\left({z}\right)\right){S}{H}\left({y}\right)\right)\right)$
18 bicom ${⊢}\left({{H}}^{-1}\left({z}\right){R}{y}↔{H}\left({{H}}^{-1}\left({z}\right)\right){S}{H}\left({y}\right)\right)↔\left({H}\left({{H}}^{-1}\left({z}\right)\right){S}{H}\left({y}\right)↔{{H}}^{-1}\left({z}\right){R}{y}\right)$
19 17 18 syl6bb ${⊢}{x}={{H}}^{-1}\left({z}\right)\to \left(\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)↔\left({H}\left({{H}}^{-1}\left({z}\right)\right){S}{H}\left({y}\right)↔{{H}}^{-1}\left({z}\right){R}{y}\right)\right)$
20 fveq2 ${⊢}{y}={{H}}^{-1}\left({w}\right)\to {H}\left({y}\right)={H}\left({{H}}^{-1}\left({w}\right)\right)$
21 20 breq2d ${⊢}{y}={{H}}^{-1}\left({w}\right)\to \left({H}\left({{H}}^{-1}\left({z}\right)\right){S}{H}\left({y}\right)↔{H}\left({{H}}^{-1}\left({z}\right)\right){S}{H}\left({{H}}^{-1}\left({w}\right)\right)\right)$
22 breq2 ${⊢}{y}={{H}}^{-1}\left({w}\right)\to \left({{H}}^{-1}\left({z}\right){R}{y}↔{{H}}^{-1}\left({z}\right){R}{{H}}^{-1}\left({w}\right)\right)$
23 21 22 bibi12d ${⊢}{y}={{H}}^{-1}\left({w}\right)\to \left(\left({H}\left({{H}}^{-1}\left({z}\right)\right){S}{H}\left({y}\right)↔{{H}}^{-1}\left({z}\right){R}{y}\right)↔\left({H}\left({{H}}^{-1}\left({z}\right)\right){S}{H}\left({{H}}^{-1}\left({w}\right)\right)↔{{H}}^{-1}\left({z}\right){R}{{H}}^{-1}\left({w}\right)\right)\right)$
24 19 23 rspc2va ${⊢}\left(\left({{H}}^{-1}\left({z}\right)\in {A}\wedge {{H}}^{-1}\left({w}\right)\in {A}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)\right)\to \left({H}\left({{H}}^{-1}\left({z}\right)\right){S}{H}\left({{H}}^{-1}\left({w}\right)\right)↔{{H}}^{-1}\left({z}\right){R}{{H}}^{-1}\left({w}\right)\right)$
25 13 24 sylan ${⊢}\left(\left({{H}}^{-1}:{B}⟶{A}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)\right)\to \left({H}\left({{H}}^{-1}\left({z}\right)\right){S}{H}\left({{H}}^{-1}\left({w}\right)\right)↔{{H}}^{-1}\left({z}\right){R}{{H}}^{-1}\left({w}\right)\right)$
26 25 an32s ${⊢}\left(\left({{H}}^{-1}:{B}⟶{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)\right)\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\to \left({H}\left({{H}}^{-1}\left({z}\right)\right){S}{H}\left({{H}}^{-1}\left({w}\right)\right)↔{{H}}^{-1}\left({z}\right){R}{{H}}^{-1}\left({w}\right)\right)$
27 10 26 sylanl1 ${⊢}\left(\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)\right)\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\to \left({H}\left({{H}}^{-1}\left({z}\right)\right){S}{H}\left({{H}}^{-1}\left({w}\right)\right)↔{{H}}^{-1}\left({z}\right){R}{{H}}^{-1}\left({w}\right)\right)$
28 8 27 bitr3d ${⊢}\left(\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)\right)\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\to \left({z}{S}{w}↔{{H}}^{-1}\left({z}\right){R}{{H}}^{-1}\left({w}\right)\right)$
29 28 ralrimivva ${⊢}\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)\right)\to \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}{S}{w}↔{{H}}^{-1}\left({z}\right){R}{{H}}^{-1}\left({w}\right)\right)$
30 2 29 jca ${⊢}\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)\right)\to \left({{H}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}{S}{w}↔{{H}}^{-1}\left({z}\right){R}{{H}}^{-1}\left({w}\right)\right)\right)$
31 df-isom ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)↔\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)\right)$
32 df-isom ${⊢}{{H}}^{-1}{Isom}_{{S},{R}}\left({B},{A}\right)↔\left({{H}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}{S}{w}↔{{H}}^{-1}\left({z}\right){R}{{H}}^{-1}\left({w}\right)\right)\right)$
33 30 31 32 3imtr4i ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)\to {{H}}^{-1}{Isom}_{{S},{R}}\left({B},{A}\right)$