# Metamath Proof Explorer

## Theorem mgmhmf1o

Description: A magma homomorphism is bijective iff its converse is also a magma homomorphism. (Contributed by AV, 25-Feb-2020)

Ref Expression
Hypotheses mgmhmf1o.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
mgmhmf1o.c ${⊢}{C}={\mathrm{Base}}_{{S}}$
Assertion mgmhmf1o ${⊢}{F}\in \left({R}\mathrm{MgmHom}{S}\right)\to \left({F}:{B}\underset{1-1 onto}{⟶}{C}↔{{F}}^{-1}\in \left({S}\mathrm{MgmHom}{R}\right)\right)$

### Proof

Step Hyp Ref Expression
1 mgmhmf1o.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
2 mgmhmf1o.c ${⊢}{C}={\mathrm{Base}}_{{S}}$
3 mgmhmrcl ${⊢}{F}\in \left({R}\mathrm{MgmHom}{S}\right)\to \left({R}\in \mathrm{Mgm}\wedge {S}\in \mathrm{Mgm}\right)$
4 3 ancomd ${⊢}{F}\in \left({R}\mathrm{MgmHom}{S}\right)\to \left({S}\in \mathrm{Mgm}\wedge {R}\in \mathrm{Mgm}\right)$
5 4 adantr ${⊢}\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\to \left({S}\in \mathrm{Mgm}\wedge {R}\in \mathrm{Mgm}\right)$
6 f1ocnv ${⊢}{F}:{B}\underset{1-1 onto}{⟶}{C}\to {{F}}^{-1}:{C}\underset{1-1 onto}{⟶}{B}$
7 6 adantl ${⊢}\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\to {{F}}^{-1}:{C}\underset{1-1 onto}{⟶}{B}$
8 f1of ${⊢}{{F}}^{-1}:{C}\underset{1-1 onto}{⟶}{B}\to {{F}}^{-1}:{C}⟶{B}$
9 7 8 syl ${⊢}\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\to {{F}}^{-1}:{C}⟶{B}$
10 simpll ${⊢}\left(\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {F}\in \left({R}\mathrm{MgmHom}{S}\right)$
11 9 adantr ${⊢}\left(\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {{F}}^{-1}:{C}⟶{B}$
12 simprl ${⊢}\left(\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {x}\in {C}$
13 11 12 ffvelrnd ${⊢}\left(\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {{F}}^{-1}\left({x}\right)\in {B}$
14 simprr ${⊢}\left(\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {y}\in {C}$
15 11 14 ffvelrnd ${⊢}\left(\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {{F}}^{-1}\left({y}\right)\in {B}$
16 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
17 eqid ${⊢}{+}_{{S}}={+}_{{S}}$
18 1 16 17 mgmhmlin ${⊢}\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {{F}}^{-1}\left({x}\right)\in {B}\wedge {{F}}^{-1}\left({y}\right)\in {B}\right)\to {F}\left({{F}}^{-1}\left({x}\right){+}_{{R}}{{F}}^{-1}\left({y}\right)\right)={F}\left({{F}}^{-1}\left({x}\right)\right){+}_{{S}}{F}\left({{F}}^{-1}\left({y}\right)\right)$
19 10 13 15 18 syl3anc ${⊢}\left(\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {F}\left({{F}}^{-1}\left({x}\right){+}_{{R}}{{F}}^{-1}\left({y}\right)\right)={F}\left({{F}}^{-1}\left({x}\right)\right){+}_{{S}}{F}\left({{F}}^{-1}\left({y}\right)\right)$
20 simplr ${⊢}\left(\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {F}:{B}\underset{1-1 onto}{⟶}{C}$
21 f1ocnvfv2 ${⊢}\left({F}:{B}\underset{1-1 onto}{⟶}{C}\wedge {x}\in {C}\right)\to {F}\left({{F}}^{-1}\left({x}\right)\right)={x}$
22 20 12 21 syl2anc ${⊢}\left(\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {F}\left({{F}}^{-1}\left({x}\right)\right)={x}$
23 f1ocnvfv2 ${⊢}\left({F}:{B}\underset{1-1 onto}{⟶}{C}\wedge {y}\in {C}\right)\to {F}\left({{F}}^{-1}\left({y}\right)\right)={y}$
24 20 14 23 syl2anc ${⊢}\left(\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {F}\left({{F}}^{-1}\left({y}\right)\right)={y}$
25 22 24 oveq12d ${⊢}\left(\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {F}\left({{F}}^{-1}\left({x}\right)\right){+}_{{S}}{F}\left({{F}}^{-1}\left({y}\right)\right)={x}{+}_{{S}}{y}$
26 19 25 eqtrd ${⊢}\left(\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {F}\left({{F}}^{-1}\left({x}\right){+}_{{R}}{{F}}^{-1}\left({y}\right)\right)={x}{+}_{{S}}{y}$
27 3 simpld ${⊢}{F}\in \left({R}\mathrm{MgmHom}{S}\right)\to {R}\in \mathrm{Mgm}$
28 27 adantr ${⊢}\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\to {R}\in \mathrm{Mgm}$
29 28 adantr ${⊢}\left(\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {R}\in \mathrm{Mgm}$
30 1 16 mgmcl ${⊢}\left({R}\in \mathrm{Mgm}\wedge {{F}}^{-1}\left({x}\right)\in {B}\wedge {{F}}^{-1}\left({y}\right)\in {B}\right)\to {{F}}^{-1}\left({x}\right){+}_{{R}}{{F}}^{-1}\left({y}\right)\in {B}$
31 29 13 15 30 syl3anc ${⊢}\left(\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {{F}}^{-1}\left({x}\right){+}_{{R}}{{F}}^{-1}\left({y}\right)\in {B}$
32 f1ocnvfv ${⊢}\left({F}:{B}\underset{1-1 onto}{⟶}{C}\wedge {{F}}^{-1}\left({x}\right){+}_{{R}}{{F}}^{-1}\left({y}\right)\in {B}\right)\to \left({F}\left({{F}}^{-1}\left({x}\right){+}_{{R}}{{F}}^{-1}\left({y}\right)\right)={x}{+}_{{S}}{y}\to {{F}}^{-1}\left({x}{+}_{{S}}{y}\right)={{F}}^{-1}\left({x}\right){+}_{{R}}{{F}}^{-1}\left({y}\right)\right)$
33 20 31 32 syl2anc ${⊢}\left(\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to \left({F}\left({{F}}^{-1}\left({x}\right){+}_{{R}}{{F}}^{-1}\left({y}\right)\right)={x}{+}_{{S}}{y}\to {{F}}^{-1}\left({x}{+}_{{S}}{y}\right)={{F}}^{-1}\left({x}\right){+}_{{R}}{{F}}^{-1}\left({y}\right)\right)$
34 26 33 mpd ${⊢}\left(\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {{F}}^{-1}\left({x}{+}_{{S}}{y}\right)={{F}}^{-1}\left({x}\right){+}_{{R}}{{F}}^{-1}\left({y}\right)$
35 34 ralrimivva ${⊢}\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\to \forall {x}\in {C}\phantom{\rule{.4em}{0ex}}\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left({x}{+}_{{S}}{y}\right)={{F}}^{-1}\left({x}\right){+}_{{R}}{{F}}^{-1}\left({y}\right)$
36 9 35 jca ${⊢}\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\to \left({{F}}^{-1}:{C}⟶{B}\wedge \forall {x}\in {C}\phantom{\rule{.4em}{0ex}}\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left({x}{+}_{{S}}{y}\right)={{F}}^{-1}\left({x}\right){+}_{{R}}{{F}}^{-1}\left({y}\right)\right)$
37 2 1 17 16 ismgmhm ${⊢}{{F}}^{-1}\in \left({S}\mathrm{MgmHom}{R}\right)↔\left(\left({S}\in \mathrm{Mgm}\wedge {R}\in \mathrm{Mgm}\right)\wedge \left({{F}}^{-1}:{C}⟶{B}\wedge \forall {x}\in {C}\phantom{\rule{.4em}{0ex}}\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left({x}{+}_{{S}}{y}\right)={{F}}^{-1}\left({x}\right){+}_{{R}}{{F}}^{-1}\left({y}\right)\right)\right)$
38 5 36 37 sylanbrc ${⊢}\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {F}:{B}\underset{1-1 onto}{⟶}{C}\right)\to {{F}}^{-1}\in \left({S}\mathrm{MgmHom}{R}\right)$
39 1 2 mgmhmf ${⊢}{F}\in \left({R}\mathrm{MgmHom}{S}\right)\to {F}:{B}⟶{C}$
40 39 adantr ${⊢}\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {{F}}^{-1}\in \left({S}\mathrm{MgmHom}{R}\right)\right)\to {F}:{B}⟶{C}$
41 40 ffnd ${⊢}\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {{F}}^{-1}\in \left({S}\mathrm{MgmHom}{R}\right)\right)\to {F}Fn{B}$
42 2 1 mgmhmf ${⊢}{{F}}^{-1}\in \left({S}\mathrm{MgmHom}{R}\right)\to {{F}}^{-1}:{C}⟶{B}$
43 42 adantl ${⊢}\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {{F}}^{-1}\in \left({S}\mathrm{MgmHom}{R}\right)\right)\to {{F}}^{-1}:{C}⟶{B}$
44 43 ffnd ${⊢}\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {{F}}^{-1}\in \left({S}\mathrm{MgmHom}{R}\right)\right)\to {{F}}^{-1}Fn{C}$
45 dff1o4 ${⊢}{F}:{B}\underset{1-1 onto}{⟶}{C}↔\left({F}Fn{B}\wedge {{F}}^{-1}Fn{C}\right)$
46 41 44 45 sylanbrc ${⊢}\left({F}\in \left({R}\mathrm{MgmHom}{S}\right)\wedge {{F}}^{-1}\in \left({S}\mathrm{MgmHom}{R}\right)\right)\to {F}:{B}\underset{1-1 onto}{⟶}{C}$
47 38 46 impbida ${⊢}{F}\in \left({R}\mathrm{MgmHom}{S}\right)\to \left({F}:{B}\underset{1-1 onto}{⟶}{C}↔{{F}}^{-1}\in \left({S}\mathrm{MgmHom}{R}\right)\right)$