| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . . . . 8
⊢ ran
(pmTrsp‘𝐴) = ran
(pmTrsp‘𝐴) |
| 2 | | pgrple2abl.g |
. . . . . . . 8
⊢ 𝐺 = (SymGrp‘𝐴) |
| 3 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝐺) =
(Base‘𝐺) |
| 4 | 1, 2, 3 | symgtrf 19487 |
. . . . . . 7
⊢ ran
(pmTrsp‘𝐴) ⊆
(Base‘𝐺) |
| 5 | | hashcl 14395 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℕ0) |
| 6 | | 2nn0 12543 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℕ0 |
| 7 | | nn0ltp1le 12676 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℕ0 ∧ (♯‘𝐴) ∈ ℕ0) → (2 <
(♯‘𝐴) ↔ (2
+ 1) ≤ (♯‘𝐴))) |
| 8 | 6, 7 | mpan 690 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝐴)
∈ ℕ0 → (2 < (♯‘𝐴) ↔ (2 + 1) ≤ (♯‘𝐴))) |
| 9 | | 2p1e3 12408 |
. . . . . . . . . . . . . . . 16
⊢ (2 + 1) =
3 |
| 10 | 9 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝐴)
∈ ℕ0 → (2 + 1) = 3) |
| 11 | 10 | breq1d 5153 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝐴)
∈ ℕ0 → ((2 + 1) ≤ (♯‘𝐴) ↔ 3 ≤
(♯‘𝐴))) |
| 12 | 8, 11 | bitrd 279 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐴)
∈ ℕ0 → (2 < (♯‘𝐴) ↔ 3 ≤ (♯‘𝐴))) |
| 13 | 12 | biimpd 229 |
. . . . . . . . . . . 12
⊢
((♯‘𝐴)
∈ ℕ0 → (2 < (♯‘𝐴) → 3 ≤ (♯‘𝐴))) |
| 14 | 13 | adantld 490 |
. . . . . . . . . . 11
⊢
((♯‘𝐴)
∈ ℕ0 → ((𝐴 ∈ 𝑉 ∧ 2 < (♯‘𝐴)) → 3 ≤
(♯‘𝐴))) |
| 15 | 5, 14 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin → ((𝐴 ∈ 𝑉 ∧ 2 < (♯‘𝐴)) → 3 ≤
(♯‘𝐴))) |
| 16 | | 3re 12346 |
. . . . . . . . . . . . . . . 16
⊢ 3 ∈
ℝ |
| 17 | 16 | rexri 11319 |
. . . . . . . . . . . . . . 15
⊢ 3 ∈
ℝ* |
| 18 | | pnfge 13172 |
. . . . . . . . . . . . . . 15
⊢ (3 ∈
ℝ* → 3 ≤ +∞) |
| 19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ 3 ≤
+∞ |
| 20 | | hashinf 14374 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘𝐴) = +∞) |
| 21 | 19, 20 | breqtrrid 5181 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → 3 ≤
(♯‘𝐴)) |
| 22 | 21 | ex 412 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑉 → (¬ 𝐴 ∈ Fin → 3 ≤
(♯‘𝐴))) |
| 23 | 22 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (♯‘𝐴)) → (¬ 𝐴 ∈ Fin → 3 ≤
(♯‘𝐴))) |
| 24 | 23 | com12 32 |
. . . . . . . . . 10
⊢ (¬
𝐴 ∈ Fin → ((𝐴 ∈ 𝑉 ∧ 2 < (♯‘𝐴)) → 3 ≤
(♯‘𝐴))) |
| 25 | 15, 24 | pm2.61i 182 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (♯‘𝐴)) → 3 ≤
(♯‘𝐴)) |
| 26 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(pmTrsp‘𝐴) =
(pmTrsp‘𝐴) |
| 27 | 26 | pmtr3ncom 19493 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 3 ≤ (♯‘𝐴)) → ∃𝑦 ∈ ran (pmTrsp‘𝐴)∃𝑥 ∈ ran (pmTrsp‘𝐴)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥)) |
| 28 | | rexcom 3290 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈ ran
(pmTrsp‘𝐴)∃𝑦 ∈ ran (pmTrsp‘𝐴)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥) ↔ ∃𝑦 ∈ ran (pmTrsp‘𝐴)∃𝑥 ∈ ran (pmTrsp‘𝐴)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥)) |
| 29 | 27, 28 | sylibr 234 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 3 ≤ (♯‘𝐴)) → ∃𝑥 ∈ ran (pmTrsp‘𝐴)∃𝑦 ∈ ran (pmTrsp‘𝐴)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥)) |
| 30 | 25, 29 | syldan 591 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (♯‘𝐴)) → ∃𝑥 ∈ ran (pmTrsp‘𝐴)∃𝑦 ∈ ran (pmTrsp‘𝐴)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥)) |
| 31 | | ssrexv 4053 |
. . . . . . . . 9
⊢ (ran
(pmTrsp‘𝐴) ⊆
(Base‘𝐺) →
(∃𝑦 ∈ ran
(pmTrsp‘𝐴)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥) → ∃𝑦 ∈ (Base‘𝐺)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥))) |
| 32 | 31 | reximdv 3170 |
. . . . . . . 8
⊢ (ran
(pmTrsp‘𝐴) ⊆
(Base‘𝐺) →
(∃𝑥 ∈ ran
(pmTrsp‘𝐴)∃𝑦 ∈ ran (pmTrsp‘𝐴)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥) → ∃𝑥 ∈ ran (pmTrsp‘𝐴)∃𝑦 ∈ (Base‘𝐺)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥))) |
| 33 | 4, 30, 32 | mpsyl 68 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (♯‘𝐴)) → ∃𝑥 ∈ ran (pmTrsp‘𝐴)∃𝑦 ∈ (Base‘𝐺)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥)) |
| 34 | | ssrexv 4053 |
. . . . . . 7
⊢ (ran
(pmTrsp‘𝐴) ⊆
(Base‘𝐺) →
(∃𝑥 ∈ ran
(pmTrsp‘𝐴)∃𝑦 ∈ (Base‘𝐺)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥) → ∃𝑥 ∈ (Base‘𝐺)∃𝑦 ∈ (Base‘𝐺)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥))) |
| 35 | 4, 33, 34 | mpsyl 68 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (♯‘𝐴)) → ∃𝑥 ∈ (Base‘𝐺)∃𝑦 ∈ (Base‘𝐺)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥)) |
| 36 | | eqid 2737 |
. . . . . . . . . 10
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 37 | 2, 3, 36 | symgov 19401 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥(+g‘𝐺)𝑦) = (𝑥 ∘ 𝑦)) |
| 38 | 37 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 2 < (♯‘𝐴)) ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → (𝑥(+g‘𝐺)𝑦) = (𝑥 ∘ 𝑦)) |
| 39 | | pm3.22 459 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑦 ∈ (Base‘𝐺) ∧ 𝑥 ∈ (Base‘𝐺))) |
| 40 | 39 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 2 < (♯‘𝐴)) ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → (𝑦 ∈ (Base‘𝐺) ∧ 𝑥 ∈ (Base‘𝐺))) |
| 41 | 2, 3, 36 | symgov 19401 |
. . . . . . . . 9
⊢ ((𝑦 ∈ (Base‘𝐺) ∧ 𝑥 ∈ (Base‘𝐺)) → (𝑦(+g‘𝐺)𝑥) = (𝑦 ∘ 𝑥)) |
| 42 | 40, 41 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 2 < (♯‘𝐴)) ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → (𝑦(+g‘𝐺)𝑥) = (𝑦 ∘ 𝑥)) |
| 43 | 38, 42 | neeq12d 3002 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 2 < (♯‘𝐴)) ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → ((𝑥(+g‘𝐺)𝑦) ≠ (𝑦(+g‘𝐺)𝑥) ↔ (𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥))) |
| 44 | 43 | 2rexbidva 3220 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (♯‘𝐴)) → (∃𝑥 ∈ (Base‘𝐺)∃𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) ≠ (𝑦(+g‘𝐺)𝑥) ↔ ∃𝑥 ∈ (Base‘𝐺)∃𝑦 ∈ (Base‘𝐺)(𝑥 ∘ 𝑦) ≠ (𝑦 ∘ 𝑥))) |
| 45 | 35, 44 | mpbird 257 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (♯‘𝐴)) → ∃𝑥 ∈ (Base‘𝐺)∃𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) ≠ (𝑦(+g‘𝐺)𝑥)) |
| 46 | | rexnal 3100 |
. . . . . 6
⊢
(∃𝑥 ∈
(Base‘𝐺) ¬
∀𝑦 ∈
(Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥) ↔ ¬ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) |
| 47 | | rexnal 3100 |
. . . . . . . 8
⊢
(∃𝑦 ∈
(Base‘𝐺) ¬ (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥) ↔ ¬ ∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) |
| 48 | | df-ne 2941 |
. . . . . . . . . 10
⊢ ((𝑥(+g‘𝐺)𝑦) ≠ (𝑦(+g‘𝐺)𝑥) ↔ ¬ (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) |
| 49 | 48 | bicomi 224 |
. . . . . . . . 9
⊢ (¬
(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥) ↔ (𝑥(+g‘𝐺)𝑦) ≠ (𝑦(+g‘𝐺)𝑥)) |
| 50 | 49 | rexbii 3094 |
. . . . . . . 8
⊢
(∃𝑦 ∈
(Base‘𝐺) ¬ (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥) ↔ ∃𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) ≠ (𝑦(+g‘𝐺)𝑥)) |
| 51 | 47, 50 | bitr3i 277 |
. . . . . . 7
⊢ (¬
∀𝑦 ∈
(Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥) ↔ ∃𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) ≠ (𝑦(+g‘𝐺)𝑥)) |
| 52 | 51 | rexbii 3094 |
. . . . . 6
⊢
(∃𝑥 ∈
(Base‘𝐺) ¬
∀𝑦 ∈
(Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥) ↔ ∃𝑥 ∈ (Base‘𝐺)∃𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) ≠ (𝑦(+g‘𝐺)𝑥)) |
| 53 | 46, 52 | bitr3i 277 |
. . . . 5
⊢ (¬
∀𝑥 ∈
(Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥) ↔ ∃𝑥 ∈ (Base‘𝐺)∃𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) ≠ (𝑦(+g‘𝐺)𝑥)) |
| 54 | 45, 53 | sylibr 234 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (♯‘𝐴)) → ¬ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) |
| 55 | 54 | intnand 488 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (♯‘𝐴)) → ¬ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥))) |
| 56 | 55 | intnand 488 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (♯‘𝐴)) → ¬ (𝐺 ∈ Grp ∧ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))) |
| 57 | | df-nel 3047 |
. . 3
⊢ (𝐺 ∉ Abel ↔ ¬ 𝐺 ∈ Abel) |
| 58 | | isabl 19802 |
. . . 4
⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) |
| 59 | 3, 36 | iscmn 19807 |
. . . . 5
⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥))) |
| 60 | 59 | anbi2i 623 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd) ↔ (𝐺 ∈ Grp ∧ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))) |
| 61 | 58, 60 | bitri 275 |
. . 3
⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))) |
| 62 | 57, 61 | xchbinx 334 |
. 2
⊢ (𝐺 ∉ Abel ↔ ¬
(𝐺 ∈ Grp ∧ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))) |
| 63 | 56, 62 | sylibr 234 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (♯‘𝐴)) → 𝐺 ∉ Abel) |