Step | Hyp | Ref
| Expression |
1 | | gimghm 18878 |
. . . 4
⊢ (𝐹 ∈ (𝑀 GrpIso 𝑁) → 𝐹 ∈ (𝑀 GrpHom 𝑁)) |
2 | | ghmgrp2 18835 |
. . . 4
⊢ (𝐹 ∈ (𝑀 GrpHom 𝑁) → 𝑁 ∈ Grp) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝐹 ∈ (𝑀 GrpIso 𝑁) → 𝑁 ∈ Grp) |
4 | 3 | adantl 482 |
. 2
⊢ ((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) → 𝑁 ∈ Grp) |
5 | 4 | grpmndd 18587 |
. . 3
⊢ ((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) → 𝑁 ∈ Mnd) |
6 | | simpll 764 |
. . . . . . . 8
⊢ (((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) ∧ (𝑥 ∈ (Base‘𝑁) ∧ 𝑦 ∈ (Base‘𝑁))) → 𝑀 ∈ Abel) |
7 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(Base‘𝑀) =
(Base‘𝑀) |
8 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(Base‘𝑁) =
(Base‘𝑁) |
9 | 7, 8 | gimf1o 18877 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑀 GrpIso 𝑁) → 𝐹:(Base‘𝑀)–1-1-onto→(Base‘𝑁)) |
10 | | f1ocnv 6730 |
. . . . . . . . . . 11
⊢ (𝐹:(Base‘𝑀)–1-1-onto→(Base‘𝑁) → ◡𝐹:(Base‘𝑁)–1-1-onto→(Base‘𝑀)) |
11 | | f1of 6718 |
. . . . . . . . . . 11
⊢ (◡𝐹:(Base‘𝑁)–1-1-onto→(Base‘𝑀) → ◡𝐹:(Base‘𝑁)⟶(Base‘𝑀)) |
12 | 9, 10, 11 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝑀 GrpIso 𝑁) → ◡𝐹:(Base‘𝑁)⟶(Base‘𝑀)) |
13 | 12 | ad2antlr 724 |
. . . . . . . . 9
⊢ (((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) ∧ (𝑥 ∈ (Base‘𝑁) ∧ 𝑦 ∈ (Base‘𝑁))) → ◡𝐹:(Base‘𝑁)⟶(Base‘𝑀)) |
14 | | simprl 768 |
. . . . . . . . 9
⊢ (((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) ∧ (𝑥 ∈ (Base‘𝑁) ∧ 𝑦 ∈ (Base‘𝑁))) → 𝑥 ∈ (Base‘𝑁)) |
15 | 13, 14 | ffvelrnd 6964 |
. . . . . . . 8
⊢ (((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) ∧ (𝑥 ∈ (Base‘𝑁) ∧ 𝑦 ∈ (Base‘𝑁))) → (◡𝐹‘𝑥) ∈ (Base‘𝑀)) |
16 | | simprr 770 |
. . . . . . . . 9
⊢ (((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) ∧ (𝑥 ∈ (Base‘𝑁) ∧ 𝑦 ∈ (Base‘𝑁))) → 𝑦 ∈ (Base‘𝑁)) |
17 | 13, 16 | ffvelrnd 6964 |
. . . . . . . 8
⊢ (((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) ∧ (𝑥 ∈ (Base‘𝑁) ∧ 𝑦 ∈ (Base‘𝑁))) → (◡𝐹‘𝑦) ∈ (Base‘𝑀)) |
18 | | eqid 2738 |
. . . . . . . . 9
⊢
(+g‘𝑀) = (+g‘𝑀) |
19 | 7, 18 | ablcom 19402 |
. . . . . . . 8
⊢ ((𝑀 ∈ Abel ∧ (◡𝐹‘𝑥) ∈ (Base‘𝑀) ∧ (◡𝐹‘𝑦) ∈ (Base‘𝑀)) → ((◡𝐹‘𝑥)(+g‘𝑀)(◡𝐹‘𝑦)) = ((◡𝐹‘𝑦)(+g‘𝑀)(◡𝐹‘𝑥))) |
20 | 6, 15, 17, 19 | syl3anc 1370 |
. . . . . . 7
⊢ (((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) ∧ (𝑥 ∈ (Base‘𝑁) ∧ 𝑦 ∈ (Base‘𝑁))) → ((◡𝐹‘𝑥)(+g‘𝑀)(◡𝐹‘𝑦)) = ((◡𝐹‘𝑦)(+g‘𝑀)(◡𝐹‘𝑥))) |
21 | | gimcnv 18881 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝑀 GrpIso 𝑁) → ◡𝐹 ∈ (𝑁 GrpIso 𝑀)) |
22 | 21 | ad2antlr 724 |
. . . . . . . . 9
⊢ (((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) ∧ (𝑥 ∈ (Base‘𝑁) ∧ 𝑦 ∈ (Base‘𝑁))) → ◡𝐹 ∈ (𝑁 GrpIso 𝑀)) |
23 | | gimghm 18878 |
. . . . . . . . 9
⊢ (◡𝐹 ∈ (𝑁 GrpIso 𝑀) → ◡𝐹 ∈ (𝑁 GrpHom 𝑀)) |
24 | 22, 23 | syl 17 |
. . . . . . . 8
⊢ (((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) ∧ (𝑥 ∈ (Base‘𝑁) ∧ 𝑦 ∈ (Base‘𝑁))) → ◡𝐹 ∈ (𝑁 GrpHom 𝑀)) |
25 | | eqid 2738 |
. . . . . . . . 9
⊢
(+g‘𝑁) = (+g‘𝑁) |
26 | 8, 25, 18 | ghmlin 18837 |
. . . . . . . 8
⊢ ((◡𝐹 ∈ (𝑁 GrpHom 𝑀) ∧ 𝑥 ∈ (Base‘𝑁) ∧ 𝑦 ∈ (Base‘𝑁)) → (◡𝐹‘(𝑥(+g‘𝑁)𝑦)) = ((◡𝐹‘𝑥)(+g‘𝑀)(◡𝐹‘𝑦))) |
27 | 24, 14, 16, 26 | syl3anc 1370 |
. . . . . . 7
⊢ (((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) ∧ (𝑥 ∈ (Base‘𝑁) ∧ 𝑦 ∈ (Base‘𝑁))) → (◡𝐹‘(𝑥(+g‘𝑁)𝑦)) = ((◡𝐹‘𝑥)(+g‘𝑀)(◡𝐹‘𝑦))) |
28 | 8, 25, 18 | ghmlin 18837 |
. . . . . . . 8
⊢ ((◡𝐹 ∈ (𝑁 GrpHom 𝑀) ∧ 𝑦 ∈ (Base‘𝑁) ∧ 𝑥 ∈ (Base‘𝑁)) → (◡𝐹‘(𝑦(+g‘𝑁)𝑥)) = ((◡𝐹‘𝑦)(+g‘𝑀)(◡𝐹‘𝑥))) |
29 | 24, 16, 14, 28 | syl3anc 1370 |
. . . . . . 7
⊢ (((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) ∧ (𝑥 ∈ (Base‘𝑁) ∧ 𝑦 ∈ (Base‘𝑁))) → (◡𝐹‘(𝑦(+g‘𝑁)𝑥)) = ((◡𝐹‘𝑦)(+g‘𝑀)(◡𝐹‘𝑥))) |
30 | 20, 27, 29 | 3eqtr4d 2788 |
. . . . . 6
⊢ (((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) ∧ (𝑥 ∈ (Base‘𝑁) ∧ 𝑦 ∈ (Base‘𝑁))) → (◡𝐹‘(𝑥(+g‘𝑁)𝑦)) = (◡𝐹‘(𝑦(+g‘𝑁)𝑥))) |
31 | 30 | fveq2d 6780 |
. . . . 5
⊢ (((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) ∧ (𝑥 ∈ (Base‘𝑁) ∧ 𝑦 ∈ (Base‘𝑁))) → (𝐹‘(◡𝐹‘(𝑥(+g‘𝑁)𝑦))) = (𝐹‘(◡𝐹‘(𝑦(+g‘𝑁)𝑥)))) |
32 | 9 | ad2antlr 724 |
. . . . . 6
⊢ (((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) ∧ (𝑥 ∈ (Base‘𝑁) ∧ 𝑦 ∈ (Base‘𝑁))) → 𝐹:(Base‘𝑀)–1-1-onto→(Base‘𝑁)) |
33 | 3 | ad2antlr 724 |
. . . . . . 7
⊢ (((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) ∧ (𝑥 ∈ (Base‘𝑁) ∧ 𝑦 ∈ (Base‘𝑁))) → 𝑁 ∈ Grp) |
34 | 8, 25 | grpcl 18583 |
. . . . . . 7
⊢ ((𝑁 ∈ Grp ∧ 𝑥 ∈ (Base‘𝑁) ∧ 𝑦 ∈ (Base‘𝑁)) → (𝑥(+g‘𝑁)𝑦) ∈ (Base‘𝑁)) |
35 | 33, 14, 16, 34 | syl3anc 1370 |
. . . . . 6
⊢ (((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) ∧ (𝑥 ∈ (Base‘𝑁) ∧ 𝑦 ∈ (Base‘𝑁))) → (𝑥(+g‘𝑁)𝑦) ∈ (Base‘𝑁)) |
36 | | f1ocnvfv2 7151 |
. . . . . 6
⊢ ((𝐹:(Base‘𝑀)–1-1-onto→(Base‘𝑁) ∧ (𝑥(+g‘𝑁)𝑦) ∈ (Base‘𝑁)) → (𝐹‘(◡𝐹‘(𝑥(+g‘𝑁)𝑦))) = (𝑥(+g‘𝑁)𝑦)) |
37 | 32, 35, 36 | syl2anc 584 |
. . . . 5
⊢ (((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) ∧ (𝑥 ∈ (Base‘𝑁) ∧ 𝑦 ∈ (Base‘𝑁))) → (𝐹‘(◡𝐹‘(𝑥(+g‘𝑁)𝑦))) = (𝑥(+g‘𝑁)𝑦)) |
38 | 8, 25 | grpcl 18583 |
. . . . . . 7
⊢ ((𝑁 ∈ Grp ∧ 𝑦 ∈ (Base‘𝑁) ∧ 𝑥 ∈ (Base‘𝑁)) → (𝑦(+g‘𝑁)𝑥) ∈ (Base‘𝑁)) |
39 | 33, 16, 14, 38 | syl3anc 1370 |
. . . . . 6
⊢ (((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) ∧ (𝑥 ∈ (Base‘𝑁) ∧ 𝑦 ∈ (Base‘𝑁))) → (𝑦(+g‘𝑁)𝑥) ∈ (Base‘𝑁)) |
40 | | f1ocnvfv2 7151 |
. . . . . 6
⊢ ((𝐹:(Base‘𝑀)–1-1-onto→(Base‘𝑁) ∧ (𝑦(+g‘𝑁)𝑥) ∈ (Base‘𝑁)) → (𝐹‘(◡𝐹‘(𝑦(+g‘𝑁)𝑥))) = (𝑦(+g‘𝑁)𝑥)) |
41 | 32, 39, 40 | syl2anc 584 |
. . . . 5
⊢ (((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) ∧ (𝑥 ∈ (Base‘𝑁) ∧ 𝑦 ∈ (Base‘𝑁))) → (𝐹‘(◡𝐹‘(𝑦(+g‘𝑁)𝑥))) = (𝑦(+g‘𝑁)𝑥)) |
42 | 31, 37, 41 | 3eqtr3d 2786 |
. . . 4
⊢ (((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) ∧ (𝑥 ∈ (Base‘𝑁) ∧ 𝑦 ∈ (Base‘𝑁))) → (𝑥(+g‘𝑁)𝑦) = (𝑦(+g‘𝑁)𝑥)) |
43 | 42 | ralrimivva 3111 |
. . 3
⊢ ((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) → ∀𝑥 ∈ (Base‘𝑁)∀𝑦 ∈ (Base‘𝑁)(𝑥(+g‘𝑁)𝑦) = (𝑦(+g‘𝑁)𝑥)) |
44 | 8, 25 | iscmn 19392 |
. . 3
⊢ (𝑁 ∈ CMnd ↔ (𝑁 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑁)∀𝑦 ∈ (Base‘𝑁)(𝑥(+g‘𝑁)𝑦) = (𝑦(+g‘𝑁)𝑥))) |
45 | 5, 43, 44 | sylanbrc 583 |
. 2
⊢ ((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) → 𝑁 ∈ CMnd) |
46 | | isabl 19388 |
. 2
⊢ (𝑁 ∈ Abel ↔ (𝑁 ∈ Grp ∧ 𝑁 ∈ CMnd)) |
47 | 4, 45, 46 | sylanbrc 583 |
1
⊢ ((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) → 𝑁 ∈ Abel) |