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 = Base R
mgmhmf1o.c C = Base S
Assertion mgmhmf1o F R MgmHom S F : B 1-1 onto C F -1 S MgmHom R

Proof

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