Metamath Proof Explorer

Theorem ghmf1o

Description: A bijective group homomorphism is an isomorphism. (Contributed by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses ghmf1o.x 
|- X = ( Base ` S )
ghmf1o.y 
|- Y = ( Base ` T )
Assertion ghmf1o 
|- ( F e. ( S GrpHom T ) -> ( F : X -1-1-onto-> Y <-> `' F e. ( T GrpHom S ) ) )

Proof

Step Hyp Ref Expression
1 ghmf1o.x 
 |-  X = ( Base ` S )
2 ghmf1o.y 
 |-  Y = ( Base ` T )
3 ghmgrp2 
 |-  ( F e. ( S GrpHom T ) -> T e. Grp )
4 ghmgrp1 
 |-  ( F e. ( S GrpHom T ) -> S e. Grp )
5 3 4 jca 
 |-  ( F e. ( S GrpHom T ) -> ( T e. Grp /\ S e. Grp ) )
6 5 adantr 
 |-  ( ( F e. ( S GrpHom T ) /\ F : X -1-1-onto-> Y ) -> ( T e. Grp /\ S e. Grp ) )
7 f1ocnv 
 |-  ( F : X -1-1-onto-> Y -> `' F : Y -1-1-onto-> X )
8 7 adantl 
 |-  ( ( F e. ( S GrpHom T ) /\ F : X -1-1-onto-> Y ) -> `' F : Y -1-1-onto-> X )
9 f1of 
 |-  ( `' F : Y -1-1-onto-> X -> `' F : Y --> X )
10 8 9 syl 
 |-  ( ( F e. ( S GrpHom T ) /\ F : X -1-1-onto-> Y ) -> `' F : Y --> X )
11 simpll 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-onto-> Y ) /\ ( x e. Y /\ y e. Y ) ) -> F e. ( S GrpHom T ) )
12 10 adantr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-onto-> Y ) /\ ( x e. Y /\ y e. Y ) ) -> `' F : Y --> X )
13 simprl 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-onto-> Y ) /\ ( x e. Y /\ y e. Y ) ) -> x e. Y )
14 12 13 ffvelrnd 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-onto-> Y ) /\ ( x e. Y /\ y e. Y ) ) -> ( `' F ` x ) e. X )
15 simprr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-onto-> Y ) /\ ( x e. Y /\ y e. Y ) ) -> y e. Y )
16 12 15 ffvelrnd 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-onto-> Y ) /\ ( x e. Y /\ y e. Y ) ) -> ( `' F ` y ) e. X )
17 eqid 
 |-  ( +g ` S ) = ( +g ` S )
18 eqid 
 |-  ( +g ` T ) = ( +g ` T )
19 1 17 18 ghmlin 
 |-  ( ( F e. ( S GrpHom T ) /\ ( `' F ` x ) e. X /\ ( `' F ` y ) e. X ) -> ( F ` ( ( `' F ` x ) ( +g ` S ) ( `' F ` y ) ) ) = ( ( F ` ( `' F ` x ) ) ( +g ` T ) ( F ` ( `' F ` y ) ) ) )
20 11 14 16 19 syl3anc 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-onto-> Y ) /\ ( x e. Y /\ y e. Y ) ) -> ( F ` ( ( `' F ` x ) ( +g ` S ) ( `' F ` y ) ) ) = ( ( F ` ( `' F ` x ) ) ( +g ` T ) ( F ` ( `' F ` y ) ) ) )
21 simplr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-onto-> Y ) /\ ( x e. Y /\ y e. Y ) ) -> F : X -1-1-onto-> Y )
22 f1ocnvfv2 
 |-  ( ( F : X -1-1-onto-> Y /\ x e. Y ) -> ( F ` ( `' F ` x ) ) = x )
23 21 13 22 syl2anc 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-onto-> Y ) /\ ( x e. Y /\ y e. Y ) ) -> ( F ` ( `' F ` x ) ) = x )
24 f1ocnvfv2 
 |-  ( ( F : X -1-1-onto-> Y /\ y e. Y ) -> ( F ` ( `' F ` y ) ) = y )
25 21 15 24 syl2anc 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-onto-> Y ) /\ ( x e. Y /\ y e. Y ) ) -> ( F ` ( `' F ` y ) ) = y )
26 23 25 oveq12d 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-onto-> Y ) /\ ( x e. Y /\ y e. Y ) ) -> ( ( F ` ( `' F ` x ) ) ( +g ` T ) ( F ` ( `' F ` y ) ) ) = ( x ( +g ` T ) y ) )
27 20 26 eqtrd 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-onto-> Y ) /\ ( x e. Y /\ y e. Y ) ) -> ( F ` ( ( `' F ` x ) ( +g ` S ) ( `' F ` y ) ) ) = ( x ( +g ` T ) y ) )
28 11 4 syl 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-onto-> Y ) /\ ( x e. Y /\ y e. Y ) ) -> S e. Grp )
29 1 17 grpcl 
 |-  ( ( S e. Grp /\ ( `' F ` x ) e. X /\ ( `' F ` y ) e. X ) -> ( ( `' F ` x ) ( +g ` S ) ( `' F ` y ) ) e. X )
30 28 14 16 29 syl3anc 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-onto-> Y ) /\ ( x e. Y /\ y e. Y ) ) -> ( ( `' F ` x ) ( +g ` S ) ( `' F ` y ) ) e. X )
31 f1ocnvfv 
 |-  ( ( F : X -1-1-onto-> Y /\ ( ( `' F ` x ) ( +g ` S ) ( `' F ` y ) ) e. X ) -> ( ( F ` ( ( `' F ` x ) ( +g ` S ) ( `' F ` y ) ) ) = ( x ( +g ` T ) y ) -> ( `' F ` ( x ( +g ` T ) y ) ) = ( ( `' F ` x ) ( +g ` S ) ( `' F ` y ) ) ) )
32 21 30 31 syl2anc 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-onto-> Y ) /\ ( x e. Y /\ y e. Y ) ) -> ( ( F ` ( ( `' F ` x ) ( +g ` S ) ( `' F ` y ) ) ) = ( x ( +g ` T ) y ) -> ( `' F ` ( x ( +g ` T ) y ) ) = ( ( `' F ` x ) ( +g ` S ) ( `' F ` y ) ) ) )
33 27 32 mpd 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-onto-> Y ) /\ ( x e. Y /\ y e. Y ) ) -> ( `' F ` ( x ( +g ` T ) y ) ) = ( ( `' F ` x ) ( +g ` S ) ( `' F ` y ) ) )
34 33 ralrimivva 
 |-  ( ( F e. ( S GrpHom T ) /\ F : X -1-1-onto-> Y ) -> A. x e. Y A. y e. Y ( `' F ` ( x ( +g ` T ) y ) ) = ( ( `' F ` x ) ( +g ` S ) ( `' F ` y ) ) )
35 10 34 jca 
 |-  ( ( F e. ( S GrpHom T ) /\ F : X -1-1-onto-> Y ) -> ( `' F : Y --> X /\ A. x e. Y A. y e. Y ( `' F ` ( x ( +g ` T ) y ) ) = ( ( `' F ` x ) ( +g ` S ) ( `' F ` y ) ) ) )
36 2 1 18 17 isghm 
 |-  ( `' F e. ( T GrpHom S ) <-> ( ( T e. Grp /\ S e. Grp ) /\ ( `' F : Y --> X /\ A. x e. Y A. y e. Y ( `' F ` ( x ( +g ` T ) y ) ) = ( ( `' F ` x ) ( +g ` S ) ( `' F ` y ) ) ) ) )
37 6 35 36 sylanbrc 
 |-  ( ( F e. ( S GrpHom T ) /\ F : X -1-1-onto-> Y ) -> `' F e. ( T GrpHom S ) )
38 1 2 ghmf 
 |-  ( F e. ( S GrpHom T ) -> F : X --> Y )
39 38 adantr 
 |-  ( ( F e. ( S GrpHom T ) /\ `' F e. ( T GrpHom S ) ) -> F : X --> Y )
40 39 ffnd 
 |-  ( ( F e. ( S GrpHom T ) /\ `' F e. ( T GrpHom S ) ) -> F Fn X )
41 2 1 ghmf 
 |-  ( `' F e. ( T GrpHom S ) -> `' F : Y --> X )
42 41 adantl 
 |-  ( ( F e. ( S GrpHom T ) /\ `' F e. ( T GrpHom S ) ) -> `' F : Y --> X )
43 42 ffnd 
 |-  ( ( F e. ( S GrpHom T ) /\ `' F e. ( T GrpHom S ) ) -> `' F Fn Y )
44 dff1o4 
 |-  ( F : X -1-1-onto-> Y <-> ( F Fn X /\ `' F Fn Y ) )
45 40 43 44 sylanbrc 
 |-  ( ( F e. ( S GrpHom T ) /\ `' F e. ( T GrpHom S ) ) -> F : X -1-1-onto-> Y )
46 37 45 impbida 
 |-  ( F e. ( S GrpHom T ) -> ( F : X -1-1-onto-> Y <-> `' F e. ( T GrpHom S ) ) )