Metamath Proof Explorer

Theorem mhmf1o

Description: A monoid homomorphism is bijective iff its converse is also a monoid homomorphism. (Contributed by AV, 22-Oct-2019)

Ref Expression
Hypotheses mhmf1o.b 
|- B = ( Base ` R )
mhmf1o.c 
|- C = ( Base ` S )
Assertion mhmf1o 
|- ( F e. ( R MndHom S ) -> ( F : B -1-1-onto-> C <-> `' F e. ( S MndHom R ) ) )

Proof

Step Hyp Ref Expression
1 mhmf1o.b 
 |-  B = ( Base ` R )
2 mhmf1o.c 
 |-  C = ( Base ` S )
3 mhmrcl2 
 |-  ( F e. ( R MndHom S ) -> S e. Mnd )
4 mhmrcl1 
 |-  ( F e. ( R MndHom S ) -> R e. Mnd )
5 3 4 jca 
 |-  ( F e. ( R MndHom S ) -> ( S e. Mnd /\ R e. Mnd ) )
6 5 adantr 
 |-  ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) -> ( S e. Mnd /\ R e. Mnd ) )
7 f1ocnv 
 |-  ( F : B -1-1-onto-> C -> `' F : C -1-1-onto-> B )
8 7 adantl 
 |-  ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) -> `' F : C -1-1-onto-> B )
9 f1of 
 |-  ( `' F : C -1-1-onto-> B -> `' F : C --> B )
10 8 9 syl 
 |-  ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) -> `' F : C --> B )
11 simpll 
 |-  ( ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) /\ ( x e. C /\ y e. C ) ) -> F e. ( R MndHom S ) )
12 10 adantr 
 |-  ( ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) /\ ( x e. C /\ y e. C ) ) -> `' F : C --> B )
13 simprl 
 |-  ( ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) /\ ( x e. C /\ y e. C ) ) -> x e. C )
14 12 13 ffvelrnd 
 |-  ( ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) /\ ( x e. C /\ y e. C ) ) -> ( `' F ` x ) e. B )
15 simprr 
 |-  ( ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) /\ ( x e. C /\ y e. C ) ) -> y e. C )
16 12 15 ffvelrnd 
 |-  ( ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) /\ ( x e. C /\ y e. C ) ) -> ( `' F ` y ) e. B )
17 eqid 
 |-  ( +g ` R ) = ( +g ` R )
18 eqid 
 |-  ( +g ` S ) = ( +g ` S )
19 1 17 18 mhmlin 
 |-  ( ( F e. ( R MndHom S ) /\ ( `' F ` x ) e. B /\ ( `' F ` y ) e. B ) -> ( F ` ( ( `' F ` x ) ( +g ` R ) ( `' F ` y ) ) ) = ( ( F ` ( `' F ` x ) ) ( +g ` S ) ( F ` ( `' F ` y ) ) ) )
20 11 14 16 19 syl3anc 
 |-  ( ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) /\ ( x e. C /\ y e. C ) ) -> ( F ` ( ( `' F ` x ) ( +g ` R ) ( `' F ` y ) ) ) = ( ( F ` ( `' F ` x ) ) ( +g ` S ) ( F ` ( `' F ` y ) ) ) )
21 simpr 
 |-  ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) -> F : B -1-1-onto-> C )
22 21 adantr 
 |-  ( ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) /\ ( x e. C /\ y e. C ) ) -> F : B -1-1-onto-> C )
23 f1ocnvfv2 
 |-  ( ( F : B -1-1-onto-> C /\ x e. C ) -> ( F ` ( `' F ` x ) ) = x )
24 22 13 23 syl2anc 
 |-  ( ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) /\ ( x e. C /\ y e. C ) ) -> ( F ` ( `' F ` x ) ) = x )
25 f1ocnvfv2 
 |-  ( ( F : B -1-1-onto-> C /\ y e. C ) -> ( F ` ( `' F ` y ) ) = y )
26 22 15 25 syl2anc 
 |-  ( ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) /\ ( x e. C /\ y e. C ) ) -> ( F ` ( `' F ` y ) ) = y )
27 24 26 oveq12d 
 |-  ( ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) /\ ( x e. C /\ y e. C ) ) -> ( ( F ` ( `' F ` x ) ) ( +g ` S ) ( F ` ( `' F ` y ) ) ) = ( x ( +g ` S ) y ) )
28 20 27 eqtrd 
 |-  ( ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) /\ ( x e. C /\ y e. C ) ) -> ( F ` ( ( `' F ` x ) ( +g ` R ) ( `' F ` y ) ) ) = ( x ( +g ` S ) y ) )
29 4 adantr 
 |-  ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) -> R e. Mnd )
30 29 adantr 
 |-  ( ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) /\ ( x e. C /\ y e. C ) ) -> R e. Mnd )
31 1 17 mndcl 
 |-  ( ( R e. Mnd /\ ( `' F ` x ) e. B /\ ( `' F ` y ) e. B ) -> ( ( `' F ` x ) ( +g ` R ) ( `' F ` y ) ) e. B )
32 30 14 16 31 syl3anc 
 |-  ( ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) /\ ( x e. C /\ y e. C ) ) -> ( ( `' F ` x ) ( +g ` R ) ( `' F ` y ) ) e. B )
33 f1ocnvfv 
 |-  ( ( F : B -1-1-onto-> C /\ ( ( `' F ` x ) ( +g ` R ) ( `' F ` y ) ) e. B ) -> ( ( F ` ( ( `' F ` x ) ( +g ` R ) ( `' F ` y ) ) ) = ( x ( +g ` S ) y ) -> ( `' F ` ( x ( +g ` S ) y ) ) = ( ( `' F ` x ) ( +g ` R ) ( `' F ` y ) ) ) )
34 22 32 33 syl2anc 
 |-  ( ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) /\ ( x e. C /\ y e. C ) ) -> ( ( F ` ( ( `' F ` x ) ( +g ` R ) ( `' F ` y ) ) ) = ( x ( +g ` S ) y ) -> ( `' F ` ( x ( +g ` S ) y ) ) = ( ( `' F ` x ) ( +g ` R ) ( `' F ` y ) ) ) )
35 28 34 mpd 
 |-  ( ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) /\ ( x e. C /\ y e. C ) ) -> ( `' F ` ( x ( +g ` S ) y ) ) = ( ( `' F ` x ) ( +g ` R ) ( `' F ` y ) ) )
36 35 ralrimivva 
 |-  ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) -> A. x e. C A. y e. C ( `' F ` ( x ( +g ` S ) y ) ) = ( ( `' F ` x ) ( +g ` R ) ( `' F ` y ) ) )
37 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
38 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
39 37 38 mhm0 
 |-  ( F e. ( R MndHom S ) -> ( F ` ( 0g ` R ) ) = ( 0g ` S ) )
40 39 adantr 
 |-  ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) -> ( F ` ( 0g ` R ) ) = ( 0g ` S ) )
41 40 eqcomd 
 |-  ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) -> ( 0g ` S ) = ( F ` ( 0g ` R ) ) )
42 41 fveq2d 
 |-  ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) -> ( `' F ` ( 0g ` S ) ) = ( `' F ` ( F ` ( 0g ` R ) ) ) )
43 1 37 mndidcl 
 |-  ( R e. Mnd -> ( 0g ` R ) e. B )
44 4 43 syl 
 |-  ( F e. ( R MndHom S ) -> ( 0g ` R ) e. B )
45 44 adantr 
 |-  ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) -> ( 0g ` R ) e. B )
46 f1ocnvfv1 
 |-  ( ( F : B -1-1-onto-> C /\ ( 0g ` R ) e. B ) -> ( `' F ` ( F ` ( 0g ` R ) ) ) = ( 0g ` R ) )
47 21 45 46 syl2anc 
 |-  ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) -> ( `' F ` ( F ` ( 0g ` R ) ) ) = ( 0g ` R ) )
48 42 47 eqtrd 
 |-  ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) -> ( `' F ` ( 0g ` S ) ) = ( 0g ` R ) )
49 10 36 48 3jca 
 |-  ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) -> ( `' F : C --> B /\ A. x e. C A. y e. C ( `' F ` ( x ( +g ` S ) y ) ) = ( ( `' F ` x ) ( +g ` R ) ( `' F ` y ) ) /\ ( `' F ` ( 0g ` S ) ) = ( 0g ` R ) ) )
50 2 1 18 17 38 37 ismhm 
 |-  ( `' F e. ( S MndHom R ) <-> ( ( S e. Mnd /\ R e. Mnd ) /\ ( `' F : C --> B /\ A. x e. C A. y e. C ( `' F ` ( x ( +g ` S ) y ) ) = ( ( `' F ` x ) ( +g ` R ) ( `' F ` y ) ) /\ ( `' F ` ( 0g ` S ) ) = ( 0g ` R ) ) ) )
51 6 49 50 sylanbrc 
 |-  ( ( F e. ( R MndHom S ) /\ F : B -1-1-onto-> C ) -> `' F e. ( S MndHom R ) )
52 1 2 mhmf 
 |-  ( F e. ( R MndHom S ) -> F : B --> C )
53 52 adantr 
 |-  ( ( F e. ( R MndHom S ) /\ `' F e. ( S MndHom R ) ) -> F : B --> C )
54 53 ffnd 
 |-  ( ( F e. ( R MndHom S ) /\ `' F e. ( S MndHom R ) ) -> F Fn B )
55 2 1 mhmf 
 |-  ( `' F e. ( S MndHom R ) -> `' F : C --> B )
56 55 adantl 
 |-  ( ( F e. ( R MndHom S ) /\ `' F e. ( S MndHom R ) ) -> `' F : C --> B )
57 56 ffnd 
 |-  ( ( F e. ( R MndHom S ) /\ `' F e. ( S MndHom R ) ) -> `' F Fn C )
58 dff1o4 
 |-  ( F : B -1-1-onto-> C <-> ( F Fn B /\ `' F Fn C ) )
59 54 57 58 sylanbrc 
 |-  ( ( F e. ( R MndHom S ) /\ `' F e. ( S MndHom R ) ) -> F : B -1-1-onto-> C )
60 51 59 impbida 
 |-  ( F e. ( R MndHom S ) -> ( F : B -1-1-onto-> C <-> `' F e. ( S MndHom R ) ) )