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