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 e. ( R MgmHom S ) -> ( F : B -1-1-onto-> C <-> `' F e. ( S MgmHom R ) ) )

Proof

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