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 = ( SymGrp ` A )
Assertion pgrpgt2nabl 
|- ( ( A e. V /\ 2 < ( # ` A ) ) -> G e/ Abel )

Proof

Step Hyp Ref Expression
1 pgrple2abl.g 
 |-  G = ( SymGrp ` A )
2 eqid 
 |-  ran ( pmTrsp ` A ) = ran ( pmTrsp ` A )
3 eqid 
 |-  ( Base ` G ) = ( Base ` G )
4 2 1 3 symgtrf 
 |-  ran ( pmTrsp ` A ) C_ ( Base ` G )
5 hashcl 
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
6 2nn0 
 |-  2 e. NN0
7 nn0ltp1le 
 |-  ( ( 2 e. NN0 /\ ( # ` A ) e. NN0 ) -> ( 2 < ( # ` A ) <-> ( 2 + 1 ) <_ ( # ` A ) ) )
8 6 7 mpan 
 |-  ( ( # ` A ) e. NN0 -> ( 2 < ( # ` A ) <-> ( 2 + 1 ) <_ ( # ` A ) ) )
9 2p1e3 
 |-  ( 2 + 1 ) = 3
10 9 a1i 
 |-  ( ( # ` A ) e. NN0 -> ( 2 + 1 ) = 3 )
11 10 breq1d 
 |-  ( ( # ` A ) e. NN0 -> ( ( 2 + 1 ) <_ ( # ` A ) <-> 3 <_ ( # ` A ) ) )
12 8 11 bitrd 
 |-  ( ( # ` A ) e. NN0 -> ( 2 < ( # ` A ) <-> 3 <_ ( # ` A ) ) )
13 12 biimpd 
 |-  ( ( # ` A ) e. NN0 -> ( 2 < ( # ` A ) -> 3 <_ ( # ` A ) ) )
14 13 adantld 
 |-  ( ( # ` A ) e. NN0 -> ( ( A e. V /\ 2 < ( # ` A ) ) -> 3 <_ ( # ` A ) ) )
15 5 14 syl 
 |-  ( A e. Fin -> ( ( A e. V /\ 2 < ( # ` A ) ) -> 3 <_ ( # ` A ) ) )
16 3re 
 |-  3 e. RR
17 16 rexri 
 |-  3 e. RR*
18 pnfge 
 |-  ( 3 e. RR* -> 3 <_ +oo )
19 17 18 ax-mp 
 |-  3 <_ +oo
20 hashinf 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( # ` A ) = +oo )
21 19 20 breqtrrid 
 |-  ( ( A e. V /\ -. A e. Fin ) -> 3 <_ ( # ` A ) )
22 21 ex 
 |-  ( A e. V -> ( -. A e. Fin -> 3 <_ ( # ` A ) ) )
23 22 adantr 
 |-  ( ( A e. V /\ 2 < ( # ` A ) ) -> ( -. A e. Fin -> 3 <_ ( # ` A ) ) )
24 23 com12 
 |-  ( -. A e. Fin -> ( ( A e. V /\ 2 < ( # ` A ) ) -> 3 <_ ( # ` A ) ) )
25 15 24 pm2.61i 
 |-  ( ( A e. V /\ 2 < ( # ` A ) ) -> 3 <_ ( # ` A ) )
26 eqid 
 |-  ( pmTrsp ` A ) = ( pmTrsp ` A )
27 26 pmtr3ncom 
 |-  ( ( A e. V /\ 3 <_ ( # ` A ) ) -> E. y e. ran ( pmTrsp ` A ) E. x e. ran ( pmTrsp ` A ) ( x o. y ) =/= ( y o. x ) )
28 rexcom 
 |-  ( E. x e. ran ( pmTrsp ` A ) E. y e. ran ( pmTrsp ` A ) ( x o. y ) =/= ( y o. x ) <-> E. y e. ran ( pmTrsp ` A ) E. x e. ran ( pmTrsp ` A ) ( x o. y ) =/= ( y o. x ) )
29 27 28 sylibr 
 |-  ( ( A e. V /\ 3 <_ ( # ` A ) ) -> E. x e. ran ( pmTrsp ` A ) E. y e. ran ( pmTrsp ` A ) ( x o. y ) =/= ( y o. x ) )
30 25 29 syldan 
 |-  ( ( A e. V /\ 2 < ( # ` A ) ) -> E. x e. ran ( pmTrsp ` A ) E. y e. ran ( pmTrsp ` A ) ( x o. y ) =/= ( y o. x ) )
31 ssrexv 
 |-  ( ran ( pmTrsp ` A ) C_ ( Base ` G ) -> ( E. y e. ran ( pmTrsp ` A ) ( x o. y ) =/= ( y o. x ) -> E. y e. ( Base ` G ) ( x o. y ) =/= ( y o. x ) ) )
32 31 reximdv 
 |-  ( ran ( pmTrsp ` A ) C_ ( Base ` G ) -> ( E. x e. ran ( pmTrsp ` A ) E. y e. ran ( pmTrsp ` A ) ( x o. y ) =/= ( y o. x ) -> E. x e. ran ( pmTrsp ` A ) E. y e. ( Base ` G ) ( x o. y ) =/= ( y o. x ) ) )
33 4 30 32 mpsyl 
 |-  ( ( A e. V /\ 2 < ( # ` A ) ) -> E. x e. ran ( pmTrsp ` A ) E. y e. ( Base ` G ) ( x o. y ) =/= ( y o. x ) )
34 ssrexv 
 |-  ( ran ( pmTrsp ` A ) C_ ( Base ` G ) -> ( E. x e. ran ( pmTrsp ` A ) E. y e. ( Base ` G ) ( x o. y ) =/= ( y o. x ) -> E. x e. ( Base ` G ) E. y e. ( Base ` G ) ( x o. y ) =/= ( y o. x ) ) )
35 4 33 34 mpsyl 
 |-  ( ( A e. V /\ 2 < ( # ` A ) ) -> E. x e. ( Base ` G ) E. y e. ( Base ` G ) ( x o. y ) =/= ( y o. x ) )
36 eqid 
 |-  ( +g ` G ) = ( +g ` G )
37 1 3 36 symgov 
 |-  ( ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x ( +g ` G ) y ) = ( x o. y ) )
38 37 adantl 
 |-  ( ( ( A e. V /\ 2 < ( # ` A ) ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( x ( +g ` G ) y ) = ( x o. y ) )
39 pm3.22 
 |-  ( ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( y e. ( Base ` G ) /\ x e. ( Base ` G ) ) )
40 39 adantl 
 |-  ( ( ( A e. V /\ 2 < ( # ` A ) ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( y e. ( Base ` G ) /\ x e. ( Base ` G ) ) )
41 1 3 36 symgov 
 |-  ( ( y e. ( Base ` G ) /\ x e. ( Base ` G ) ) -> ( y ( +g ` G ) x ) = ( y o. x ) )
42 40 41 syl 
 |-  ( ( ( A e. V /\ 2 < ( # ` A ) ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( y ( +g ` G ) x ) = ( y o. x ) )
43 38 42 neeq12d 
 |-  ( ( ( A e. V /\ 2 < ( # ` A ) ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( ( x ( +g ` G ) y ) =/= ( y ( +g ` G ) x ) <-> ( x o. y ) =/= ( y o. x ) ) )
44 43 2rexbidva 
 |-  ( ( A e. V /\ 2 < ( # ` A ) ) -> ( E. x e. ( Base ` G ) E. y e. ( Base ` G ) ( x ( +g ` G ) y ) =/= ( y ( +g ` G ) x ) <-> E. x e. ( Base ` G ) E. y e. ( Base ` G ) ( x o. y ) =/= ( y o. x ) ) )
45 35 44 mpbird 
 |-  ( ( A e. V /\ 2 < ( # ` A ) ) -> E. x e. ( Base ` G ) E. y e. ( Base ` G ) ( x ( +g ` G ) y ) =/= ( y ( +g ` G ) x ) )
46 rexnal 
 |-  ( E. x e. ( Base ` G ) -. A. y e. ( Base ` G ) ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) <-> -. A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) )
47 rexnal 
 |-  ( E. y e. ( Base ` G ) -. ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) <-> -. A. y e. ( Base ` G ) ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) )
48 df-ne 
 |-  ( ( x ( +g ` G ) y ) =/= ( y ( +g ` G ) x ) <-> -. ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) )
49 48 bicomi 
 |-  ( -. ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) <-> ( x ( +g ` G ) y ) =/= ( y ( +g ` G ) x ) )
50 49 rexbii 
 |-  ( E. y e. ( Base ` G ) -. ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) <-> E. y e. ( Base ` G ) ( x ( +g ` G ) y ) =/= ( y ( +g ` G ) x ) )
51 47 50 bitr3i 
 |-  ( -. A. y e. ( Base ` G ) ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) <-> E. y e. ( Base ` G ) ( x ( +g ` G ) y ) =/= ( y ( +g ` G ) x ) )
52 51 rexbii 
 |-  ( E. x e. ( Base ` G ) -. A. y e. ( Base ` G ) ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) <-> E. x e. ( Base ` G ) E. y e. ( Base ` G ) ( x ( +g ` G ) y ) =/= ( y ( +g ` G ) x ) )
53 46 52 bitr3i 
 |-  ( -. A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) <-> E. x e. ( Base ` G ) E. y e. ( Base ` G ) ( x ( +g ` G ) y ) =/= ( y ( +g ` G ) x ) )
54 45 53 sylibr 
 |-  ( ( A e. V /\ 2 < ( # ` A ) ) -> -. A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) )
55 54 intnand 
 |-  ( ( A e. V /\ 2 < ( # ` A ) ) -> -. ( G e. Mnd /\ A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) )
56 55 intnand 
 |-  ( ( A e. V /\ 2 < ( # ` A ) ) -> -. ( G e. Grp /\ ( G e. Mnd /\ A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) ) )
57 df-nel 
 |-  ( G e/ Abel <-> -. G e. Abel )
58 isabl 
 |-  ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )
59 3 36 iscmn 
 |-  ( G e. CMnd <-> ( G e. Mnd /\ A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) )
60 59 anbi2i 
 |-  ( ( G e. Grp /\ G e. CMnd ) <-> ( G e. Grp /\ ( G e. Mnd /\ A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) ) )
61 58 60 bitri 
 |-  ( G e. Abel <-> ( G e. Grp /\ ( G e. Mnd /\ A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) ) )
62 57 61 xchbinx 
 |-  ( G e/ Abel <-> -. ( G e. Grp /\ ( G e. Mnd /\ A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) ) )
63 56 62 sylibr 
 |-  ( ( A e. V /\ 2 < ( # ` A ) ) -> G e/ Abel )