Metamath Proof Explorer

Theorem imasgim

Description: A relabeling of the elements of a group induces an isomorphism to the relabeled group.MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015) (Revised by Mario Carneiro, 11-Aug-2015)

Ref Expression
Hypotheses imasgim.u 
|- ( ph -> U = ( F "s R ) )
imasgim.v 
|- ( ph -> V = ( Base ` R ) )
imasgim.f 
|- ( ph -> F : V -1-1-onto-> B )
imasgim.r 
|- ( ph -> R e. Grp )
Assertion imasgim 
|- ( ph -> F e. ( R GrpIso U ) )

Proof

Step Hyp Ref Expression
1 imasgim.u 
 |-  ( ph -> U = ( F "s R ) )
2 imasgim.v 
 |-  ( ph -> V = ( Base ` R ) )
3 imasgim.f 
 |-  ( ph -> F : V -1-1-onto-> B )
4 imasgim.r 
 |-  ( ph -> R e. Grp )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 eqid 
 |-  ( Base ` U ) = ( Base ` U )
7 eqid 
 |-  ( +g ` R ) = ( +g ` R )
8 eqid 
 |-  ( +g ` U ) = ( +g ` U )
9 eqidd 
 |-  ( ph -> ( +g ` R ) = ( +g ` R ) )
10 f1ofo 
 |-  ( F : V -1-1-onto-> B -> F : V -onto-> B )
11 3 10 syl 
 |-  ( ph -> F : V -onto-> B )
12 3 f1ocpbl 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) /\ ( c e. V /\ d e. V ) ) -> ( ( ( F ` a ) = ( F ` c ) /\ ( F ` b ) = ( F ` d ) ) -> ( F ` ( a ( +g ` R ) b ) ) = ( F ` ( c ( +g ` R ) d ) ) ) )
13 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
14 1 2 9 11 12 4 13 imasgrp 
 |-  ( ph -> ( U e. Grp /\ ( F ` ( 0g ` R ) ) = ( 0g ` U ) ) )
15 14 simpld 
 |-  ( ph -> U e. Grp )
16 1 2 11 4 imasbas 
 |-  ( ph -> B = ( Base ` U ) )
17 f1oeq3 
 |-  ( B = ( Base ` U ) -> ( F : V -1-1-onto-> B <-> F : V -1-1-onto-> ( Base ` U ) ) )
18 16 17 syl 
 |-  ( ph -> ( F : V -1-1-onto-> B <-> F : V -1-1-onto-> ( Base ` U ) ) )
19 3 18 mpbid 
 |-  ( ph -> F : V -1-1-onto-> ( Base ` U ) )
20 2 f1oeq2d 
 |-  ( ph -> ( F : V -1-1-onto-> ( Base ` U ) <-> F : ( Base ` R ) -1-1-onto-> ( Base ` U ) ) )
21 19 20 mpbid 
 |-  ( ph -> F : ( Base ` R ) -1-1-onto-> ( Base ` U ) )
22 f1of 
 |-  ( F : ( Base ` R ) -1-1-onto-> ( Base ` U ) -> F : ( Base ` R ) --> ( Base ` U ) )
23 21 22 syl 
 |-  ( ph -> F : ( Base ` R ) --> ( Base ` U ) )
24 2 eleq2d 
 |-  ( ph -> ( a e. V <-> a e. ( Base ` R ) ) )
25 2 eleq2d 
 |-  ( ph -> ( b e. V <-> b e. ( Base ` R ) ) )
26 24 25 anbi12d 
 |-  ( ph -> ( ( a e. V /\ b e. V ) <-> ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) )
27 11 12 1 2 4 7 8 imasaddval 
 |-  ( ( ph /\ a e. V /\ b e. V ) -> ( ( F ` a ) ( +g ` U ) ( F ` b ) ) = ( F ` ( a ( +g ` R ) b ) ) )
28 27 eqcomd 
 |-  ( ( ph /\ a e. V /\ b e. V ) -> ( F ` ( a ( +g ` R ) b ) ) = ( ( F ` a ) ( +g ` U ) ( F ` b ) ) )
29 28 3expib 
 |-  ( ph -> ( ( a e. V /\ b e. V ) -> ( F ` ( a ( +g ` R ) b ) ) = ( ( F ` a ) ( +g ` U ) ( F ` b ) ) ) )
30 26 29 sylbird 
 |-  ( ph -> ( ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) -> ( F ` ( a ( +g ` R ) b ) ) = ( ( F ` a ) ( +g ` U ) ( F ` b ) ) ) )
31 30 imp 
 |-  ( ( ph /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) -> ( F ` ( a ( +g ` R ) b ) ) = ( ( F ` a ) ( +g ` U ) ( F ` b ) ) )
32 5 6 7 8 4 15 23 31 isghmd 
 |-  ( ph -> F e. ( R GrpHom U ) )
33 5 6 isgim 
 |-  ( F e. ( R GrpIso U ) <-> ( F e. ( R GrpHom U ) /\ F : ( Base ` R ) -1-1-onto-> ( Base ` U ) ) )
34 32 21 33 sylanbrc 
 |-  ( ph -> F e. ( R GrpIso U ) )