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=SymGrpA
Assertion pgrpgt2nabl AV2<AGAbel

Proof

Step Hyp Ref Expression
1 pgrple2abl.g G=SymGrpA
2 eqid ranpmTrspA=ranpmTrspA
3 eqid BaseG=BaseG
4 2 1 3 symgtrf ranpmTrspABaseG
5 hashcl AFinA0
6 2nn0 20
7 nn0ltp1le 20A02<A2+1A
8 6 7 mpan A02<A2+1A
9 2p1e3 2+1=3
10 9 a1i A02+1=3
11 10 breq1d A02+1A3A
12 8 11 bitrd A02<A3A
13 12 biimpd A02<A3A
14 13 adantld A0AV2<A3A
15 5 14 syl AFinAV2<A3A
16 3re 3
17 16 rexri 3*
18 pnfge 3*3+∞
19 17 18 ax-mp 3+∞
20 hashinf AV¬AFinA=+∞
21 19 20 breqtrrid AV¬AFin3A
22 21 ex AV¬AFin3A
23 22 adantr AV2<A¬AFin3A
24 23 com12 ¬AFinAV2<A3A
25 15 24 pm2.61i AV2<A3A
26 eqid pmTrspA=pmTrspA
27 26 pmtr3ncom AV3AyranpmTrspAxranpmTrspAxyyx
28 rexcom xranpmTrspAyranpmTrspAxyyxyranpmTrspAxranpmTrspAxyyx
29 27 28 sylibr AV3AxranpmTrspAyranpmTrspAxyyx
30 25 29 syldan AV2<AxranpmTrspAyranpmTrspAxyyx
31 ssrexv ranpmTrspABaseGyranpmTrspAxyyxyBaseGxyyx
32 31 reximdv ranpmTrspABaseGxranpmTrspAyranpmTrspAxyyxxranpmTrspAyBaseGxyyx
33 4 30 32 mpsyl AV2<AxranpmTrspAyBaseGxyyx
34 ssrexv ranpmTrspABaseGxranpmTrspAyBaseGxyyxxBaseGyBaseGxyyx
35 4 33 34 mpsyl AV2<AxBaseGyBaseGxyyx
36 eqid +G=+G
37 1 3 36 symgov xBaseGyBaseGx+Gy=xy
38 37 adantl AV2<AxBaseGyBaseGx+Gy=xy
39 pm3.22 xBaseGyBaseGyBaseGxBaseG
40 39 adantl AV2<AxBaseGyBaseGyBaseGxBaseG
41 1 3 36 symgov yBaseGxBaseGy+Gx=yx
42 40 41 syl AV2<AxBaseGyBaseGy+Gx=yx
43 38 42 neeq12d AV2<AxBaseGyBaseGx+Gyy+Gxxyyx
44 43 2rexbidva AV2<AxBaseGyBaseGx+Gyy+GxxBaseGyBaseGxyyx
45 35 44 mpbird AV2<AxBaseGyBaseGx+Gyy+Gx
46 rexnal xBaseG¬yBaseGx+Gy=y+Gx¬xBaseGyBaseGx+Gy=y+Gx
47 rexnal yBaseG¬x+Gy=y+Gx¬yBaseGx+Gy=y+Gx
48 df-ne x+Gyy+Gx¬x+Gy=y+Gx
49 48 bicomi ¬x+Gy=y+Gxx+Gyy+Gx
50 49 rexbii yBaseG¬x+Gy=y+GxyBaseGx+Gyy+Gx
51 47 50 bitr3i ¬yBaseGx+Gy=y+GxyBaseGx+Gyy+Gx
52 51 rexbii xBaseG¬yBaseGx+Gy=y+GxxBaseGyBaseGx+Gyy+Gx
53 46 52 bitr3i ¬xBaseGyBaseGx+Gy=y+GxxBaseGyBaseGx+Gyy+Gx
54 45 53 sylibr AV2<A¬xBaseGyBaseGx+Gy=y+Gx
55 54 intnand AV2<A¬GMndxBaseGyBaseGx+Gy=y+Gx
56 55 intnand AV2<A¬GGrpGMndxBaseGyBaseGx+Gy=y+Gx
57 df-nel GAbel¬GAbel
58 isabl GAbelGGrpGCMnd
59 3 36 iscmn GCMndGMndxBaseGyBaseGx+Gy=y+Gx
60 59 anbi2i GGrpGCMndGGrpGMndxBaseGyBaseGx+Gy=y+Gx
61 58 60 bitri GAbelGGrpGMndxBaseGyBaseGx+Gy=y+Gx
62 57 61 xchbinx GAbel¬GGrpGMndxBaseGyBaseGx+Gy=y+Gx
63 56 62 sylibr AV2<AGAbel