Metamath Proof Explorer

Theorem gicabl

Description: Being Abelian is a group invariant.MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015)

Ref Expression
Assertion gicabl 
|- ( G ~=g H -> ( G e. Abel <-> H e. Abel ) )

Proof

Step Hyp Ref Expression
1 brgic 
 |-  ( G ~=g H <-> ( G GrpIso H ) =/= (/) )
2 n0 
 |-  ( ( G GrpIso H ) =/= (/) <-> E. x x e. ( G GrpIso H ) )
3 gimghm 
 |-  ( x e. ( G GrpIso H ) -> x e. ( G GrpHom H ) )
4 ghmgrp1 
 |-  ( x e. ( G GrpHom H ) -> G e. Grp )
5 3 4 syl 
 |-  ( x e. ( G GrpIso H ) -> G e. Grp )
6 ghmgrp2 
 |-  ( x e. ( G GrpHom H ) -> H e. Grp )
7 3 6 syl 
 |-  ( x e. ( G GrpIso H ) -> H e. Grp )
8 5 7 2thd 
 |-  ( x e. ( G GrpIso H ) -> ( G e. Grp <-> H e. Grp ) )
9 5 grpmndd 
 |-  ( x e. ( G GrpIso H ) -> G e. Mnd )
10 7 grpmndd 
 |-  ( x e. ( G GrpIso H ) -> H e. Mnd )
11 9 10 2thd 
 |-  ( x e. ( G GrpIso H ) -> ( G e. Mnd <-> H e. Mnd ) )
12 eqid 
 |-  ( Base ` G ) = ( Base ` G )
13 eqid 
 |-  ( Base ` H ) = ( Base ` H )
14 12 13 gimf1o 
 |-  ( x e. ( G GrpIso H ) -> x : ( Base ` G ) -1-1-onto-> ( Base ` H ) )
15 f1of1 
 |-  ( x : ( Base ` G ) -1-1-onto-> ( Base ` H ) -> x : ( Base ` G ) -1-1-> ( Base ` H ) )
16 14 15 syl 
 |-  ( x e. ( G GrpIso H ) -> x : ( Base ` G ) -1-1-> ( Base ` H ) )
17 16 adantr 
 |-  ( ( x e. ( G GrpIso H ) /\ ( y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> x : ( Base ` G ) -1-1-> ( Base ` H ) )
18 5 adantr 
 |-  ( ( x e. ( G GrpIso H ) /\ ( y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> G e. Grp )
19 simprl 
 |-  ( ( x e. ( G GrpIso H ) /\ ( y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> y e. ( Base ` G ) )
20 simprr 
 |-  ( ( x e. ( G GrpIso H ) /\ ( y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> z e. ( Base ` G ) )
21 eqid 
 |-  ( +g ` G ) = ( +g ` G )
22 12 21 grpcl 
 |-  ( ( G e. Grp /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) -> ( y ( +g ` G ) z ) e. ( Base ` G ) )
23 18 19 20 22 syl3anc 
 |-  ( ( x e. ( G GrpIso H ) /\ ( y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( y ( +g ` G ) z ) e. ( Base ` G ) )
24 12 21 grpcl 
 |-  ( ( G e. Grp /\ z e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( z ( +g ` G ) y ) e. ( Base ` G ) )
25 18 20 19 24 syl3anc 
 |-  ( ( x e. ( G GrpIso H ) /\ ( y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( z ( +g ` G ) y ) e. ( Base ` G ) )
26 f1fveq 
 |-  ( ( x : ( Base ` G ) -1-1-> ( Base ` H ) /\ ( ( y ( +g ` G ) z ) e. ( Base ` G ) /\ ( z ( +g ` G ) y ) e. ( Base ` G ) ) ) -> ( ( x ` ( y ( +g ` G ) z ) ) = ( x ` ( z ( +g ` G ) y ) ) <-> ( y ( +g ` G ) z ) = ( z ( +g ` G ) y ) ) )
27 17 23 25 26 syl12anc 
 |-  ( ( x e. ( G GrpIso H ) /\ ( y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( ( x ` ( y ( +g ` G ) z ) ) = ( x ` ( z ( +g ` G ) y ) ) <-> ( y ( +g ` G ) z ) = ( z ( +g ` G ) y ) ) )
28 3 adantr 
 |-  ( ( x e. ( G GrpIso H ) /\ ( y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> x e. ( G GrpHom H ) )
29 eqid 
 |-  ( +g ` H ) = ( +g ` H )
30 12 21 29 ghmlin 
 |-  ( ( x e. ( G GrpHom H ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) -> ( x ` ( y ( +g ` G ) z ) ) = ( ( x ` y ) ( +g ` H ) ( x ` z ) ) )
31 28 19 20 30 syl3anc 
 |-  ( ( x e. ( G GrpIso H ) /\ ( y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( x ` ( y ( +g ` G ) z ) ) = ( ( x ` y ) ( +g ` H ) ( x ` z ) ) )
32 12 21 29 ghmlin 
 |-  ( ( x e. ( G GrpHom H ) /\ z e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x ` ( z ( +g ` G ) y ) ) = ( ( x ` z ) ( +g ` H ) ( x ` y ) ) )
33 28 20 19 32 syl3anc 
 |-  ( ( x e. ( G GrpIso H ) /\ ( y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( x ` ( z ( +g ` G ) y ) ) = ( ( x ` z ) ( +g ` H ) ( x ` y ) ) )
34 31 33 eqeq12d 
 |-  ( ( x e. ( G GrpIso H ) /\ ( y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( ( x ` ( y ( +g ` G ) z ) ) = ( x ` ( z ( +g ` G ) y ) ) <-> ( ( x ` y ) ( +g ` H ) ( x ` z ) ) = ( ( x ` z ) ( +g ` H ) ( x ` y ) ) ) )
35 27 34 bitr3d 
 |-  ( ( x e. ( G GrpIso H ) /\ ( y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( ( y ( +g ` G ) z ) = ( z ( +g ` G ) y ) <-> ( ( x ` y ) ( +g ` H ) ( x ` z ) ) = ( ( x ` z ) ( +g ` H ) ( x ` y ) ) ) )
36 35 2ralbidva 
 |-  ( x e. ( G GrpIso H ) -> ( A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( y ( +g ` G ) z ) = ( z ( +g ` G ) y ) <-> A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( ( x ` y ) ( +g ` H ) ( x ` z ) ) = ( ( x ` z ) ( +g ` H ) ( x ` y ) ) ) )
37 f1ofo 
 |-  ( x : ( Base ` G ) -1-1-onto-> ( Base ` H ) -> x : ( Base ` G ) -onto-> ( Base ` H ) )
38 foima 
 |-  ( x : ( Base ` G ) -onto-> ( Base ` H ) -> ( x " ( Base ` G ) ) = ( Base ` H ) )
39 37 38 syl 
 |-  ( x : ( Base ` G ) -1-1-onto-> ( Base ` H ) -> ( x " ( Base ` G ) ) = ( Base ` H ) )
40 14 39 syl 
 |-  ( x e. ( G GrpIso H ) -> ( x " ( Base ` G ) ) = ( Base ` H ) )
41 40 raleqdv 
 |-  ( x e. ( G GrpIso H ) -> ( A. v e. ( x " ( Base ` G ) ) ( ( x ` y ) ( +g ` H ) v ) = ( v ( +g ` H ) ( x ` y ) ) <-> A. v e. ( Base ` H ) ( ( x ` y ) ( +g ` H ) v ) = ( v ( +g ` H ) ( x ` y ) ) ) )
42 f1ofn 
 |-  ( x : ( Base ` G ) -1-1-onto-> ( Base ` H ) -> x Fn ( Base ` G ) )
43 14 42 syl 
 |-  ( x e. ( G GrpIso H ) -> x Fn ( Base ` G ) )
44 ssid 
 |-  ( Base ` G ) C_ ( Base ` G )
45 oveq2 
 |-  ( v = ( x ` z ) -> ( ( x ` y ) ( +g ` H ) v ) = ( ( x ` y ) ( +g ` H ) ( x ` z ) ) )
46 oveq1 
 |-  ( v = ( x ` z ) -> ( v ( +g ` H ) ( x ` y ) ) = ( ( x ` z ) ( +g ` H ) ( x ` y ) ) )
47 45 46 eqeq12d 
 |-  ( v = ( x ` z ) -> ( ( ( x ` y ) ( +g ` H ) v ) = ( v ( +g ` H ) ( x ` y ) ) <-> ( ( x ` y ) ( +g ` H ) ( x ` z ) ) = ( ( x ` z ) ( +g ` H ) ( x ` y ) ) ) )
48 47 ralima 
 |-  ( ( x Fn ( Base ` G ) /\ ( Base ` G ) C_ ( Base ` G ) ) -> ( A. v e. ( x " ( Base ` G ) ) ( ( x ` y ) ( +g ` H ) v ) = ( v ( +g ` H ) ( x ` y ) ) <-> A. z e. ( Base ` G ) ( ( x ` y ) ( +g ` H ) ( x ` z ) ) = ( ( x ` z ) ( +g ` H ) ( x ` y ) ) ) )
49 43 44 48 sylancl 
 |-  ( x e. ( G GrpIso H ) -> ( A. v e. ( x " ( Base ` G ) ) ( ( x ` y ) ( +g ` H ) v ) = ( v ( +g ` H ) ( x ` y ) ) <-> A. z e. ( Base ` G ) ( ( x ` y ) ( +g ` H ) ( x ` z ) ) = ( ( x ` z ) ( +g ` H ) ( x ` y ) ) ) )
50 41 49 bitr3d 
 |-  ( x e. ( G GrpIso H ) -> ( A. v e. ( Base ` H ) ( ( x ` y ) ( +g ` H ) v ) = ( v ( +g ` H ) ( x ` y ) ) <-> A. z e. ( Base ` G ) ( ( x ` y ) ( +g ` H ) ( x ` z ) ) = ( ( x ` z ) ( +g ` H ) ( x ` y ) ) ) )
51 50 ralbidv 
 |-  ( x e. ( G GrpIso H ) -> ( A. y e. ( Base ` G ) A. v e. ( Base ` H ) ( ( x ` y ) ( +g ` H ) v ) = ( v ( +g ` H ) ( x ` y ) ) <-> A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( ( x ` y ) ( +g ` H ) ( x ` z ) ) = ( ( x ` z ) ( +g ` H ) ( x ` y ) ) ) )
52 36 51 bitr4d 
 |-  ( x e. ( G GrpIso H ) -> ( A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( y ( +g ` G ) z ) = ( z ( +g ` G ) y ) <-> A. y e. ( Base ` G ) A. v e. ( Base ` H ) ( ( x ` y ) ( +g ` H ) v ) = ( v ( +g ` H ) ( x ` y ) ) ) )
53 40 raleqdv 
 |-  ( x e. ( G GrpIso H ) -> ( A. w e. ( x " ( Base ` G ) ) A. v e. ( Base ` H ) ( w ( +g ` H ) v ) = ( v ( +g ` H ) w ) <-> A. w e. ( Base ` H ) A. v e. ( Base ` H ) ( w ( +g ` H ) v ) = ( v ( +g ` H ) w ) ) )
54 oveq1 
 |-  ( w = ( x ` y ) -> ( w ( +g ` H ) v ) = ( ( x ` y ) ( +g ` H ) v ) )
55 oveq2 
 |-  ( w = ( x ` y ) -> ( v ( +g ` H ) w ) = ( v ( +g ` H ) ( x ` y ) ) )
56 54 55 eqeq12d 
 |-  ( w = ( x ` y ) -> ( ( w ( +g ` H ) v ) = ( v ( +g ` H ) w ) <-> ( ( x ` y ) ( +g ` H ) v ) = ( v ( +g ` H ) ( x ` y ) ) ) )
57 56 ralbidv 
 |-  ( w = ( x ` y ) -> ( A. v e. ( Base ` H ) ( w ( +g ` H ) v ) = ( v ( +g ` H ) w ) <-> A. v e. ( Base ` H ) ( ( x ` y ) ( +g ` H ) v ) = ( v ( +g ` H ) ( x ` y ) ) ) )
58 57 ralima 
 |-  ( ( x Fn ( Base ` G ) /\ ( Base ` G ) C_ ( Base ` G ) ) -> ( A. w e. ( x " ( Base ` G ) ) A. v e. ( Base ` H ) ( w ( +g ` H ) v ) = ( v ( +g ` H ) w ) <-> A. y e. ( Base ` G ) A. v e. ( Base ` H ) ( ( x ` y ) ( +g ` H ) v ) = ( v ( +g ` H ) ( x ` y ) ) ) )
59 43 44 58 sylancl 
 |-  ( x e. ( G GrpIso H ) -> ( A. w e. ( x " ( Base ` G ) ) A. v e. ( Base ` H ) ( w ( +g ` H ) v ) = ( v ( +g ` H ) w ) <-> A. y e. ( Base ` G ) A. v e. ( Base ` H ) ( ( x ` y ) ( +g ` H ) v ) = ( v ( +g ` H ) ( x ` y ) ) ) )
60 53 59 bitr3d 
 |-  ( x e. ( G GrpIso H ) -> ( A. w e. ( Base ` H ) A. v e. ( Base ` H ) ( w ( +g ` H ) v ) = ( v ( +g ` H ) w ) <-> A. y e. ( Base ` G ) A. v e. ( Base ` H ) ( ( x ` y ) ( +g ` H ) v ) = ( v ( +g ` H ) ( x ` y ) ) ) )
61 52 60 bitr4d 
 |-  ( x e. ( G GrpIso H ) -> ( A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( y ( +g ` G ) z ) = ( z ( +g ` G ) y ) <-> A. w e. ( Base ` H ) A. v e. ( Base ` H ) ( w ( +g ` H ) v ) = ( v ( +g ` H ) w ) ) )
62 11 61 anbi12d 
 |-  ( x e. ( G GrpIso H ) -> ( ( G e. Mnd /\ A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( y ( +g ` G ) z ) = ( z ( +g ` G ) y ) ) <-> ( H e. Mnd /\ A. w e. ( Base ` H ) A. v e. ( Base ` H ) ( w ( +g ` H ) v ) = ( v ( +g ` H ) w ) ) ) )
63 12 21 iscmn 
 |-  ( G e. CMnd <-> ( G e. Mnd /\ A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( y ( +g ` G ) z ) = ( z ( +g ` G ) y ) ) )
64 13 29 iscmn 
 |-  ( H e. CMnd <-> ( H e. Mnd /\ A. w e. ( Base ` H ) A. v e. ( Base ` H ) ( w ( +g ` H ) v ) = ( v ( +g ` H ) w ) ) )
65 62 63 64 3bitr4g 
 |-  ( x e. ( G GrpIso H ) -> ( G e. CMnd <-> H e. CMnd ) )
66 8 65 anbi12d 
 |-  ( x e. ( G GrpIso H ) -> ( ( G e. Grp /\ G e. CMnd ) <-> ( H e. Grp /\ H e. CMnd ) ) )
67 isabl 
 |-  ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )
68 isabl 
 |-  ( H e. Abel <-> ( H e. Grp /\ H e. CMnd ) )
69 66 67 68 3bitr4g 
 |-  ( x e. ( G GrpIso H ) -> ( G e. Abel <-> H e. Abel ) )
70 69 exlimiv 
 |-  ( E. x x e. ( G GrpIso H ) -> ( G e. Abel <-> H e. Abel ) )
71 2 70 sylbi 
 |-  ( ( G GrpIso H ) =/= (/) -> ( G e. Abel <-> H e. Abel ) )
72 1 71 sylbi 
 |-  ( G ~=g H -> ( G e. Abel <-> H e. Abel ) )