Step | Hyp | Ref
| Expression |
1 | | brgic 18069 |
. 2
⊢ (𝐺 ≃𝑔
𝐻 ↔ (𝐺 GrpIso 𝐻) ≠ ∅) |
2 | | n0 4162 |
. . 3
⊢ ((𝐺 GrpIso 𝐻) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐺 GrpIso 𝐻)) |
3 | | gimghm 18064 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝑥 ∈ (𝐺 GrpHom 𝐻)) |
4 | | ghmgrp1 18020 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐺 GrpHom 𝐻) → 𝐺 ∈ Grp) |
5 | 3, 4 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝐺 ∈ Grp) |
6 | | ghmgrp2 18021 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐺 GrpHom 𝐻) → 𝐻 ∈ Grp) |
7 | 3, 6 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝐻 ∈ Grp) |
8 | 5, 7 | 2thd 257 |
. . . . . 6
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ Grp ↔ 𝐻 ∈ Grp)) |
9 | | grpmnd 17790 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) |
10 | 5, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝐺 ∈ Mnd) |
11 | | grpmnd 17790 |
. . . . . . . . . 10
⊢ (𝐻 ∈ Grp → 𝐻 ∈ Mnd) |
12 | 7, 11 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝐻 ∈ Mnd) |
13 | 10, 12 | 2thd 257 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ Mnd ↔ 𝐻 ∈ Mnd)) |
14 | | eqid 2825 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝐺) =
(Base‘𝐺) |
15 | | eqid 2825 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝐻) =
(Base‘𝐻) |
16 | 14, 15 | gimf1o 18063 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝑥:(Base‘𝐺)–1-1-onto→(Base‘𝐻)) |
17 | | f1of1 6381 |
. . . . . . . . . . . . . . 15
⊢ (𝑥:(Base‘𝐺)–1-1-onto→(Base‘𝐻) → 𝑥:(Base‘𝐺)–1-1→(Base‘𝐻)) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝑥:(Base‘𝐺)–1-1→(Base‘𝐻)) |
19 | 18 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑥:(Base‘𝐺)–1-1→(Base‘𝐻)) |
20 | 5 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝐺 ∈ Grp) |
21 | | simprl 787 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑦 ∈ (Base‘𝐺)) |
22 | | simprr 789 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑧 ∈ (Base‘𝐺)) |
23 | | eqid 2825 |
. . . . . . . . . . . . . . 15
⊢
(+g‘𝐺) = (+g‘𝐺) |
24 | 14, 23 | grpcl 17791 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺)) → (𝑦(+g‘𝐺)𝑧) ∈ (Base‘𝐺)) |
25 | 20, 21, 22, 24 | syl3anc 1494 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑦(+g‘𝐺)𝑧) ∈ (Base‘𝐺)) |
26 | 14, 23 | grpcl 17791 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑧(+g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
27 | 20, 22, 21, 26 | syl3anc 1494 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑧(+g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
28 | | f1fveq 6779 |
. . . . . . . . . . . . 13
⊢ ((𝑥:(Base‘𝐺)–1-1→(Base‘𝐻) ∧ ((𝑦(+g‘𝐺)𝑧) ∈ (Base‘𝐺) ∧ (𝑧(+g‘𝐺)𝑦) ∈ (Base‘𝐺))) → ((𝑥‘(𝑦(+g‘𝐺)𝑧)) = (𝑥‘(𝑧(+g‘𝐺)𝑦)) ↔ (𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦))) |
29 | 19, 25, 27, 28 | syl12anc 870 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥‘(𝑦(+g‘𝐺)𝑧)) = (𝑥‘(𝑧(+g‘𝐺)𝑦)) ↔ (𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦))) |
30 | 3 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑥 ∈ (𝐺 GrpHom 𝐻)) |
31 | | eqid 2825 |
. . . . . . . . . . . . . . 15
⊢
(+g‘𝐻) = (+g‘𝐻) |
32 | 14, 23, 31 | ghmlin 18023 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺)) → (𝑥‘(𝑦(+g‘𝐺)𝑧)) = ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧))) |
33 | 30, 21, 22, 32 | syl3anc 1494 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥‘(𝑦(+g‘𝐺)𝑧)) = ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧))) |
34 | 14, 23, 31 | ghmlin 18023 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥‘(𝑧(+g‘𝐺)𝑦)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))) |
35 | 30, 22, 21, 34 | syl3anc 1494 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥‘(𝑧(+g‘𝐺)𝑦)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))) |
36 | 33, 35 | eqeq12d 2840 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥‘(𝑦(+g‘𝐺)𝑧)) = (𝑥‘(𝑧(+g‘𝐺)𝑦)) ↔ ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦)))) |
37 | 29, 36 | bitr3d 273 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦) ↔ ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦)))) |
38 | 37 | 2ralbidva 3197 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)(𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦)))) |
39 | | f1ofo 6389 |
. . . . . . . . . . . . . . 15
⊢ (𝑥:(Base‘𝐺)–1-1-onto→(Base‘𝐻) → 𝑥:(Base‘𝐺)–onto→(Base‘𝐻)) |
40 | | foima 6362 |
. . . . . . . . . . . . . . 15
⊢ (𝑥:(Base‘𝐺)–onto→(Base‘𝐻) → (𝑥 “ (Base‘𝐺)) = (Base‘𝐻)) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑥:(Base‘𝐺)–1-1-onto→(Base‘𝐻) → (𝑥 “ (Base‘𝐺)) = (Base‘𝐻)) |
42 | 16, 41 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝑥 “ (Base‘𝐺)) = (Base‘𝐻)) |
43 | 42 | raleqdv 3356 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑣 ∈ (𝑥 “ (Base‘𝐺))((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)))) |
44 | | f1ofn 6383 |
. . . . . . . . . . . . . 14
⊢ (𝑥:(Base‘𝐺)–1-1-onto→(Base‘𝐻) → 𝑥 Fn (Base‘𝐺)) |
45 | 16, 44 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝑥 Fn (Base‘𝐺)) |
46 | | ssid 3848 |
. . . . . . . . . . . . 13
⊢
(Base‘𝐺)
⊆ (Base‘𝐺) |
47 | | oveq2 6918 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = (𝑥‘𝑧) → ((𝑥‘𝑦)(+g‘𝐻)𝑣) = ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧))) |
48 | | oveq1 6917 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = (𝑥‘𝑧) → (𝑣(+g‘𝐻)(𝑥‘𝑦)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))) |
49 | 47, 48 | eqeq12d 2840 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = (𝑥‘𝑧) → (((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦)))) |
50 | 49 | ralima 6759 |
. . . . . . . . . . . . 13
⊢ ((𝑥 Fn (Base‘𝐺) ∧ (Base‘𝐺) ⊆ (Base‘𝐺)) → (∀𝑣 ∈ (𝑥 “ (Base‘𝐺))((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ∀𝑧 ∈ (Base‘𝐺)((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦)))) |
51 | 45, 46, 50 | sylancl 580 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑣 ∈ (𝑥 “ (Base‘𝐺))((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ∀𝑧 ∈ (Base‘𝐺)((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦)))) |
52 | 43, 51 | bitr3d 273 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ∀𝑧 ∈ (Base‘𝐺)((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦)))) |
53 | 52 | ralbidv 3195 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑦 ∈ (Base‘𝐺)∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦)))) |
54 | 38, 53 | bitr4d 274 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)(𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)))) |
55 | 42 | raleqdv 3356 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑤 ∈ (𝑥 “ (Base‘𝐺))∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ∀𝑤 ∈ (Base‘𝐻)∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤))) |
56 | | oveq1 6917 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝑥‘𝑦) → (𝑤(+g‘𝐻)𝑣) = ((𝑥‘𝑦)(+g‘𝐻)𝑣)) |
57 | | oveq2 6918 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝑥‘𝑦) → (𝑣(+g‘𝐻)𝑤) = (𝑣(+g‘𝐻)(𝑥‘𝑦))) |
58 | 56, 57 | eqeq12d 2840 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝑥‘𝑦) → ((𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)))) |
59 | 58 | ralbidv 3195 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝑥‘𝑦) → (∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)))) |
60 | 59 | ralima 6759 |
. . . . . . . . . . 11
⊢ ((𝑥 Fn (Base‘𝐺) ∧ (Base‘𝐺) ⊆ (Base‘𝐺)) → (∀𝑤 ∈ (𝑥 “ (Base‘𝐺))∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)))) |
61 | 45, 46, 60 | sylancl 580 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑤 ∈ (𝑥 “ (Base‘𝐺))∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)))) |
62 | 55, 61 | bitr3d 273 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑤 ∈ (Base‘𝐻)∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)))) |
63 | 54, 62 | bitr4d 274 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)(𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦) ↔ ∀𝑤 ∈ (Base‘𝐻)∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤))) |
64 | 13, 63 | anbi12d 624 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → ((𝐺 ∈ Mnd ∧ ∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)(𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦)) ↔ (𝐻 ∈ Mnd ∧ ∀𝑤 ∈ (Base‘𝐻)∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤)))) |
65 | 14, 23 | iscmn 18560 |
. . . . . . 7
⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)(𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦))) |
66 | 15, 31 | iscmn 18560 |
. . . . . . 7
⊢ (𝐻 ∈ CMnd ↔ (𝐻 ∈ Mnd ∧ ∀𝑤 ∈ (Base‘𝐻)∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤))) |
67 | 64, 65, 66 | 3bitr4g 306 |
. . . . . 6
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ CMnd ↔ 𝐻 ∈ CMnd)) |
68 | 8, 67 | anbi12d 624 |
. . . . 5
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → ((𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd) ↔ (𝐻 ∈ Grp ∧ 𝐻 ∈ CMnd))) |
69 | | isabl 18557 |
. . . . 5
⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) |
70 | | isabl 18557 |
. . . . 5
⊢ (𝐻 ∈ Abel ↔ (𝐻 ∈ Grp ∧ 𝐻 ∈ CMnd)) |
71 | 68, 69, 70 | 3bitr4g 306 |
. . . 4
⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel)) |
72 | 71 | exlimiv 2029 |
. . 3
⊢
(∃𝑥 𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel)) |
73 | 2, 72 | sylbi 209 |
. 2
⊢ ((𝐺 GrpIso 𝐻) ≠ ∅ → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel)) |
74 | 1, 73 | sylbi 209 |
1
⊢ (𝐺 ≃𝑔
𝐻 → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel)) |