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