Metamath Proof Explorer

Theorem pmtrcnel

Description: Composing a permutation F with a transposition which results in moving at least one less point. Here the set of points moved by a permutation F is expressed as dom ( F \ _I ) . (Contributed by Thierry Arnoux, 16-Nov-2023)

Ref Expression
Hypotheses pmtrcnel.s 
|- S = ( SymGrp ` D )
pmtrcnel.t 
|- T = ( pmTrsp ` D )
pmtrcnel.b 
|- B = ( Base ` S )
pmtrcnel.j 
|- J = ( F ` I )
pmtrcnel.d 
|- ( ph -> D e. V )
pmtrcnel.f 
|- ( ph -> F e. B )
pmtrcnel.i 
|- ( ph -> I e. dom ( F \ _I ) )
Assertion pmtrcnel 
|- ( ph -> dom ( ( ( T ` { I , J } ) o. F ) \ _I ) C_ ( dom ( F \ _I ) \ { I } ) )

Proof

Step Hyp Ref Expression
1 pmtrcnel.s 
 |-  S = ( SymGrp ` D )
2 pmtrcnel.t 
 |-  T = ( pmTrsp ` D )
3 pmtrcnel.b 
 |-  B = ( Base ` S )
4 pmtrcnel.j 
 |-  J = ( F ` I )
5 pmtrcnel.d 
 |-  ( ph -> D e. V )
6 pmtrcnel.f 
 |-  ( ph -> F e. B )
7 pmtrcnel.i 
 |-  ( ph -> I e. dom ( F \ _I ) )
8 mvdco 
 |-  dom ( ( ( T ` { I , J } ) o. F ) \ _I ) C_ ( dom ( ( T ` { I , J } ) \ _I ) u. dom ( F \ _I ) )
9 difss 
 |-  ( F \ _I ) C_ F
10 dmss 
 |-  ( ( F \ _I ) C_ F -> dom ( F \ _I ) C_ dom F )
11 9 10 ax-mp 
 |-  dom ( F \ _I ) C_ dom F
12 11 7 sselid 
 |-  ( ph -> I e. dom F )
13 1 3 symgbasf1o 
 |-  ( F e. B -> F : D -1-1-onto-> D )
14 f1of 
 |-  ( F : D -1-1-onto-> D -> F : D --> D )
15 6 13 14 3syl 
 |-  ( ph -> F : D --> D )
16 15 fdmd 
 |-  ( ph -> dom F = D )
17 12 16 eleqtrd 
 |-  ( ph -> I e. D )
18 15 17 ffvelcdmd 
 |-  ( ph -> ( F ` I ) e. D )
19 4 18 eqeltrid 
 |-  ( ph -> J e. D )
20 17 19 prssd 
 |-  ( ph -> { I , J } C_ D )
21 15 ffnd 
 |-  ( ph -> F Fn D )
22 fnelnfp 
 |-  ( ( F Fn D /\ I e. D ) -> ( I e. dom ( F \ _I ) <-> ( F ` I ) =/= I ) )
23 22 biimpa 
 |-  ( ( ( F Fn D /\ I e. D ) /\ I e. dom ( F \ _I ) ) -> ( F ` I ) =/= I )
24 21 17 7 23 syl21anc 
 |-  ( ph -> ( F ` I ) =/= I )
25 24 necomd 
 |-  ( ph -> I =/= ( F ` I ) )
26 4 a1i 
 |-  ( ph -> J = ( F ` I ) )
27 25 26 neeqtrrd 
 |-  ( ph -> I =/= J )
28 enpr2 
 |-  ( ( I e. D /\ J e. D /\ I =/= J ) -> { I , J } ~~ 2o )
29 17 19 27 28 syl3anc 
 |-  ( ph -> { I , J } ~~ 2o )
30 2 pmtrmvd 
 |-  ( ( D e. V /\ { I , J } C_ D /\ { I , J } ~~ 2o ) -> dom ( ( T ` { I , J } ) \ _I ) = { I , J } )
31 5 20 29 30 syl3anc 
 |-  ( ph -> dom ( ( T ` { I , J } ) \ _I ) = { I , J } )
32 6 13 syl 
 |-  ( ph -> F : D -1-1-onto-> D )
33 f1omvdmvd 
 |-  ( ( F : D -1-1-onto-> D /\ I e. dom ( F \ _I ) ) -> ( F ` I ) e. ( dom ( F \ _I ) \ { I } ) )
34 32 7 33 syl2anc 
 |-  ( ph -> ( F ` I ) e. ( dom ( F \ _I ) \ { I } ) )
35 4 34 eqeltrid 
 |-  ( ph -> J e. ( dom ( F \ _I ) \ { I } ) )
36 35 eldifad 
 |-  ( ph -> J e. dom ( F \ _I ) )
37 7 36 prssd 
 |-  ( ph -> { I , J } C_ dom ( F \ _I ) )
38 31 37 eqsstrd 
 |-  ( ph -> dom ( ( T ` { I , J } ) \ _I ) C_ dom ( F \ _I ) )
39 ssequn1 
 |-  ( dom ( ( T ` { I , J } ) \ _I ) C_ dom ( F \ _I ) <-> ( dom ( ( T ` { I , J } ) \ _I ) u. dom ( F \ _I ) ) = dom ( F \ _I ) )
40 38 39 sylib 
 |-  ( ph -> ( dom ( ( T ` { I , J } ) \ _I ) u. dom ( F \ _I ) ) = dom ( F \ _I ) )
41 8 40 sseqtrid 
 |-  ( ph -> dom ( ( ( T ` { I , J } ) o. F ) \ _I ) C_ dom ( F \ _I ) )
42 41 sselda 
 |-  ( ( ph /\ x e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) ) -> x e. dom ( F \ _I ) )
43 simpr 
 |-  ( ( ph /\ x = I ) -> x = I )
44 eqid 
 |-  ran T = ran T
45 2 44 pmtrrn 
 |-  ( ( D e. V /\ { I , J } C_ D /\ { I , J } ~~ 2o ) -> ( T ` { I , J } ) e. ran T )
46 5 20 29 45 syl3anc 
 |-  ( ph -> ( T ` { I , J } ) e. ran T )
47 2 44 pmtrff1o 
 |-  ( ( T ` { I , J } ) e. ran T -> ( T ` { I , J } ) : D -1-1-onto-> D )
48 46 47 syl 
 |-  ( ph -> ( T ` { I , J } ) : D -1-1-onto-> D )
49 f1oco 
 |-  ( ( ( T ` { I , J } ) : D -1-1-onto-> D /\ F : D -1-1-onto-> D ) -> ( ( T ` { I , J } ) o. F ) : D -1-1-onto-> D )
50 48 32 49 syl2anc 
 |-  ( ph -> ( ( T ` { I , J } ) o. F ) : D -1-1-onto-> D )
51 f1ofn 
 |-  ( ( ( T ` { I , J } ) o. F ) : D -1-1-onto-> D -> ( ( T ` { I , J } ) o. F ) Fn D )
52 50 51 syl 
 |-  ( ph -> ( ( T ` { I , J } ) o. F ) Fn D )
53 15 17 fvco3d 
 |-  ( ph -> ( ( ( T ` { I , J } ) o. F ) ` I ) = ( ( T ` { I , J } ) ` ( F ` I ) ) )
54 26 eqcomd 
 |-  ( ph -> ( F ` I ) = J )
55 54 fveq2d 
 |-  ( ph -> ( ( T ` { I , J } ) ` ( F ` I ) ) = ( ( T ` { I , J } ) ` J ) )
56 2 pmtrprfv2 
 |-  ( ( D e. V /\ ( I e. D /\ J e. D /\ I =/= J ) ) -> ( ( T ` { I , J } ) ` J ) = I )
57 5 17 19 27 56 syl13anc 
 |-  ( ph -> ( ( T ` { I , J } ) ` J ) = I )
58 53 55 57 3eqtrd 
 |-  ( ph -> ( ( ( T ` { I , J } ) o. F ) ` I ) = I )
59 nne 
 |-  ( -. ( ( ( T ` { I , J } ) o. F ) ` I ) =/= I <-> ( ( ( T ` { I , J } ) o. F ) ` I ) = I )
60 58 59 sylibr 
 |-  ( ph -> -. ( ( ( T ` { I , J } ) o. F ) ` I ) =/= I )
61 fnelnfp 
 |-  ( ( ( ( T ` { I , J } ) o. F ) Fn D /\ I e. D ) -> ( I e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) <-> ( ( ( T ` { I , J } ) o. F ) ` I ) =/= I ) )
62 61 notbid 
 |-  ( ( ( ( T ` { I , J } ) o. F ) Fn D /\ I e. D ) -> ( -. I e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) <-> -. ( ( ( T ` { I , J } ) o. F ) ` I ) =/= I ) )
63 62 biimpar 
 |-  ( ( ( ( ( T ` { I , J } ) o. F ) Fn D /\ I e. D ) /\ -. ( ( ( T ` { I , J } ) o. F ) ` I ) =/= I ) -> -. I e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) )
64 52 17 60 63 syl21anc 
 |-  ( ph -> -. I e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) )
65 64 adantr 
 |-  ( ( ph /\ x = I ) -> -. I e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) )
66 43 65 eqneltrd 
 |-  ( ( ph /\ x = I ) -> -. x e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) )
67 66 ex 
 |-  ( ph -> ( x = I -> -. x e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) ) )
68 67 necon2ad 
 |-  ( ph -> ( x e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) -> x =/= I ) )
69 68 imp 
 |-  ( ( ph /\ x e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) ) -> x =/= I )
70 eldifsn 
 |-  ( x e. ( dom ( F \ _I ) \ { I } ) <-> ( x e. dom ( F \ _I ) /\ x =/= I ) )
71 42 69 70 sylanbrc 
 |-  ( ( ph /\ x e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) ) -> x e. ( dom ( F \ _I ) \ { I } ) )
72 71 ex 
 |-  ( ph -> ( x e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) -> x e. ( dom ( F \ _I ) \ { I } ) ) )
73 72 ssrdv 
 |-  ( ph -> dom ( ( ( T ` { I , J } ) o. F ) \ _I ) C_ ( dom ( F \ _I ) \ { I } ) )