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≃𝑔H→G∈Abel↔H∈Abel

Proof

Step Hyp Ref Expression
1 brgic ⊢G≃𝑔H↔GGrpIsoH≠∅
2 n0 ⊢GGrpIsoH≠∅↔∃xx∈GGrpIsoH
3 gimghm ⊢x∈GGrpIsoH→x∈GGrpHomH
4 ghmgrp1 ⊢x∈GGrpHomH→G∈Grp
5 3 4 syl ⊢x∈GGrpIsoH→G∈Grp
6 ghmgrp2 ⊢x∈GGrpHomH→H∈Grp
7 3 6 syl ⊢x∈GGrpIsoH→H∈Grp
8 5 7 2thd ⊢x∈GGrpIsoH→G∈Grp↔H∈Grp
9 5 grpmndd ⊢x∈GGrpIsoH→G∈Mnd
10 7 grpmndd ⊢x∈GGrpIsoH→H∈Mnd
11 9 10 2thd ⊢x∈GGrpIsoH→G∈Mnd↔H∈Mnd
12 eqid ⊢BaseG=BaseG
13 eqid ⊢BaseH=BaseH
14 12 13 gimf1o ⊢x∈GGrpIsoH→x:BaseG⟶1-1 ontoBaseH
15 f1of1 ⊢x:BaseG⟶1-1 ontoBaseH→x:BaseG⟶1-1BaseH
16 14 15 syl ⊢x∈GGrpIsoH→x:BaseG⟶1-1BaseH
17 16 adantr ⊢x∈GGrpIsoH∧y∈BaseG∧z∈BaseG→x:BaseG⟶1-1BaseH
18 5 adantr ⊢x∈GGrpIsoH∧y∈BaseG∧z∈BaseG→G∈Grp
19 simprl ⊢x∈GGrpIsoH∧y∈BaseG∧z∈BaseG→y∈BaseG
20 simprr ⊢x∈GGrpIsoH∧y∈BaseG∧z∈BaseG→z∈BaseG
21 eqid ⊢+G=+G
22 12 21 grpcl ⊢G∈Grp∧y∈BaseG∧z∈BaseG→y+Gz∈BaseG
23 18 19 20 22 syl3anc ⊢x∈GGrpIsoH∧y∈BaseG∧z∈BaseG→y+Gz∈BaseG
24 12 21 grpcl ⊢G∈Grp∧z∈BaseG∧y∈BaseG→z+Gy∈BaseG
25 18 20 19 24 syl3anc ⊢x∈GGrpIsoH∧y∈BaseG∧z∈BaseG→z+Gy∈BaseG
26 f1fveq ⊢x:BaseG⟶1-1BaseH∧y+Gz∈BaseG∧z+Gy∈BaseG→x⁡y+Gz=x⁡z+Gy↔y+Gz=z+Gy
27 17 23 25 26 syl12anc ⊢x∈GGrpIsoH∧y∈BaseG∧z∈BaseG→x⁡y+Gz=x⁡z+Gy↔y+Gz=z+Gy
28 3 adantr ⊢x∈GGrpIsoH∧y∈BaseG∧z∈BaseG→x∈GGrpHomH
29 eqid ⊢+H=+H
30 12 21 29 ghmlin ⊢x∈GGrpHomH∧y∈BaseG∧z∈BaseG→x⁡y+Gz=x⁡y+Hx⁡z
31 28 19 20 30 syl3anc ⊢x∈GGrpIsoH∧y∈BaseG∧z∈BaseG→x⁡y+Gz=x⁡y+Hx⁡z
32 12 21 29 ghmlin ⊢x∈GGrpHomH∧z∈BaseG∧y∈BaseG→x⁡z+Gy=x⁡z+Hx⁡y
33 28 20 19 32 syl3anc ⊢x∈GGrpIsoH∧y∈BaseG∧z∈BaseG→x⁡z+Gy=x⁡z+Hx⁡y
34 31 33 eqeq12d ⊢x∈GGrpIsoH∧y∈BaseG∧z∈BaseG→x⁡y+Gz=x⁡z+Gy↔x⁡y+Hx⁡z=x⁡z+Hx⁡y
35 27 34 bitr3d ⊢x∈GGrpIsoH∧y∈BaseG∧z∈BaseG→y+Gz=z+Gy↔x⁡y+Hx⁡z=x⁡z+Hx⁡y
36 35 2ralbidva ⊢x∈GGrpIsoH→∀y∈BaseG∀z∈BaseGy+Gz=z+Gy↔∀y∈BaseG∀z∈BaseGx⁡y+Hx⁡z=x⁡z+Hx⁡y
37 f1ofo ⊢x:BaseG⟶1-1 ontoBaseH→x:BaseG⟶ontoBaseH
38 foima ⊢x:BaseG⟶ontoBaseH→xBaseG=BaseH
39 37 38 syl ⊢x:BaseG⟶1-1 ontoBaseH→xBaseG=BaseH
40 14 39 syl ⊢x∈GGrpIsoH→xBaseG=BaseH
41 40 raleqdv ⊢x∈GGrpIsoH→∀v∈xBaseGx⁡y+Hv=v+Hx⁡y↔∀v∈BaseHx⁡y+Hv=v+Hx⁡y
42 f1ofn ⊢x:BaseG⟶1-1 ontoBaseH→xFnBaseG
43 14 42 syl ⊢x∈GGrpIsoH→xFnBaseG
44 ssid ⊢BaseG⊆BaseG
45 oveq2 ⊢v=x⁡z→x⁡y+Hv=x⁡y+Hx⁡z
46 oveq1 ⊢v=x⁡z→v+Hx⁡y=x⁡z+Hx⁡y
47 45 46 eqeq12d ⊢v=x⁡z→x⁡y+Hv=v+Hx⁡y↔x⁡y+Hx⁡z=x⁡z+Hx⁡y
48 47 ralima ⊢xFnBaseG∧BaseG⊆BaseG→∀v∈xBaseGx⁡y+Hv=v+Hx⁡y↔∀z∈BaseGx⁡y+Hx⁡z=x⁡z+Hx⁡y
49 43 44 48 sylancl ⊢x∈GGrpIsoH→∀v∈xBaseGx⁡y+Hv=v+Hx⁡y↔∀z∈BaseGx⁡y+Hx⁡z=x⁡z+Hx⁡y
50 41 49 bitr3d ⊢x∈GGrpIsoH→∀v∈BaseHx⁡y+Hv=v+Hx⁡y↔∀z∈BaseGx⁡y+Hx⁡z=x⁡z+Hx⁡y
51 50 ralbidv ⊢x∈GGrpIsoH→∀y∈BaseG∀v∈BaseHx⁡y+Hv=v+Hx⁡y↔∀y∈BaseG∀z∈BaseGx⁡y+Hx⁡z=x⁡z+Hx⁡y
52 36 51 bitr4d ⊢x∈GGrpIsoH→∀y∈BaseG∀z∈BaseGy+Gz=z+Gy↔∀y∈BaseG∀v∈BaseHx⁡y+Hv=v+Hx⁡y
53 40 raleqdv ⊢x∈GGrpIsoH→∀w∈xBaseG∀v∈BaseHw+Hv=v+Hw↔∀w∈BaseH∀v∈BaseHw+Hv=v+Hw
54 oveq1 ⊢w=x⁡y→w+Hv=x⁡y+Hv
55 oveq2 ⊢w=x⁡y→v+Hw=v+Hx⁡y
56 54 55 eqeq12d ⊢w=x⁡y→w+Hv=v+Hw↔x⁡y+Hv=v+Hx⁡y
57 56 ralbidv ⊢w=x⁡y→∀v∈BaseHw+Hv=v+Hw↔∀v∈BaseHx⁡y+Hv=v+Hx⁡y
58 57 ralima ⊢xFnBaseG∧BaseG⊆BaseG→∀w∈xBaseG∀v∈BaseHw+Hv=v+Hw↔∀y∈BaseG∀v∈BaseHx⁡y+Hv=v+Hx⁡y
59 43 44 58 sylancl ⊢x∈GGrpIsoH→∀w∈xBaseG∀v∈BaseHw+Hv=v+Hw↔∀y∈BaseG∀v∈BaseHx⁡y+Hv=v+Hx⁡y
60 53 59 bitr3d ⊢x∈GGrpIsoH→∀w∈BaseH∀v∈BaseHw+Hv=v+Hw↔∀y∈BaseG∀v∈BaseHx⁡y+Hv=v+Hx⁡y
61 52 60 bitr4d ⊢x∈GGrpIsoH→∀y∈BaseG∀z∈BaseGy+Gz=z+Gy↔∀w∈BaseH∀v∈BaseHw+Hv=v+Hw
62 11 61 anbi12d ⊢x∈GGrpIsoH→G∈Mnd∧∀y∈BaseG∀z∈BaseGy+Gz=z+Gy↔H∈Mnd∧∀w∈BaseH∀v∈BaseHw+Hv=v+Hw
63 12 21 iscmn ⊢G∈CMnd↔G∈Mnd∧∀y∈BaseG∀z∈BaseGy+Gz=z+Gy
64 13 29 iscmn ⊢H∈CMnd↔H∈Mnd∧∀w∈BaseH∀v∈BaseHw+Hv=v+Hw
65 62 63 64 3bitr4g ⊢x∈GGrpIsoH→G∈CMnd↔H∈CMnd
66 8 65 anbi12d ⊢x∈GGrpIsoH→G∈Grp∧G∈CMnd↔H∈Grp∧H∈CMnd
67 isabl ⊢G∈Abel↔G∈Grp∧G∈CMnd
68 isabl ⊢H∈Abel↔H∈Grp∧H∈CMnd
69 66 67 68 3bitr4g ⊢x∈GGrpIsoH→G∈Abel↔H∈Abel
70 69 exlimiv ⊢∃xx∈GGrpIsoH→G∈Abel↔H∈Abel
71 2 70 sylbi ⊢GGrpIsoH≠∅→G∈Abel↔H∈Abel
72 1 71 sylbi ⊢G≃𝑔H→G∈Abel↔H∈Abel