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 ↔ G GrpIso H ≠ ∅
2 n0 ⊢ G GrpIso H ≠ ∅ ↔ ∃ x x ∈ G GrpIso H
3 gimghm ⊢ x ∈ G GrpIso H → x ∈ G GrpHom H
4 ghmgrp1 ⊢ x ∈ G GrpHom H → G ∈ Grp
5 3 4 syl ⊢ x ∈ G GrpIso H → G ∈ Grp
6 ghmgrp2 ⊢ x ∈ G GrpHom H → H ∈ Grp
7 3 6 syl ⊢ x ∈ G GrpIso H → H ∈ Grp
8 5 7 2thd ⊢ x ∈ G GrpIso H → G ∈ Grp ↔ H ∈ Grp
9 5 grpmndd ⊢ x ∈ G GrpIso H → G ∈ Mnd
10 7 grpmndd ⊢ x ∈ G GrpIso H → H ∈ Mnd
11 9 10 2thd ⊢ x ∈ G GrpIso H → G ∈ Mnd ↔ H ∈ Mnd
12 eqid ⊢ Base G = Base G
13 eqid ⊢ Base H = Base H
14 12 13 gimf1o ⊢ x ∈ 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 ∈ G GrpIso H → x : Base G ⟶ 1-1 Base H
17 16 adantr ⊢ x ∈ G GrpIso H ∧ y ∈ Base G ∧ z ∈ Base G → x : Base G ⟶ 1-1 Base H
18 5 adantr ⊢ x ∈ G GrpIso H ∧ y ∈ Base G ∧ z ∈ Base G → G ∈ Grp
19 simprl ⊢ x ∈ G GrpIso H ∧ y ∈ Base G ∧ z ∈ Base G → y ∈ Base G
20 simprr ⊢ x ∈ G GrpIso H ∧ y ∈ Base G ∧ z ∈ Base G → z ∈ Base G
21 eqid ⊢ + G = + G
22 12 21 grpcl ⊢ G ∈ Grp ∧ y ∈ Base G ∧ z ∈ Base G → y + G z ∈ Base G
23 18 19 20 22 syl3anc ⊢ x ∈ G GrpIso H ∧ y ∈ Base G ∧ z ∈ Base G → y + G z ∈ Base G
24 12 21 grpcl ⊢ G ∈ Grp ∧ z ∈ Base G ∧ y ∈ Base G → z + G y ∈ Base G
25 18 20 19 24 syl3anc ⊢ x ∈ G GrpIso H ∧ y ∈ Base G ∧ z ∈ Base G → z + G y ∈ Base G
26 f1fveq ⊢ x : Base G ⟶ 1-1 Base H ∧ y + G z ∈ Base G ∧ z + G y ∈ Base G → x ⁡ y + G z = x ⁡ z + G y ↔ y + G z = z + G y
27 17 23 25 26 syl12anc ⊢ x ∈ G GrpIso H ∧ y ∈ Base G ∧ z ∈ Base G → x ⁡ y + G z = x ⁡ z + G y ↔ y + G z = z + G y
28 3 adantr ⊢ x ∈ G GrpIso H ∧ y ∈ Base G ∧ z ∈ Base G → x ∈ G GrpHom H
29 eqid ⊢ + H = + H
30 12 21 29 ghmlin ⊢ x ∈ G GrpHom H ∧ y ∈ Base G ∧ z ∈ Base G → x ⁡ y + G z = x ⁡ y + H x ⁡ z
31 28 19 20 30 syl3anc ⊢ x ∈ G GrpIso H ∧ y ∈ Base G ∧ z ∈ Base G → x ⁡ y + G z = x ⁡ y + H x ⁡ z
32 12 21 29 ghmlin ⊢ x ∈ G GrpHom H ∧ z ∈ Base G ∧ y ∈ Base G → x ⁡ z + G y = x ⁡ z + H x ⁡ y
33 28 20 19 32 syl3anc ⊢ x ∈ G GrpIso H ∧ y ∈ Base G ∧ z ∈ Base G → x ⁡ z + G y = x ⁡ z + H x ⁡ y
34 31 33 eqeq12d ⊢ x ∈ G GrpIso H ∧ y ∈ Base G ∧ z ∈ Base G → x ⁡ y + G z = x ⁡ z + G y ↔ x ⁡ y + H x ⁡ z = x ⁡ z + H x ⁡ y
35 27 34 bitr3d ⊢ x ∈ G GrpIso H ∧ y ∈ Base G ∧ z ∈ Base G → y + G z = z + G y ↔ x ⁡ y + H x ⁡ z = x ⁡ z + H x ⁡ y
36 35 2ralbidva ⊢ x ∈ G GrpIso H → ∀ y ∈ Base G ∀ z ∈ Base G y + G z = z + G y ↔ ∀ y ∈ Base G ∀ z ∈ Base G x ⁡ y + H x ⁡ z = x ⁡ z + 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 ∈ G GrpIso H → x Base G = Base H
41 40 raleqdv ⊢ x ∈ G GrpIso H → ∀ v ∈ x Base G x ⁡ y + H v = v + H x ⁡ y ↔ ∀ v ∈ Base H x ⁡ y + H v = v + H x ⁡ y
42 f1ofn ⊢ x : Base G ⟶ 1-1 onto Base H → x Fn Base G
43 14 42 syl ⊢ x ∈ G GrpIso H → x Fn Base G
44 ssid ⊢ Base G ⊆ Base G
45 oveq2 ⊢ v = x ⁡ z → x ⁡ y + H v = x ⁡ y + H x ⁡ z
46 oveq1 ⊢ v = x ⁡ z → v + H x ⁡ y = x ⁡ z + H x ⁡ y
47 45 46 eqeq12d ⊢ v = x ⁡ z → x ⁡ y + H v = v + H x ⁡ y ↔ x ⁡ y + H x ⁡ z = x ⁡ z + H x ⁡ y
48 47 ralima ⊢ x Fn Base G ∧ Base G ⊆ Base G → ∀ v ∈ x Base G x ⁡ y + H v = v + H x ⁡ y ↔ ∀ z ∈ Base G x ⁡ y + H x ⁡ z = x ⁡ z + H x ⁡ y
49 43 44 48 sylancl ⊢ x ∈ G GrpIso H → ∀ v ∈ x Base G x ⁡ y + H v = v + H x ⁡ y ↔ ∀ z ∈ Base G x ⁡ y + H x ⁡ z = x ⁡ z + H x ⁡ y
50 41 49 bitr3d ⊢ x ∈ G GrpIso H → ∀ v ∈ Base H x ⁡ y + H v = v + H x ⁡ y ↔ ∀ z ∈ Base G x ⁡ y + H x ⁡ z = x ⁡ z + H x ⁡ y
51 50 ralbidv ⊢ x ∈ G GrpIso H → ∀ y ∈ Base G ∀ v ∈ Base H x ⁡ y + H v = v + H x ⁡ y ↔ ∀ y ∈ Base G ∀ z ∈ Base G x ⁡ y + H x ⁡ z = x ⁡ z + H x ⁡ y
52 36 51 bitr4d ⊢ x ∈ G GrpIso H → ∀ y ∈ Base G ∀ z ∈ Base G y + G z = z + G y ↔ ∀ y ∈ Base G ∀ v ∈ Base H x ⁡ y + H v = v + H x ⁡ y
53 40 raleqdv ⊢ x ∈ G GrpIso H → ∀ w ∈ x Base G ∀ v ∈ Base H w + H v = v + H w ↔ ∀ w ∈ Base H ∀ v ∈ Base H w + H v = v + H w
54 oveq1 ⊢ w = x ⁡ y → w + H v = x ⁡ y + H v
55 oveq2 ⊢ w = x ⁡ y → v + H w = v + H x ⁡ y
56 54 55 eqeq12d ⊢ w = x ⁡ y → w + H v = v + H w ↔ x ⁡ y + H v = v + H x ⁡ y
57 56 ralbidv ⊢ w = x ⁡ y → ∀ v ∈ Base H w + H v = v + H w ↔ ∀ v ∈ Base H x ⁡ y + H v = v + H x ⁡ y
58 57 ralima ⊢ x Fn Base G ∧ Base G ⊆ Base G → ∀ w ∈ x Base G ∀ v ∈ Base H w + H v = v + H w ↔ ∀ y ∈ Base G ∀ v ∈ Base H x ⁡ y + H v = v + H x ⁡ y
59 43 44 58 sylancl ⊢ x ∈ G GrpIso H → ∀ w ∈ x Base G ∀ v ∈ Base H w + H v = v + H w ↔ ∀ y ∈ Base G ∀ v ∈ Base H x ⁡ y + H v = v + H x ⁡ y
60 53 59 bitr3d ⊢ x ∈ G GrpIso H → ∀ w ∈ Base H ∀ v ∈ Base H w + H v = v + H w ↔ ∀ y ∈ Base G ∀ v ∈ Base H x ⁡ y + H v = v + H x ⁡ y
61 52 60 bitr4d ⊢ x ∈ G GrpIso H → ∀ y ∈ Base G ∀ z ∈ Base G y + G z = z + G y ↔ ∀ w ∈ Base H ∀ v ∈ Base H w + H v = v + H w
62 11 61 anbi12d ⊢ x ∈ G GrpIso H → G ∈ Mnd ∧ ∀ y ∈ Base G ∀ z ∈ Base G y + G z = z + G y ↔ H ∈ Mnd ∧ ∀ w ∈ Base H ∀ v ∈ Base H w + H v = v + H w
63 12 21 iscmn ⊢ G ∈ CMnd ↔ G ∈ Mnd ∧ ∀ y ∈ Base G ∀ z ∈ Base G y + G z = z + G y
64 13 29 iscmn ⊢ H ∈ CMnd ↔ H ∈ Mnd ∧ ∀ w ∈ Base H ∀ v ∈ Base H w + H v = v + H w
65 62 63 64 3bitr4g ⊢ x ∈ G GrpIso H → G ∈ CMnd ↔ H ∈ CMnd
66 8 65 anbi12d ⊢ x ∈ G GrpIso H → 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 ∈ G GrpIso H → G ∈ Abel ↔ H ∈ Abel
70 69 exlimiv ⊢ ∃ x x ∈ G GrpIso H → G ∈ Abel ↔ H ∈ Abel
71 2 70 sylbi ⊢ G GrpIso H ≠ ∅ → G ∈ Abel ↔ H ∈ Abel
72 1 71 sylbi ⊢ G ≃ 𝑔 H → G ∈ Abel ↔ H ∈ Abel