Metamath Proof Explorer

Theorem pmtr3ncom

Description: Transpositions over sets with at least 3 elements are not commutative, see also the remark in Rotman p. 28. (Contributed by AV, 21-Mar-2019)

Ref Expression
Hypothesis pmtr3ncom.t 
|- T = ( pmTrsp ` D )
Assertion pmtr3ncom 
|- ( ( D e. V /\ 3 <_ ( # ` D ) ) -> E. f e. ran T E. g e. ran T ( g o. f ) =/= ( f o. g ) )

Proof

Step Hyp Ref Expression
1 pmtr3ncom.t 
 |-  T = ( pmTrsp ` D )
2 hashge3el3dif 
 |-  ( ( D e. V /\ 3 <_ ( # ` D ) ) -> E. x e. D E. y e. D E. z e. D ( x =/= y /\ x =/= z /\ y =/= z ) )
3 simprl 
 |-  ( ( ( ( ( x e. D /\ y e. D ) /\ z e. D ) /\ ( x =/= y /\ x =/= z /\ y =/= z ) ) /\ ( D e. V /\ 3 <_ ( # ` D ) ) ) -> D e. V )
4 prssi 
 |-  ( ( x e. D /\ y e. D ) -> { x , y } C_ D )
5 4 adantr 
 |-  ( ( ( x e. D /\ y e. D ) /\ z e. D ) -> { x , y } C_ D )
6 5 ad2antrr 
 |-  ( ( ( ( ( x e. D /\ y e. D ) /\ z e. D ) /\ ( x =/= y /\ x =/= z /\ y =/= z ) ) /\ ( D e. V /\ 3 <_ ( # ` D ) ) ) -> { x , y } C_ D )
7 simplll 
 |-  ( ( ( ( x e. D /\ y e. D ) /\ z e. D ) /\ ( x =/= y /\ x =/= z /\ y =/= z ) ) -> x e. D )
8 simplr 
 |-  ( ( ( x e. D /\ y e. D ) /\ z e. D ) -> y e. D )
9 8 adantr 
 |-  ( ( ( ( x e. D /\ y e. D ) /\ z e. D ) /\ ( x =/= y /\ x =/= z /\ y =/= z ) ) -> y e. D )
10 simpr1 
 |-  ( ( ( ( x e. D /\ y e. D ) /\ z e. D ) /\ ( x =/= y /\ x =/= z /\ y =/= z ) ) -> x =/= y )
11 pr2nelem 
 |-  ( ( x e. D /\ y e. D /\ x =/= y ) -> { x , y } ~~ 2o )
12 7 9 10 11 syl3anc 
 |-  ( ( ( ( x e. D /\ y e. D ) /\ z e. D ) /\ ( x =/= y /\ x =/= z /\ y =/= z ) ) -> { x , y } ~~ 2o )
13 12 adantr 
 |-  ( ( ( ( ( x e. D /\ y e. D ) /\ z e. D ) /\ ( x =/= y /\ x =/= z /\ y =/= z ) ) /\ ( D e. V /\ 3 <_ ( # ` D ) ) ) -> { x , y } ~~ 2o )
14 eqid 
 |-  ran T = ran T
15 1 14 pmtrrn 
 |-  ( ( D e. V /\ { x , y } C_ D /\ { x , y } ~~ 2o ) -> ( T ` { x , y } ) e. ran T )
16 3 6 13 15 syl3anc 
 |-  ( ( ( ( ( x e. D /\ y e. D ) /\ z e. D ) /\ ( x =/= y /\ x =/= z /\ y =/= z ) ) /\ ( D e. V /\ 3 <_ ( # ` D ) ) ) -> ( T ` { x , y } ) e. ran T )
17 prssi 
 |-  ( ( y e. D /\ z e. D ) -> { y , z } C_ D )
18 17 ad5ant23 
 |-  ( ( ( ( ( x e. D /\ y e. D ) /\ z e. D ) /\ ( x =/= y /\ x =/= z /\ y =/= z ) ) /\ ( D e. V /\ 3 <_ ( # ` D ) ) ) -> { y , z } C_ D )
19 simplr 
 |-  ( ( ( ( x e. D /\ y e. D ) /\ z e. D ) /\ ( x =/= y /\ x =/= z /\ y =/= z ) ) -> z e. D )
20 simpr3 
 |-  ( ( ( ( x e. D /\ y e. D ) /\ z e. D ) /\ ( x =/= y /\ x =/= z /\ y =/= z ) ) -> y =/= z )
21 pr2nelem 
 |-  ( ( y e. D /\ z e. D /\ y =/= z ) -> { y , z } ~~ 2o )
22 9 19 20 21 syl3anc 
 |-  ( ( ( ( x e. D /\ y e. D ) /\ z e. D ) /\ ( x =/= y /\ x =/= z /\ y =/= z ) ) -> { y , z } ~~ 2o )
23 22 adantr 
 |-  ( ( ( ( ( x e. D /\ y e. D ) /\ z e. D ) /\ ( x =/= y /\ x =/= z /\ y =/= z ) ) /\ ( D e. V /\ 3 <_ ( # ` D ) ) ) -> { y , z } ~~ 2o )
24 1 14 pmtrrn 
 |-  ( ( D e. V /\ { y , z } C_ D /\ { y , z } ~~ 2o ) -> ( T ` { y , z } ) e. ran T )
25 3 18 23 24 syl3anc 
 |-  ( ( ( ( ( x e. D /\ y e. D ) /\ z e. D ) /\ ( x =/= y /\ x =/= z /\ y =/= z ) ) /\ ( D e. V /\ 3 <_ ( # ` D ) ) ) -> ( T ` { y , z } ) e. ran T )
26 df-3an 
 |-  ( ( x e. D /\ y e. D /\ z e. D ) <-> ( ( x e. D /\ y e. D ) /\ z e. D ) )
27 26 biimpri 
 |-  ( ( ( x e. D /\ y e. D ) /\ z e. D ) -> ( x e. D /\ y e. D /\ z e. D ) )
28 27 ad2antrr 
 |-  ( ( ( ( ( x e. D /\ y e. D ) /\ z e. D ) /\ ( x =/= y /\ x =/= z /\ y =/= z ) ) /\ ( D e. V /\ 3 <_ ( # ` D ) ) ) -> ( x e. D /\ y e. D /\ z e. D ) )
29 simplr 
 |-  ( ( ( ( ( x e. D /\ y e. D ) /\ z e. D ) /\ ( x =/= y /\ x =/= z /\ y =/= z ) ) /\ ( D e. V /\ 3 <_ ( # ` D ) ) ) -> ( x =/= y /\ x =/= z /\ y =/= z ) )
30 eqid 
 |-  ( T ` { x , y } ) = ( T ` { x , y } )
31 eqid 
 |-  ( T ` { y , z } ) = ( T ` { y , z } )
32 1 30 31 pmtr3ncomlem2 
 |-  ( ( D e. V /\ ( x e. D /\ y e. D /\ z e. D ) /\ ( x =/= y /\ x =/= z /\ y =/= z ) ) -> ( ( T ` { y , z } ) o. ( T ` { x , y } ) ) =/= ( ( T ` { x , y } ) o. ( T ` { y , z } ) ) )
33 3 28 29 32 syl3anc 
 |-  ( ( ( ( ( x e. D /\ y e. D ) /\ z e. D ) /\ ( x =/= y /\ x =/= z /\ y =/= z ) ) /\ ( D e. V /\ 3 <_ ( # ` D ) ) ) -> ( ( T ` { y , z } ) o. ( T ` { x , y } ) ) =/= ( ( T ` { x , y } ) o. ( T ` { y , z } ) ) )
34 coeq2 
 |-  ( f = ( T ` { x , y } ) -> ( g o. f ) = ( g o. ( T ` { x , y } ) ) )
35 coeq1 
 |-  ( f = ( T ` { x , y } ) -> ( f o. g ) = ( ( T ` { x , y } ) o. g ) )
36 34 35 neeq12d 
 |-  ( f = ( T ` { x , y } ) -> ( ( g o. f ) =/= ( f o. g ) <-> ( g o. ( T ` { x , y } ) ) =/= ( ( T ` { x , y } ) o. g ) ) )
37 coeq1 
 |-  ( g = ( T ` { y , z } ) -> ( g o. ( T ` { x , y } ) ) = ( ( T ` { y , z } ) o. ( T ` { x , y } ) ) )
38 coeq2 
 |-  ( g = ( T ` { y , z } ) -> ( ( T ` { x , y } ) o. g ) = ( ( T ` { x , y } ) o. ( T ` { y , z } ) ) )
39 37 38 neeq12d 
 |-  ( g = ( T ` { y , z } ) -> ( ( g o. ( T ` { x , y } ) ) =/= ( ( T ` { x , y } ) o. g ) <-> ( ( T ` { y , z } ) o. ( T ` { x , y } ) ) =/= ( ( T ` { x , y } ) o. ( T ` { y , z } ) ) ) )
40 36 39 rspc2ev 
 |-  ( ( ( T ` { x , y } ) e. ran T /\ ( T ` { y , z } ) e. ran T /\ ( ( T ` { y , z } ) o. ( T ` { x , y } ) ) =/= ( ( T ` { x , y } ) o. ( T ` { y , z } ) ) ) -> E. f e. ran T E. g e. ran T ( g o. f ) =/= ( f o. g ) )
41 16 25 33 40 syl3anc 
 |-  ( ( ( ( ( x e. D /\ y e. D ) /\ z e. D ) /\ ( x =/= y /\ x =/= z /\ y =/= z ) ) /\ ( D e. V /\ 3 <_ ( # ` D ) ) ) -> E. f e. ran T E. g e. ran T ( g o. f ) =/= ( f o. g ) )
42 41 exp31 
 |-  ( ( ( x e. D /\ y e. D ) /\ z e. D ) -> ( ( x =/= y /\ x =/= z /\ y =/= z ) -> ( ( D e. V /\ 3 <_ ( # ` D ) ) -> E. f e. ran T E. g e. ran T ( g o. f ) =/= ( f o. g ) ) ) )
43 42 rexlimdva 
 |-  ( ( x e. D /\ y e. D ) -> ( E. z e. D ( x =/= y /\ x =/= z /\ y =/= z ) -> ( ( D e. V /\ 3 <_ ( # ` D ) ) -> E. f e. ran T E. g e. ran T ( g o. f ) =/= ( f o. g ) ) ) )
44 43 rexlimivv 
 |-  ( E. x e. D E. y e. D E. z e. D ( x =/= y /\ x =/= z /\ y =/= z ) -> ( ( D e. V /\ 3 <_ ( # ` D ) ) -> E. f e. ran T E. g e. ran T ( g o. f ) =/= ( f o. g ) ) )
45 2 44 mpcom 
 |-  ( ( D e. V /\ 3 <_ ( # ` D ) ) -> E. f e. ran T E. g e. ran T ( g o. f ) =/= ( f o. g ) )