Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . . . 8
⊢ ran
(pmTrsp‘𝐴) = ran
(pmTrsp‘𝐴) |
2 | | pgrple2abl.g |
. . . . . . . 8
⊢ 𝐺 = (SymGrp‘𝐴) |
3 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘𝐺) =
(Base‘𝐺) |
4 | 1, 2, 3 | symgtrf 17889 |
. . . . . . 7
⊢ ran
(pmTrsp‘𝐴) ⊆
(Base‘𝐺) |
5 | | hashcl 13147 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Fin →
(#‘𝐴) ∈
ℕ0) |
6 | | 2nn0 11309 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℕ0 |
7 | | nn0ltp1le 11435 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℕ0 ∧ (#‘𝐴) ∈ ℕ0) → (2 <
(#‘𝐴) ↔ (2 + 1)
≤ (#‘𝐴))) |
8 | 6, 7 | mpan 706 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐴) ∈
ℕ0 → (2 < (#‘𝐴) ↔ (2 + 1) ≤ (#‘𝐴))) |
9 | | 2p1e3 11151 |
. . . . . . . . . . . . . . . 16
⊢ (2 + 1) =
3 |
10 | 9 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐴) ∈
ℕ0 → (2 + 1) = 3) |
11 | 10 | breq1d 4663 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐴) ∈
ℕ0 → ((2 + 1) ≤ (#‘𝐴) ↔ 3 ≤ (#‘𝐴))) |
12 | 8, 11 | bitrd 268 |
. . . . . . . . . . . . 13
⊢
((#‘𝐴) ∈
ℕ0 → (2 < (#‘𝐴) ↔ 3 ≤ (#‘𝐴))) |
13 | 12 | biimpd 219 |
. . . . . . . . . . . 12
⊢
((#‘𝐴) ∈
ℕ0 → (2 < (#‘𝐴) → 3 ≤ (#‘𝐴))) |
14 | 13 | adantld 483 |
. . . . . . . . . . 11
⊢
((#‘𝐴) ∈
ℕ0 → ((𝐴 ∈ 𝑉 ∧ 2 < (#‘𝐴)) → 3 ≤ (#‘𝐴))) |
15 | 5, 14 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin → ((𝐴 ∈ 𝑉 ∧ 2 < (#‘𝐴)) → 3 ≤ (#‘𝐴))) |
16 | | 3re 11094 |
. . . . . . . . . . . . . . . 16
⊢ 3 ∈
ℝ |
17 | 16 | rexri 10097 |
. . . . . . . . . . . . . . 15
⊢ 3 ∈
ℝ* |
18 | | pnfge 11964 |
. . . . . . . . . . . . . . 15
⊢ (3 ∈
ℝ* → 3 ≤ +∞) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ 3 ≤
+∞ |
20 | | hashinf 13122 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (#‘𝐴) = +∞) |
21 | 19, 20 | syl5breqr 4691 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → 3 ≤ (#‘𝐴)) |
22 | 21 | ex 450 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑉 → (¬ 𝐴 ∈ Fin → 3 ≤ (#‘𝐴))) |
23 | 22 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (#‘𝐴)) → (¬ 𝐴 ∈ Fin → 3 ≤ (#‘𝐴))) |
24 | 23 | com12 32 |
. . . . . . . . . 10
⊢ (¬
𝐴 ∈ Fin → ((𝐴 ∈ 𝑉 ∧ 2 < (#‘𝐴)) → 3 ≤ (#‘𝐴))) |
25 | 15, 24 | pm2.61i 176 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (#‘𝐴)) → 3 ≤ (#‘𝐴)) |
26 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(pmTrsp‘𝐴) =
(pmTrsp‘𝐴) |
27 | 26 | pmtr3ncom 17895 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 3 ≤ (#‘𝐴)) → ∃𝑦 ∈ ran (pmTrsp‘𝐴)∃𝑥 ∈ ran (pmTrsp‘𝐴)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥)) |
28 | | rexcom 3099 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈ ran
(pmTrsp‘𝐴)∃𝑦 ∈ ran (pmTrsp‘𝐴)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥) ↔ ∃𝑦 ∈ ran (pmTrsp‘𝐴)∃𝑥 ∈ ran (pmTrsp‘𝐴)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥)) |
29 | 27, 28 | sylibr 224 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 3 ≤ (#‘𝐴)) → ∃𝑥 ∈ ran (pmTrsp‘𝐴)∃𝑦 ∈ ran (pmTrsp‘𝐴)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥)) |
30 | 25, 29 | syldan 487 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (#‘𝐴)) → ∃𝑥 ∈ ran (pmTrsp‘𝐴)∃𝑦 ∈ ran (pmTrsp‘𝐴)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥)) |
31 | | ssrexv 3667 |
. . . . . . . . 9
⊢ (ran
(pmTrsp‘𝐴) ⊆
(Base‘𝐺) →
(∃𝑦 ∈ ran
(pmTrsp‘𝐴)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥) → ∃𝑦 ∈ (Base‘𝐺)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥))) |
32 | 31 | reximdv 3016 |
. . . . . . . 8
⊢ (ran
(pmTrsp‘𝐴) ⊆
(Base‘𝐺) →
(∃𝑥 ∈ ran
(pmTrsp‘𝐴)∃𝑦 ∈ ran (pmTrsp‘𝐴)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥) → ∃𝑥 ∈ ran (pmTrsp‘𝐴)∃𝑦 ∈ (Base‘𝐺)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥))) |
33 | 4, 30, 32 | mpsyl 68 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (#‘𝐴)) → ∃𝑥 ∈ ran (pmTrsp‘𝐴)∃𝑦 ∈ (Base‘𝐺)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥)) |
34 | | ssrexv 3667 |
. . . . . . 7
⊢ (ran
(pmTrsp‘𝐴) ⊆
(Base‘𝐺) →
(∃𝑥 ∈ ran
(pmTrsp‘𝐴)∃𝑦 ∈ (Base‘𝐺)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥) → ∃𝑥 ∈ (Base‘𝐺)∃𝑦 ∈ (Base‘𝐺)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥))) |
35 | 4, 33, 34 | mpsyl 68 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (#‘𝐴)) → ∃𝑥 ∈ (Base‘𝐺)∃𝑦 ∈ (Base‘𝐺)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥)) |
36 | | eqid 2622 |
. . . . . . . . . 10
⊢
(+g‘𝐺) = (+g‘𝐺) |
37 | 2, 3, 36 | symgov 17810 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥(+g‘𝐺)𝑦) = (𝑥 ∘ 𝑦)) |
38 | 37 | adantl 482 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 2 < (#‘𝐴)) ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → (𝑥(+g‘𝐺)𝑦) = (𝑥 ∘ 𝑦)) |
39 | | pm3.22 465 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑦 ∈ (Base‘𝐺) ∧ 𝑥 ∈ (Base‘𝐺))) |
40 | 39 | adantl 482 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 2 < (#‘𝐴)) ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → (𝑦 ∈ (Base‘𝐺) ∧ 𝑥 ∈ (Base‘𝐺))) |
41 | 2, 3, 36 | symgov 17810 |
. . . . . . . . 9
⊢ ((𝑦 ∈ (Base‘𝐺) ∧ 𝑥 ∈ (Base‘𝐺)) → (𝑦(+g‘𝐺)𝑥) = (𝑦 ∘ 𝑥)) |
42 | 40, 41 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 2 < (#‘𝐴)) ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → (𝑦(+g‘𝐺)𝑥) = (𝑦 ∘ 𝑥)) |
43 | 38, 42 | neeq12d 2855 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 2 < (#‘𝐴)) ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → ((𝑥(+g‘𝐺)𝑦) ≠ (𝑦(+g‘𝐺)𝑥) ↔ (𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥))) |
44 | 43 | 2rexbidva 3056 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (#‘𝐴)) → (∃𝑥 ∈ (Base‘𝐺)∃𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) ≠ (𝑦(+g‘𝐺)𝑥) ↔ ∃𝑥 ∈ (Base‘𝐺)∃𝑦 ∈ (Base‘𝐺)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥))) |
45 | 35, 44 | mpbird 247 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (#‘𝐴)) → ∃𝑥 ∈ (Base‘𝐺)∃𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) ≠ (𝑦(+g‘𝐺)𝑥)) |
46 | | rexnal 2995 |
. . . . . 6
⊢
(∃𝑥 ∈
(Base‘𝐺) ¬
∀𝑦 ∈
(Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥) ↔ ¬ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) |
47 | | rexnal 2995 |
. . . . . . . 8
⊢
(∃𝑦 ∈
(Base‘𝐺) ¬ (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥) ↔ ¬ ∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) |
48 | | df-ne 2795 |
. . . . . . . . . 10
⊢ ((𝑥(+g‘𝐺)𝑦) ≠ (𝑦(+g‘𝐺)𝑥) ↔ ¬ (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) |
49 | 48 | bicomi 214 |
. . . . . . . . 9
⊢ (¬
(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥) ↔ (𝑥(+g‘𝐺)𝑦) ≠ (𝑦(+g‘𝐺)𝑥)) |
50 | 49 | rexbii 3041 |
. . . . . . . 8
⊢
(∃𝑦 ∈
(Base‘𝐺) ¬ (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥) ↔ ∃𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) ≠ (𝑦(+g‘𝐺)𝑥)) |
51 | 47, 50 | bitr3i 266 |
. . . . . . 7
⊢ (¬
∀𝑦 ∈
(Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥) ↔ ∃𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) ≠ (𝑦(+g‘𝐺)𝑥)) |
52 | 51 | rexbii 3041 |
. . . . . 6
⊢
(∃𝑥 ∈
(Base‘𝐺) ¬
∀𝑦 ∈
(Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥) ↔ ∃𝑥 ∈ (Base‘𝐺)∃𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) ≠ (𝑦(+g‘𝐺)𝑥)) |
53 | 46, 52 | bitr3i 266 |
. . . . 5
⊢ (¬
∀𝑥 ∈
(Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥) ↔ ∃𝑥 ∈ (Base‘𝐺)∃𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) ≠ (𝑦(+g‘𝐺)𝑥)) |
54 | 45, 53 | sylibr 224 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (#‘𝐴)) → ¬ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) |
55 | 54 | intnand 962 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (#‘𝐴)) → ¬ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥))) |
56 | 55 | intnand 962 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (#‘𝐴)) → ¬ (𝐺 ∈ Grp ∧ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))) |
57 | | df-nel 2898 |
. . 3
⊢ (𝐺 ∉ Abel ↔ ¬ 𝐺 ∈ Abel) |
58 | | isabl 18197 |
. . . 4
⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) |
59 | 3, 36 | iscmn 18200 |
. . . . 5
⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥))) |
60 | 59 | anbi2i 730 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd) ↔ (𝐺 ∈ Grp ∧ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))) |
61 | 58, 60 | bitri 264 |
. . 3
⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))) |
62 | 57, 61 | xchbinx 324 |
. 2
⊢ (𝐺 ∉ Abel ↔ ¬
(𝐺 ∈ Grp ∧ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))) |
63 | 56, 62 | sylibr 224 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (#‘𝐴)) → 𝐺 ∉ Abel) |