Metamath Proof Explorer

Theorem pgrpgt2nabl

Description: Every symmetric group on a set with more than 2 elements is not abelian, see also the remark in Rotman p. 28. (Contributed by AV, 21-Mar-2019)

Ref Expression
Hypothesis pgrple2abl.g ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
Assertion pgrpgt2nabl ( ( 𝐴 ∈ 𝑉 ∧ 2 < ( ♯ ‘ 𝐴 ) ) → 𝐺 ∉ Abel )

Proof

Step Hyp Ref Expression
1 pgrple2abl.g ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2 eqid ⊢ ran ( pmTrsp ‘ 𝐴 ) = ran ( pmTrsp ‘ 𝐴 )
3 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
4 2 1 3 symgtrf ⊢ ran ( pmTrsp ‘ 𝐴 ) ⊆ ( Base ‘ 𝐺 )
5 hashcl ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
6 2nn0 ⊢ 2 ∈ ℕ0
7 nn0ltp1le ⊢ ( ( 2 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) → ( 2 < ( ♯ ‘ 𝐴 ) ↔ ( 2 + 1 ) ≤ ( ♯ ‘ 𝐴 ) ) )
8 6 7 mpan ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( 2 < ( ♯ ‘ 𝐴 ) ↔ ( 2 + 1 ) ≤ ( ♯ ‘ 𝐴 ) ) )
9 2p1e3 ⊢ ( 2 + 1 ) = 3
10 9 a1i ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( 2 + 1 ) = 3 )
11 10 breq1d ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ( 2 + 1 ) ≤ ( ♯ ‘ 𝐴 ) ↔ 3 ≤ ( ♯ ‘ 𝐴 ) ) )
12 8 11 bitrd ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( 2 < ( ♯ ‘ 𝐴 ) ↔ 3 ≤ ( ♯ ‘ 𝐴 ) ) )
13 12 biimpd ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( 2 < ( ♯ ‘ 𝐴 ) → 3 ≤ ( ♯ ‘ 𝐴 ) ) )
14 13 adantld ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ( 𝐴 ∈ 𝑉 ∧ 2 < ( ♯ ‘ 𝐴 ) ) → 3 ≤ ( ♯ ‘ 𝐴 ) ) )
15 5 14 syl ⊢ ( 𝐴 ∈ Fin → ( ( 𝐴 ∈ 𝑉 ∧ 2 < ( ♯ ‘ 𝐴 ) ) → 3 ≤ ( ♯ ‘ 𝐴 ) ) )
16 3re ⊢ 3 ∈ ℝ
17 16 rexri ⊢ 3 ∈ ℝ*
18 pnfge ⊢ ( 3 ∈ ℝ* → 3 ≤ +∞ )
19 17 18 ax-mp ⊢ 3 ≤ +∞
20 hashinf ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = +∞ )
21 19 20 breqtrrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → 3 ≤ ( ♯ ‘ 𝐴 ) )
22 21 ex ⊢ ( 𝐴 ∈ 𝑉 → ( ¬ 𝐴 ∈ Fin → 3 ≤ ( ♯ ‘ 𝐴 ) ) )
23 22 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 2 < ( ♯ ‘ 𝐴 ) ) → ( ¬ 𝐴 ∈ Fin → 3 ≤ ( ♯ ‘ 𝐴 ) ) )
24 23 com12 ⊢ ( ¬ 𝐴 ∈ Fin → ( ( 𝐴 ∈ 𝑉 ∧ 2 < ( ♯ ‘ 𝐴 ) ) → 3 ≤ ( ♯ ‘ 𝐴 ) ) )
25 15 24 pm2.61i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 2 < ( ♯ ‘ 𝐴 ) ) → 3 ≤ ( ♯ ‘ 𝐴 ) )
26 eqid ⊢ ( pmTrsp ‘ 𝐴 ) = ( pmTrsp ‘ 𝐴 )
27 26 pmtr3ncom ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐴 ) ) → ∃ 𝑦 ∈ ran ( pmTrsp ‘ 𝐴 ) ∃ 𝑥 ∈ ran ( pmTrsp ‘ 𝐴 ) ( 𝑥 ∘ 𝑦 ) ≠ ( 𝑦 ∘ 𝑥 ) )
28 rexcom ⊢ ( ∃ 𝑥 ∈ ran ( pmTrsp ‘ 𝐴 ) ∃ 𝑦 ∈ ran ( pmTrsp ‘ 𝐴 ) ( 𝑥 ∘ 𝑦 ) ≠ ( 𝑦 ∘ 𝑥 ) ↔ ∃ 𝑦 ∈ ran ( pmTrsp ‘ 𝐴 ) ∃ 𝑥 ∈ ran ( pmTrsp ‘ 𝐴 ) ( 𝑥 ∘ 𝑦 ) ≠ ( 𝑦 ∘ 𝑥 ) )
29 27 28 sylibr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐴 ) ) → ∃ 𝑥 ∈ ran ( pmTrsp ‘ 𝐴 ) ∃ 𝑦 ∈ ran ( pmTrsp ‘ 𝐴 ) ( 𝑥 ∘ 𝑦 ) ≠ ( 𝑦 ∘ 𝑥 ) )
30 25 29 syldan ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 2 < ( ♯ ‘ 𝐴 ) ) → ∃ 𝑥 ∈ ran ( pmTrsp ‘ 𝐴 ) ∃ 𝑦 ∈ ran ( pmTrsp ‘ 𝐴 ) ( 𝑥 ∘ 𝑦 ) ≠ ( 𝑦 ∘ 𝑥 ) )
31 ssrexv ⊢ ( ran ( pmTrsp ‘ 𝐴 ) ⊆ ( Base ‘ 𝐺 ) → ( ∃ 𝑦 ∈ ran ( pmTrsp ‘ 𝐴 ) ( 𝑥 ∘ 𝑦 ) ≠ ( 𝑦 ∘ 𝑥 ) → ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ∘ 𝑦 ) ≠ ( 𝑦 ∘ 𝑥 ) ) )
32 31 reximdv ⊢ ( ran ( pmTrsp ‘ 𝐴 ) ⊆ ( Base ‘ 𝐺 ) → ( ∃ 𝑥 ∈ ran ( pmTrsp ‘ 𝐴 ) ∃ 𝑦 ∈ ran ( pmTrsp ‘ 𝐴 ) ( 𝑥 ∘ 𝑦 ) ≠ ( 𝑦 ∘ 𝑥 ) → ∃ 𝑥 ∈ ran ( pmTrsp ‘ 𝐴 ) ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ∘ 𝑦 ) ≠ ( 𝑦 ∘ 𝑥 ) ) )
33 4 30 32 mpsyl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 2 < ( ♯ ‘ 𝐴 ) ) → ∃ 𝑥 ∈ ran ( pmTrsp ‘ 𝐴 ) ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ∘ 𝑦 ) ≠ ( 𝑦 ∘ 𝑥 ) )
34 ssrexv ⊢ ( ran ( pmTrsp ‘ 𝐴 ) ⊆ ( Base ‘ 𝐺 ) → ( ∃ 𝑥 ∈ ran ( pmTrsp ‘ 𝐴 ) ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ∘ 𝑦 ) ≠ ( 𝑦 ∘ 𝑥 ) → ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ∘ 𝑦 ) ≠ ( 𝑦 ∘ 𝑥 ) ) )
35 4 33 34 mpsyl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 2 < ( ♯ ‘ 𝐴 ) ) → ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ∘ 𝑦 ) ≠ ( 𝑦 ∘ 𝑥 ) )
36 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
37 1 3 36 symgov ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ∘ 𝑦 ) )
38 37 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 2 < ( ♯ ‘ 𝐴 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ∘ 𝑦 ) )
39 pm3.22 ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) )
40 39 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 2 < ( ♯ ‘ 𝐴 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) )
41 1 3 36 symgov ⊢ ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 𝑦 ∘ 𝑥 ) )
42 40 41 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 2 < ( ♯ ‘ 𝐴 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 𝑦 ∘ 𝑥 ) )
43 38 42 neeq12d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 2 < ( ♯ ‘ 𝐴 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ≠ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ↔ ( 𝑥 ∘ 𝑦 ) ≠ ( 𝑦 ∘ 𝑥 ) ) )
44 43 2rexbidva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 2 < ( ♯ ‘ 𝐴 ) ) → ( ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ≠ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ↔ ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ∘ 𝑦 ) ≠ ( 𝑦 ∘ 𝑥 ) ) )
45 35 44 mpbird ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 2 < ( ♯ ‘ 𝐴 ) ) → ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ≠ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
46 rexnal ⊢ ( ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) ¬ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
47 rexnal ⊢ ( ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ¬ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ↔ ¬ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
48 df-ne ⊢ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ≠ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ↔ ¬ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
49 48 bicomi ⊢ ( ¬ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ↔ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ≠ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
50 49 rexbii ⊢ ( ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ¬ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ↔ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ≠ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
51 47 50 bitr3i ⊢ ( ¬ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ↔ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ≠ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
52 51 rexbii ⊢ ( ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) ¬ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ↔ ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ≠ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
53 46 52 bitr3i ⊢ ( ¬ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ↔ ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ≠ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
54 45 53 sylibr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 2 < ( ♯ ‘ 𝐴 ) ) → ¬ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
55 54 intnand ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 2 < ( ♯ ‘ 𝐴 ) ) → ¬ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
56 55 intnand ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 2 < ( ♯ ‘ 𝐴 ) ) → ¬ ( 𝐺 ∈ Grp ∧ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
57 df-nel ⊢ ( 𝐺 ∉ Abel ↔ ¬ 𝐺 ∈ Abel )
58 isabl ⊢ ( 𝐺 ∈ Abel ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd ) )
59 3 36 iscmn ⊢ ( 𝐺 ∈ CMnd ↔ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
60 59 anbi2i ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd ) ↔ ( 𝐺 ∈ Grp ∧ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
61 58 60 bitri ⊢ ( 𝐺 ∈ Abel ↔ ( 𝐺 ∈ Grp ∧ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
62 57 61 xchbinx ⊢ ( 𝐺 ∉ Abel ↔ ¬ ( 𝐺 ∈ Grp ∧ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
63 56 62 sylibr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 2 < ( ♯ ‘ 𝐴 ) ) → 𝐺 ∉ Abel )