Metamath Proof Explorer

Theorem pmtrcnelor

Description: Composing a permutation F with a transposition which results in moving one or two less points. (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 ) )
pmtrcnel.e 
|- E = dom ( F \ _I )
pmtrcnel.a 
|- A = dom ( ( ( T ` { I , J } ) o. F ) \ _I )
Assertion pmtrcnelor 
|- ( ph -> ( A = ( E \ { I , J } ) \/ A = ( E \ { 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 pmtrcnel.e 
 |-  E = dom ( F \ _I )
9 pmtrcnel.a 
 |-  A = dom ( ( ( T ` { I , J } ) o. F ) \ _I )
10 1 2 3 4 5 6 7 pmtrcnel 
 |-  ( ph -> dom ( ( ( T ` { I , J } ) o. F ) \ _I ) C_ ( dom ( F \ _I ) \ { I } ) )
11 8 difeq1i 
 |-  ( E \ { I } ) = ( dom ( F \ _I ) \ { I } )
12 10 9 11 3sstr4g 
 |-  ( ph -> A C_ ( E \ { I } ) )
13 12 ssdifd 
 |-  ( ph -> ( A \ ( E \ { I , J } ) ) C_ ( ( E \ { I } ) \ ( E \ { I , J } ) ) )
14 difpr 
 |-  ( E \ { I , J } ) = ( ( E \ { I } ) \ { J } )
15 14 difeq2i 
 |-  ( ( E \ { I } ) \ ( E \ { I , J } ) ) = ( ( E \ { I } ) \ ( ( E \ { I } ) \ { J } ) )
16 1 3 symgbasf1o 
 |-  ( F e. B -> F : D -1-1-onto-> D )
17 6 16 syl 
 |-  ( ph -> F : D -1-1-onto-> D )
18 f1omvdmvd 
 |-  ( ( F : D -1-1-onto-> D /\ I e. dom ( F \ _I ) ) -> ( F ` I ) e. ( dom ( F \ _I ) \ { I } ) )
19 17 7 18 syl2anc 
 |-  ( ph -> ( F ` I ) e. ( dom ( F \ _I ) \ { I } ) )
20 4 19 eqeltrid 
 |-  ( ph -> J e. ( dom ( F \ _I ) \ { I } ) )
21 20 eldifad 
 |-  ( ph -> J e. dom ( F \ _I ) )
22 21 8 eleqtrrdi 
 |-  ( ph -> J e. E )
23 4 a1i 
 |-  ( ph -> J = ( F ` I ) )
24 f1of 
 |-  ( F : D -1-1-onto-> D -> F : D --> D )
25 17 24 syl 
 |-  ( ph -> F : D --> D )
26 25 ffnd 
 |-  ( ph -> F Fn D )
27 difss 
 |-  ( F \ _I ) C_ F
28 dmss 
 |-  ( ( F \ _I ) C_ F -> dom ( F \ _I ) C_ dom F )
29 27 28 ax-mp 
 |-  dom ( F \ _I ) C_ dom F
30 29 7 sselid 
 |-  ( ph -> I e. dom F )
31 25 fdmd 
 |-  ( ph -> dom F = D )
32 30 31 eleqtrd 
 |-  ( ph -> I e. D )
33 fnelnfp 
 |-  ( ( F Fn D /\ I e. D ) -> ( I e. dom ( F \ _I ) <-> ( F ` I ) =/= I ) )
34 33 biimpa 
 |-  ( ( ( F Fn D /\ I e. D ) /\ I e. dom ( F \ _I ) ) -> ( F ` I ) =/= I )
35 26 32 7 34 syl21anc 
 |-  ( ph -> ( F ` I ) =/= I )
36 23 35 eqnetrd 
 |-  ( ph -> J =/= I )
37 eldifsn 
 |-  ( J e. ( E \ { I } ) <-> ( J e. E /\ J =/= I ) )
38 22 36 37 sylanbrc 
 |-  ( ph -> J e. ( E \ { I } ) )
39 38 snssd 
 |-  ( ph -> { J } C_ ( E \ { I } ) )
40 dfss4 
 |-  ( { J } C_ ( E \ { I } ) <-> ( ( E \ { I } ) \ ( ( E \ { I } ) \ { J } ) ) = { J } )
41 39 40 sylib 
 |-  ( ph -> ( ( E \ { I } ) \ ( ( E \ { I } ) \ { J } ) ) = { J } )
42 15 41 syl5eq 
 |-  ( ph -> ( ( E \ { I } ) \ ( E \ { I , J } ) ) = { J } )
43 13 42 sseqtrd 
 |-  ( ph -> ( A \ ( E \ { I , J } ) ) C_ { J } )
44 sssn 
 |-  ( ( A \ ( E \ { I , J } ) ) C_ { J } <-> ( ( A \ ( E \ { I , J } ) ) = (/) \/ ( A \ ( E \ { I , J } ) ) = { J } ) )
45 43 44 sylib 
 |-  ( ph -> ( ( A \ ( E \ { I , J } ) ) = (/) \/ ( A \ ( E \ { I , J } ) ) = { J } ) )
46 simpr 
 |-  ( ( ph /\ ( A \ ( E \ { I , J } ) ) = (/) ) -> ( A \ ( E \ { I , J } ) ) = (/) )
47 1 2 3 4 5 6 7 pmtrcnel2 
 |-  ( ph -> ( dom ( F \ _I ) \ { I , J } ) C_ dom ( ( ( T ` { I , J } ) o. F ) \ _I ) )
48 8 difeq1i 
 |-  ( E \ { I , J } ) = ( dom ( F \ _I ) \ { I , J } )
49 47 48 9 3sstr4g 
 |-  ( ph -> ( E \ { I , J } ) C_ A )
50 ssdif0 
 |-  ( ( E \ { I , J } ) C_ A <-> ( ( E \ { I , J } ) \ A ) = (/) )
51 49 50 sylib 
 |-  ( ph -> ( ( E \ { I , J } ) \ A ) = (/) )
52 51 adantr 
 |-  ( ( ph /\ ( A \ ( E \ { I , J } ) ) = (/) ) -> ( ( E \ { I , J } ) \ A ) = (/) )
53 eqdif 
 |-  ( ( ( A \ ( E \ { I , J } ) ) = (/) /\ ( ( E \ { I , J } ) \ A ) = (/) ) -> A = ( E \ { I , J } ) )
54 46 52 53 syl2anc 
 |-  ( ( ph /\ ( A \ ( E \ { I , J } ) ) = (/) ) -> A = ( E \ { I , J } ) )
55 54 ex 
 |-  ( ph -> ( ( A \ ( E \ { I , J } ) ) = (/) -> A = ( E \ { I , J } ) ) )
56 12 adantr 
 |-  ( ( ph /\ ( A \ ( E \ { I , J } ) ) = { J } ) -> A C_ ( E \ { I } ) )
57 14 49 eqsstrrid 
 |-  ( ph -> ( ( E \ { I } ) \ { J } ) C_ A )
58 57 adantr 
 |-  ( ( ph /\ ( A \ ( E \ { I , J } ) ) = { J } ) -> ( ( E \ { I } ) \ { J } ) C_ A )
59 ssundif 
 |-  ( ( E \ { I } ) C_ ( { J } u. A ) <-> ( ( E \ { I } ) \ { J } ) C_ A )
60 58 59 sylibr 
 |-  ( ( ph /\ ( A \ ( E \ { I , J } ) ) = { J } ) -> ( E \ { I } ) C_ ( { J } u. A ) )
61 ssidd 
 |-  ( ( ph /\ ( A \ ( E \ { I , J } ) ) = { J } ) -> { J } C_ { J } )
62 simpr 
 |-  ( ( ph /\ ( A \ ( E \ { I , J } ) ) = { J } ) -> ( A \ ( E \ { I , J } ) ) = { J } )
63 61 62 sseqtrrd 
 |-  ( ( ph /\ ( A \ ( E \ { I , J } ) ) = { J } ) -> { J } C_ ( A \ ( E \ { I , J } ) ) )
64 63 difss2d 
 |-  ( ( ph /\ ( A \ ( E \ { I , J } ) ) = { J } ) -> { J } C_ A )
65 ssequn1 
 |-  ( { J } C_ A <-> ( { J } u. A ) = A )
66 64 65 sylib 
 |-  ( ( ph /\ ( A \ ( E \ { I , J } ) ) = { J } ) -> ( { J } u. A ) = A )
67 60 66 sseqtrd 
 |-  ( ( ph /\ ( A \ ( E \ { I , J } ) ) = { J } ) -> ( E \ { I } ) C_ A )
68 56 67 eqssd 
 |-  ( ( ph /\ ( A \ ( E \ { I , J } ) ) = { J } ) -> A = ( E \ { I } ) )
69 68 ex 
 |-  ( ph -> ( ( A \ ( E \ { I , J } ) ) = { J } -> A = ( E \ { I } ) ) )
70 55 69 orim12d 
 |-  ( ph -> ( ( ( A \ ( E \ { I , J } ) ) = (/) \/ ( A \ ( E \ { I , J } ) ) = { J } ) -> ( A = ( E \ { I , J } ) \/ A = ( E \ { I } ) ) ) )
71 45 70 mpd 
 |-  ( ph -> ( A = ( E \ { I , J } ) \/ A = ( E \ { I } ) ) )