Metamath Proof Explorer

Theorem abliso

Description: The image of an Abelian group by a group isomorphism is also Abelian. (Contributed by Thierry Arnoux, 8-Mar-2018)

Ref Expression
Assertion abliso 
|- ( ( M e. Abel /\ F e. ( M GrpIso N ) ) -> N e. Abel )

Proof

Step Hyp Ref Expression
1 gimghm 
 |-  ( F e. ( M GrpIso N ) -> F e. ( M GrpHom N ) )
2 ghmgrp2 
 |-  ( F e. ( M GrpHom N ) -> N e. Grp )
3 1 2 syl 
 |-  ( F e. ( M GrpIso N ) -> N e. Grp )
4 3 adantl 
 |-  ( ( M e. Abel /\ F e. ( M GrpIso N ) ) -> N e. Grp )
5 4 grpmndd 
 |-  ( ( M e. Abel /\ F e. ( M GrpIso N ) ) -> N e. Mnd )
6 simpll 
 |-  ( ( ( M e. Abel /\ F e. ( M GrpIso N ) ) /\ ( x e. ( Base ` N ) /\ y e. ( Base ` N ) ) ) -> M e. Abel )
7 eqid 
 |-  ( Base ` M ) = ( Base ` M )
8 eqid 
 |-  ( Base ` N ) = ( Base ` N )
9 7 8 gimf1o 
 |-  ( F e. ( M GrpIso N ) -> F : ( Base ` M ) -1-1-onto-> ( Base ` N ) )
10 f1ocnv 
 |-  ( F : ( Base ` M ) -1-1-onto-> ( Base ` N ) -> `' F : ( Base ` N ) -1-1-onto-> ( Base ` M ) )
11 f1of 
 |-  ( `' F : ( Base ` N ) -1-1-onto-> ( Base ` M ) -> `' F : ( Base ` N ) --> ( Base ` M ) )
12 9 10 11 3syl 
 |-  ( F e. ( M GrpIso N ) -> `' F : ( Base ` N ) --> ( Base ` M ) )
13 12 ad2antlr 
 |-  ( ( ( M e. Abel /\ F e. ( M GrpIso N ) ) /\ ( x e. ( Base ` N ) /\ y e. ( Base ` N ) ) ) -> `' F : ( Base ` N ) --> ( Base ` M ) )
14 simprl 
 |-  ( ( ( M e. Abel /\ F e. ( M GrpIso N ) ) /\ ( x e. ( Base ` N ) /\ y e. ( Base ` N ) ) ) -> x e. ( Base ` N ) )
15 13 14 ffvelcdmd 
 |-  ( ( ( M e. Abel /\ F e. ( M GrpIso N ) ) /\ ( x e. ( Base ` N ) /\ y e. ( Base ` N ) ) ) -> ( `' F ` x ) e. ( Base ` M ) )
16 simprr 
 |-  ( ( ( M e. Abel /\ F e. ( M GrpIso N ) ) /\ ( x e. ( Base ` N ) /\ y e. ( Base ` N ) ) ) -> y e. ( Base ` N ) )
17 13 16 ffvelcdmd 
 |-  ( ( ( M e. Abel /\ F e. ( M GrpIso N ) ) /\ ( x e. ( Base ` N ) /\ y e. ( Base ` N ) ) ) -> ( `' F ` y ) e. ( Base ` M ) )
18 eqid 
 |-  ( +g ` M ) = ( +g ` M )
19 7 18 ablcom 
 |-  ( ( M e. Abel /\ ( `' F ` x ) e. ( Base ` M ) /\ ( `' F ` y ) e. ( Base ` M ) ) -> ( ( `' F ` x ) ( +g ` M ) ( `' F ` y ) ) = ( ( `' F ` y ) ( +g ` M ) ( `' F ` x ) ) )
20 6 15 17 19 syl3anc 
 |-  ( ( ( M e. Abel /\ F e. ( M GrpIso N ) ) /\ ( x e. ( Base ` N ) /\ y e. ( Base ` N ) ) ) -> ( ( `' F ` x ) ( +g ` M ) ( `' F ` y ) ) = ( ( `' F ` y ) ( +g ` M ) ( `' F ` x ) ) )
21 gimcnv 
 |-  ( F e. ( M GrpIso N ) -> `' F e. ( N GrpIso M ) )
22 21 ad2antlr 
 |-  ( ( ( M e. Abel /\ F e. ( M GrpIso N ) ) /\ ( x e. ( Base ` N ) /\ y e. ( Base ` N ) ) ) -> `' F e. ( N GrpIso M ) )
23 gimghm 
 |-  ( `' F e. ( N GrpIso M ) -> `' F e. ( N GrpHom M ) )
24 22 23 syl 
 |-  ( ( ( M e. Abel /\ F e. ( M GrpIso N ) ) /\ ( x e. ( Base ` N ) /\ y e. ( Base ` N ) ) ) -> `' F e. ( N GrpHom M ) )
25 eqid 
 |-  ( +g ` N ) = ( +g ` N )
26 8 25 18 ghmlin 
 |-  ( ( `' F e. ( N GrpHom M ) /\ x e. ( Base ` N ) /\ y e. ( Base ` N ) ) -> ( `' F ` ( x ( +g ` N ) y ) ) = ( ( `' F ` x ) ( +g ` M ) ( `' F ` y ) ) )
27 24 14 16 26 syl3anc 
 |-  ( ( ( M e. Abel /\ F e. ( M GrpIso N ) ) /\ ( x e. ( Base ` N ) /\ y e. ( Base ` N ) ) ) -> ( `' F ` ( x ( +g ` N ) y ) ) = ( ( `' F ` x ) ( +g ` M ) ( `' F ` y ) ) )
28 8 25 18 ghmlin 
 |-  ( ( `' F e. ( N GrpHom M ) /\ y e. ( Base ` N ) /\ x e. ( Base ` N ) ) -> ( `' F ` ( y ( +g ` N ) x ) ) = ( ( `' F ` y ) ( +g ` M ) ( `' F ` x ) ) )
29 24 16 14 28 syl3anc 
 |-  ( ( ( M e. Abel /\ F e. ( M GrpIso N ) ) /\ ( x e. ( Base ` N ) /\ y e. ( Base ` N ) ) ) -> ( `' F ` ( y ( +g ` N ) x ) ) = ( ( `' F ` y ) ( +g ` M ) ( `' F ` x ) ) )
30 20 27 29 3eqtr4d 
 |-  ( ( ( M e. Abel /\ F e. ( M GrpIso N ) ) /\ ( x e. ( Base ` N ) /\ y e. ( Base ` N ) ) ) -> ( `' F ` ( x ( +g ` N ) y ) ) = ( `' F ` ( y ( +g ` N ) x ) ) )
31 30 fveq2d 
 |-  ( ( ( M e. Abel /\ F e. ( M GrpIso N ) ) /\ ( x e. ( Base ` N ) /\ y e. ( Base ` N ) ) ) -> ( F ` ( `' F ` ( x ( +g ` N ) y ) ) ) = ( F ` ( `' F ` ( y ( +g ` N ) x ) ) ) )
32 9 ad2antlr 
 |-  ( ( ( M e. Abel /\ F e. ( M GrpIso N ) ) /\ ( x e. ( Base ` N ) /\ y e. ( Base ` N ) ) ) -> F : ( Base ` M ) -1-1-onto-> ( Base ` N ) )
33 3 ad2antlr 
 |-  ( ( ( M e. Abel /\ F e. ( M GrpIso N ) ) /\ ( x e. ( Base ` N ) /\ y e. ( Base ` N ) ) ) -> N e. Grp )
34 8 25 grpcl 
 |-  ( ( N e. Grp /\ x e. ( Base ` N ) /\ y e. ( Base ` N ) ) -> ( x ( +g ` N ) y ) e. ( Base ` N ) )
35 33 14 16 34 syl3anc 
 |-  ( ( ( M e. Abel /\ F e. ( M GrpIso N ) ) /\ ( x e. ( Base ` N ) /\ y e. ( Base ` N ) ) ) -> ( x ( +g ` N ) y ) e. ( Base ` N ) )
36 f1ocnvfv2 
 |-  ( ( F : ( Base ` M ) -1-1-onto-> ( Base ` N ) /\ ( x ( +g ` N ) y ) e. ( Base ` N ) ) -> ( F ` ( `' F ` ( x ( +g ` N ) y ) ) ) = ( x ( +g ` N ) y ) )
37 32 35 36 syl2anc 
 |-  ( ( ( M e. Abel /\ F e. ( M GrpIso N ) ) /\ ( x e. ( Base ` N ) /\ y e. ( Base ` N ) ) ) -> ( F ` ( `' F ` ( x ( +g ` N ) y ) ) ) = ( x ( +g ` N ) y ) )
38 8 25 grpcl 
 |-  ( ( N e. Grp /\ y e. ( Base ` N ) /\ x e. ( Base ` N ) ) -> ( y ( +g ` N ) x ) e. ( Base ` N ) )
39 33 16 14 38 syl3anc 
 |-  ( ( ( M e. Abel /\ F e. ( M GrpIso N ) ) /\ ( x e. ( Base ` N ) /\ y e. ( Base ` N ) ) ) -> ( y ( +g ` N ) x ) e. ( Base ` N ) )
40 f1ocnvfv2 
 |-  ( ( F : ( Base ` M ) -1-1-onto-> ( Base ` N ) /\ ( y ( +g ` N ) x ) e. ( Base ` N ) ) -> ( F ` ( `' F ` ( y ( +g ` N ) x ) ) ) = ( y ( +g ` N ) x ) )
41 32 39 40 syl2anc 
 |-  ( ( ( M e. Abel /\ F e. ( M GrpIso N ) ) /\ ( x e. ( Base ` N ) /\ y e. ( Base ` N ) ) ) -> ( F ` ( `' F ` ( y ( +g ` N ) x ) ) ) = ( y ( +g ` N ) x ) )
42 31 37 41 3eqtr3d 
 |-  ( ( ( M e. Abel /\ F e. ( M GrpIso N ) ) /\ ( x e. ( Base ` N ) /\ y e. ( Base ` N ) ) ) -> ( x ( +g ` N ) y ) = ( y ( +g ` N ) x ) )
43 42 ralrimivva 
 |-  ( ( M e. Abel /\ F e. ( M GrpIso N ) ) -> A. x e. ( Base ` N ) A. y e. ( Base ` N ) ( x ( +g ` N ) y ) = ( y ( +g ` N ) x ) )
44 8 25 iscmn 
 |-  ( N e. CMnd <-> ( N e. Mnd /\ A. x e. ( Base ` N ) A. y e. ( Base ` N ) ( x ( +g ` N ) y ) = ( y ( +g ` N ) x ) ) )
45 5 43 44 sylanbrc 
 |-  ( ( M e. Abel /\ F e. ( M GrpIso N ) ) -> N e. CMnd )
46 isabl 
 |-  ( N e. Abel <-> ( N e. Grp /\ N e. CMnd ) )
47 4 45 46 sylanbrc 
 |-  ( ( M e. Abel /\ F e. ( M GrpIso N ) ) -> N e. Abel )