# 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 ${⊢}{G}=\mathrm{SymGrp}\left({A}\right)$
Assertion pgrpgt2nabl ${⊢}\left({A}\in {V}\wedge 2<\left|{A}\right|\right)\to {G}\notin \mathrm{Abel}$

### Proof

Step Hyp Ref Expression
1 pgrple2abl.g ${⊢}{G}=\mathrm{SymGrp}\left({A}\right)$
2 eqid ${⊢}\mathrm{ran}\mathrm{pmTrsp}\left({A}\right)=\mathrm{ran}\mathrm{pmTrsp}\left({A}\right)$
3 eqid ${⊢}{\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{G}}$
4 2 1 3 symgtrf ${⊢}\mathrm{ran}\mathrm{pmTrsp}\left({A}\right)\subseteq {\mathrm{Base}}_{{G}}$
5 hashcl ${⊢}{A}\in \mathrm{Fin}\to \left|{A}\right|\in {ℕ}_{0}$
6 2nn0 ${⊢}2\in {ℕ}_{0}$
7 nn0ltp1le ${⊢}\left(2\in {ℕ}_{0}\wedge \left|{A}\right|\in {ℕ}_{0}\right)\to \left(2<\left|{A}\right|↔2+1\le \left|{A}\right|\right)$
8 6 7 mpan ${⊢}\left|{A}\right|\in {ℕ}_{0}\to \left(2<\left|{A}\right|↔2+1\le \left|{A}\right|\right)$
9 2p1e3 ${⊢}2+1=3$
10 9 a1i ${⊢}\left|{A}\right|\in {ℕ}_{0}\to 2+1=3$
11 10 breq1d ${⊢}\left|{A}\right|\in {ℕ}_{0}\to \left(2+1\le \left|{A}\right|↔3\le \left|{A}\right|\right)$
12 8 11 bitrd ${⊢}\left|{A}\right|\in {ℕ}_{0}\to \left(2<\left|{A}\right|↔3\le \left|{A}\right|\right)$
13 12 biimpd ${⊢}\left|{A}\right|\in {ℕ}_{0}\to \left(2<\left|{A}\right|\to 3\le \left|{A}\right|\right)$
14 13 adantld ${⊢}\left|{A}\right|\in {ℕ}_{0}\to \left(\left({A}\in {V}\wedge 2<\left|{A}\right|\right)\to 3\le \left|{A}\right|\right)$
15 5 14 syl ${⊢}{A}\in \mathrm{Fin}\to \left(\left({A}\in {V}\wedge 2<\left|{A}\right|\right)\to 3\le \left|{A}\right|\right)$
16 3re ${⊢}3\in ℝ$
17 16 rexri ${⊢}3\in {ℝ}^{*}$
18 pnfge ${⊢}3\in {ℝ}^{*}\to 3\le \mathrm{+\infty }$
19 17 18 ax-mp ${⊢}3\le \mathrm{+\infty }$
20 hashinf ${⊢}\left({A}\in {V}\wedge ¬{A}\in \mathrm{Fin}\right)\to \left|{A}\right|=\mathrm{+\infty }$
21 19 20 breqtrrid ${⊢}\left({A}\in {V}\wedge ¬{A}\in \mathrm{Fin}\right)\to 3\le \left|{A}\right|$
22 21 ex ${⊢}{A}\in {V}\to \left(¬{A}\in \mathrm{Fin}\to 3\le \left|{A}\right|\right)$
23 22 adantr ${⊢}\left({A}\in {V}\wedge 2<\left|{A}\right|\right)\to \left(¬{A}\in \mathrm{Fin}\to 3\le \left|{A}\right|\right)$
24 23 com12 ${⊢}¬{A}\in \mathrm{Fin}\to \left(\left({A}\in {V}\wedge 2<\left|{A}\right|\right)\to 3\le \left|{A}\right|\right)$
25 15 24 pm2.61i ${⊢}\left({A}\in {V}\wedge 2<\left|{A}\right|\right)\to 3\le \left|{A}\right|$
26 eqid ${⊢}\mathrm{pmTrsp}\left({A}\right)=\mathrm{pmTrsp}\left({A}\right)$
27 26 pmtr3ncom ${⊢}\left({A}\in {V}\wedge 3\le \left|{A}\right|\right)\to \exists {y}\in \mathrm{ran}\mathrm{pmTrsp}\left({A}\right)\phantom{\rule{.4em}{0ex}}\exists {x}\in \mathrm{ran}\mathrm{pmTrsp}\left({A}\right)\phantom{\rule{.4em}{0ex}}{x}\circ {y}\ne {y}\circ {x}$
28 rexcom ${⊢}\exists {x}\in \mathrm{ran}\mathrm{pmTrsp}\left({A}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in \mathrm{ran}\mathrm{pmTrsp}\left({A}\right)\phantom{\rule{.4em}{0ex}}{x}\circ {y}\ne {y}\circ {x}↔\exists {y}\in \mathrm{ran}\mathrm{pmTrsp}\left({A}\right)\phantom{\rule{.4em}{0ex}}\exists {x}\in \mathrm{ran}\mathrm{pmTrsp}\left({A}\right)\phantom{\rule{.4em}{0ex}}{x}\circ {y}\ne {y}\circ {x}$
29 27 28 sylibr ${⊢}\left({A}\in {V}\wedge 3\le \left|{A}\right|\right)\to \exists {x}\in \mathrm{ran}\mathrm{pmTrsp}\left({A}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in \mathrm{ran}\mathrm{pmTrsp}\left({A}\right)\phantom{\rule{.4em}{0ex}}{x}\circ {y}\ne {y}\circ {x}$
30 25 29 syldan ${⊢}\left({A}\in {V}\wedge 2<\left|{A}\right|\right)\to \exists {x}\in \mathrm{ran}\mathrm{pmTrsp}\left({A}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in \mathrm{ran}\mathrm{pmTrsp}\left({A}\right)\phantom{\rule{.4em}{0ex}}{x}\circ {y}\ne {y}\circ {x}$
31 ssrexv ${⊢}\mathrm{ran}\mathrm{pmTrsp}\left({A}\right)\subseteq {\mathrm{Base}}_{{G}}\to \left(\exists {y}\in \mathrm{ran}\mathrm{pmTrsp}\left({A}\right)\phantom{\rule{.4em}{0ex}}{x}\circ {y}\ne {y}\circ {x}\to \exists {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}\circ {y}\ne {y}\circ {x}\right)$
32 31 reximdv ${⊢}\mathrm{ran}\mathrm{pmTrsp}\left({A}\right)\subseteq {\mathrm{Base}}_{{G}}\to \left(\exists {x}\in \mathrm{ran}\mathrm{pmTrsp}\left({A}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in \mathrm{ran}\mathrm{pmTrsp}\left({A}\right)\phantom{\rule{.4em}{0ex}}{x}\circ {y}\ne {y}\circ {x}\to \exists {x}\in \mathrm{ran}\mathrm{pmTrsp}\left({A}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}\circ {y}\ne {y}\circ {x}\right)$
33 4 30 32 mpsyl ${⊢}\left({A}\in {V}\wedge 2<\left|{A}\right|\right)\to \exists {x}\in \mathrm{ran}\mathrm{pmTrsp}\left({A}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}\circ {y}\ne {y}\circ {x}$
34 ssrexv ${⊢}\mathrm{ran}\mathrm{pmTrsp}\left({A}\right)\subseteq {\mathrm{Base}}_{{G}}\to \left(\exists {x}\in \mathrm{ran}\mathrm{pmTrsp}\left({A}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}\circ {y}\ne {y}\circ {x}\to \exists {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\exists {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}\circ {y}\ne {y}\circ {x}\right)$
35 4 33 34 mpsyl ${⊢}\left({A}\in {V}\wedge 2<\left|{A}\right|\right)\to \exists {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\exists {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}\circ {y}\ne {y}\circ {x}$
36 eqid ${⊢}{+}_{{G}}={+}_{{G}}$
37 1 3 36 symgov ${⊢}\left({x}\in {\mathrm{Base}}_{{G}}\wedge {y}\in {\mathrm{Base}}_{{G}}\right)\to {x}{+}_{{G}}{y}={x}\circ {y}$
38 37 adantl ${⊢}\left(\left({A}\in {V}\wedge 2<\left|{A}\right|\right)\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge {y}\in {\mathrm{Base}}_{{G}}\right)\right)\to {x}{+}_{{G}}{y}={x}\circ {y}$
39 pm3.22 ${⊢}\left({x}\in {\mathrm{Base}}_{{G}}\wedge {y}\in {\mathrm{Base}}_{{G}}\right)\to \left({y}\in {\mathrm{Base}}_{{G}}\wedge {x}\in {\mathrm{Base}}_{{G}}\right)$
40 39 adantl ${⊢}\left(\left({A}\in {V}\wedge 2<\left|{A}\right|\right)\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge {y}\in {\mathrm{Base}}_{{G}}\right)\right)\to \left({y}\in {\mathrm{Base}}_{{G}}\wedge {x}\in {\mathrm{Base}}_{{G}}\right)$
41 1 3 36 symgov ${⊢}\left({y}\in {\mathrm{Base}}_{{G}}\wedge {x}\in {\mathrm{Base}}_{{G}}\right)\to {y}{+}_{{G}}{x}={y}\circ {x}$
42 40 41 syl ${⊢}\left(\left({A}\in {V}\wedge 2<\left|{A}\right|\right)\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge {y}\in {\mathrm{Base}}_{{G}}\right)\right)\to {y}{+}_{{G}}{x}={y}\circ {x}$
43 38 42 neeq12d ${⊢}\left(\left({A}\in {V}\wedge 2<\left|{A}\right|\right)\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge {y}\in {\mathrm{Base}}_{{G}}\right)\right)\to \left({x}{+}_{{G}}{y}\ne {y}{+}_{{G}}{x}↔{x}\circ {y}\ne {y}\circ {x}\right)$
44 43 2rexbidva ${⊢}\left({A}\in {V}\wedge 2<\left|{A}\right|\right)\to \left(\exists {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\exists {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\ne {y}{+}_{{G}}{x}↔\exists {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\exists {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}\circ {y}\ne {y}\circ {x}\right)$
45 35 44 mpbird ${⊢}\left({A}\in {V}\wedge 2<\left|{A}\right|\right)\to \exists {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\exists {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\ne {y}{+}_{{G}}{x}$
46 rexnal ${⊢}\exists {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}¬\forall {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}={y}{+}_{{G}}{x}↔¬\forall {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}={y}{+}_{{G}}{x}$
47 rexnal ${⊢}\exists {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}¬{x}{+}_{{G}}{y}={y}{+}_{{G}}{x}↔¬\forall {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}={y}{+}_{{G}}{x}$
48 df-ne ${⊢}{x}{+}_{{G}}{y}\ne {y}{+}_{{G}}{x}↔¬{x}{+}_{{G}}{y}={y}{+}_{{G}}{x}$
49 48 bicomi ${⊢}¬{x}{+}_{{G}}{y}={y}{+}_{{G}}{x}↔{x}{+}_{{G}}{y}\ne {y}{+}_{{G}}{x}$
50 49 rexbii ${⊢}\exists {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}¬{x}{+}_{{G}}{y}={y}{+}_{{G}}{x}↔\exists {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\ne {y}{+}_{{G}}{x}$
51 47 50 bitr3i ${⊢}¬\forall {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}={y}{+}_{{G}}{x}↔\exists {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\ne {y}{+}_{{G}}{x}$
52 51 rexbii ${⊢}\exists {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}¬\forall {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}={y}{+}_{{G}}{x}↔\exists {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\exists {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\ne {y}{+}_{{G}}{x}$
53 46 52 bitr3i ${⊢}¬\forall {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}={y}{+}_{{G}}{x}↔\exists {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\exists {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\ne {y}{+}_{{G}}{x}$
54 45 53 sylibr ${⊢}\left({A}\in {V}\wedge 2<\left|{A}\right|\right)\to ¬\forall {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}={y}{+}_{{G}}{x}$
55 54 intnand ${⊢}\left({A}\in {V}\wedge 2<\left|{A}\right|\right)\to ¬\left({G}\in \mathrm{Mnd}\wedge \forall {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}={y}{+}_{{G}}{x}\right)$
56 55 intnand ${⊢}\left({A}\in {V}\wedge 2<\left|{A}\right|\right)\to ¬\left({G}\in \mathrm{Grp}\wedge \left({G}\in \mathrm{Mnd}\wedge \forall {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}={y}{+}_{{G}}{x}\right)\right)$
57 df-nel ${⊢}{G}\notin \mathrm{Abel}↔¬{G}\in \mathrm{Abel}$
58 isabl ${⊢}{G}\in \mathrm{Abel}↔\left({G}\in \mathrm{Grp}\wedge {G}\in \mathrm{CMnd}\right)$
59 3 36 iscmn ${⊢}{G}\in \mathrm{CMnd}↔\left({G}\in \mathrm{Mnd}\wedge \forall {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}={y}{+}_{{G}}{x}\right)$
60 59 anbi2i ${⊢}\left({G}\in \mathrm{Grp}\wedge {G}\in \mathrm{CMnd}\right)↔\left({G}\in \mathrm{Grp}\wedge \left({G}\in \mathrm{Mnd}\wedge \forall {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}={y}{+}_{{G}}{x}\right)\right)$
61 58 60 bitri ${⊢}{G}\in \mathrm{Abel}↔\left({G}\in \mathrm{Grp}\wedge \left({G}\in \mathrm{Mnd}\wedge \forall {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}={y}{+}_{{G}}{x}\right)\right)$
62 57 61 xchbinx ${⊢}{G}\notin \mathrm{Abel}↔¬\left({G}\in \mathrm{Grp}\wedge \left({G}\in \mathrm{Mnd}\wedge \forall {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}={y}{+}_{{G}}{x}\right)\right)$
63 56 62 sylibr ${⊢}\left({A}\in {V}\wedge 2<\left|{A}\right|\right)\to {G}\notin \mathrm{Abel}$