Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pmtrcnelor Structured version   Visualization version   GIF version

Theorem pmtrcnelor 30834
 Description: Composing a permutation 𝐹 with a transposition which results in moving one or two less points. (Contributed by Thierry Arnoux, 16-Nov-2023.)
Hypotheses
Ref Expression
pmtrcnel.s 𝑆 = (SymGrp‘𝐷)
pmtrcnel.t 𝑇 = (pmTrsp‘𝐷)
pmtrcnel.b 𝐵 = (Base‘𝑆)
pmtrcnel.j 𝐽 = (𝐹𝐼)
pmtrcnel.d (𝜑𝐷𝑉)
pmtrcnel.f (𝜑𝐹𝐵)
pmtrcnel.i (𝜑𝐼 ∈ dom (𝐹 ∖ I ))
pmtrcnel.e 𝐸 = dom (𝐹 ∖ I )
pmtrcnel.a 𝐴 = dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I )
Assertion
Ref Expression
pmtrcnelor (𝜑 → (𝐴 = (𝐸 ∖ {𝐼, 𝐽}) ∨ 𝐴 = (𝐸 ∖ {𝐼})))

Proof of Theorem pmtrcnelor
StepHypRef Expression
1 pmtrcnel.s . . . . . . 7 𝑆 = (SymGrp‘𝐷)
2 pmtrcnel.t . . . . . . 7 𝑇 = (pmTrsp‘𝐷)
3 pmtrcnel.b . . . . . . 7 𝐵 = (Base‘𝑆)
4 pmtrcnel.j . . . . . . 7 𝐽 = (𝐹𝐼)
5 pmtrcnel.d . . . . . . 7 (𝜑𝐷𝑉)
6 pmtrcnel.f . . . . . . 7 (𝜑𝐹𝐵)
7 pmtrcnel.i . . . . . . 7 (𝜑𝐼 ∈ dom (𝐹 ∖ I ))
81, 2, 3, 4, 5, 6, 7pmtrcnel 30832 . . . . . 6 (𝜑 → dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ) ⊆ (dom (𝐹 ∖ I ) ∖ {𝐼}))
9 pmtrcnel.a . . . . . 6 𝐴 = dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I )
10 pmtrcnel.e . . . . . . 7 𝐸 = dom (𝐹 ∖ I )
1110difeq1i 4049 . . . . . 6 (𝐸 ∖ {𝐼}) = (dom (𝐹 ∖ I ) ∖ {𝐼})
128, 9, 113sstr4g 3962 . . . . 5 (𝜑𝐴 ⊆ (𝐸 ∖ {𝐼}))
1312ssdifd 4071 . . . 4 (𝜑 → (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) ⊆ ((𝐸 ∖ {𝐼}) ∖ (𝐸 ∖ {𝐼, 𝐽})))
14 difpr 4699 . . . . . 6 (𝐸 ∖ {𝐼, 𝐽}) = ((𝐸 ∖ {𝐼}) ∖ {𝐽})
1514difeq2i 4050 . . . . 5 ((𝐸 ∖ {𝐼}) ∖ (𝐸 ∖ {𝐼, 𝐽})) = ((𝐸 ∖ {𝐼}) ∖ ((𝐸 ∖ {𝐼}) ∖ {𝐽}))
161, 3symgbasf1o 18516 . . . . . . . . . . . . 13 (𝐹𝐵𝐹:𝐷1-1-onto𝐷)
176, 16syl 17 . . . . . . . . . . . 12 (𝜑𝐹:𝐷1-1-onto𝐷)
18 f1omvdmvd 18584 . . . . . . . . . . . 12 ((𝐹:𝐷1-1-onto𝐷𝐼 ∈ dom (𝐹 ∖ I )) → (𝐹𝐼) ∈ (dom (𝐹 ∖ I ) ∖ {𝐼}))
1917, 7, 18syl2anc 587 . . . . . . . . . . 11 (𝜑 → (𝐹𝐼) ∈ (dom (𝐹 ∖ I ) ∖ {𝐼}))
204, 19eqeltrid 2894 . . . . . . . . . 10 (𝜑𝐽 ∈ (dom (𝐹 ∖ I ) ∖ {𝐼}))
2120eldifad 3895 . . . . . . . . 9 (𝜑𝐽 ∈ dom (𝐹 ∖ I ))
2221, 10eleqtrrdi 2901 . . . . . . . 8 (𝜑𝐽𝐸)
234a1i 11 . . . . . . . . 9 (𝜑𝐽 = (𝐹𝐼))
24 f1of 6599 . . . . . . . . . . . 12 (𝐹:𝐷1-1-onto𝐷𝐹:𝐷𝐷)
2517, 24syl 17 . . . . . . . . . . 11 (𝜑𝐹:𝐷𝐷)
2625ffnd 6496 . . . . . . . . . 10 (𝜑𝐹 Fn 𝐷)
27 difss 4062 . . . . . . . . . . . . 13 (𝐹 ∖ I ) ⊆ 𝐹
28 dmss 5741 . . . . . . . . . . . . 13 ((𝐹 ∖ I ) ⊆ 𝐹 → dom (𝐹 ∖ I ) ⊆ dom 𝐹)
2927, 28ax-mp 5 . . . . . . . . . . . 12 dom (𝐹 ∖ I ) ⊆ dom 𝐹
3029, 7sseldi 3915 . . . . . . . . . . 11 (𝜑𝐼 ∈ dom 𝐹)
3125fdmd 6505 . . . . . . . . . . 11 (𝜑 → dom 𝐹 = 𝐷)
3230, 31eleqtrd 2892 . . . . . . . . . 10 (𝜑𝐼𝐷)
33 fnelnfp 6926 . . . . . . . . . . 11 ((𝐹 Fn 𝐷𝐼𝐷) → (𝐼 ∈ dom (𝐹 ∖ I ) ↔ (𝐹𝐼) ≠ 𝐼))
3433biimpa 480 . . . . . . . . . 10 (((𝐹 Fn 𝐷𝐼𝐷) ∧ 𝐼 ∈ dom (𝐹 ∖ I )) → (𝐹𝐼) ≠ 𝐼)
3526, 32, 7, 34syl21anc 836 . . . . . . . . 9 (𝜑 → (𝐹𝐼) ≠ 𝐼)
3623, 35eqnetrd 3054 . . . . . . . 8 (𝜑𝐽𝐼)
37 eldifsn 4683 . . . . . . . 8 (𝐽 ∈ (𝐸 ∖ {𝐼}) ↔ (𝐽𝐸𝐽𝐼))
3822, 36, 37sylanbrc 586 . . . . . . 7 (𝜑𝐽 ∈ (𝐸 ∖ {𝐼}))
3938snssd 4705 . . . . . 6 (𝜑 → {𝐽} ⊆ (𝐸 ∖ {𝐼}))
40 dfss4 4188 . . . . . 6 ({𝐽} ⊆ (𝐸 ∖ {𝐼}) ↔ ((𝐸 ∖ {𝐼}) ∖ ((𝐸 ∖ {𝐼}) ∖ {𝐽})) = {𝐽})
4139, 40sylib 221 . . . . 5 (𝜑 → ((𝐸 ∖ {𝐼}) ∖ ((𝐸 ∖ {𝐼}) ∖ {𝐽})) = {𝐽})
4215, 41syl5eq 2845 . . . 4 (𝜑 → ((𝐸 ∖ {𝐼}) ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽})
4313, 42sseqtrd 3957 . . 3 (𝜑 → (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) ⊆ {𝐽})
44 sssn 4722 . . 3 ((𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) ⊆ {𝐽} ↔ ((𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅ ∨ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}))
4543, 44sylib 221 . 2 (𝜑 → ((𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅ ∨ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}))
46 simpr 488 . . . . 5 ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅) → (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅)
471, 2, 3, 4, 5, 6, 7pmtrcnel2 30833 . . . . . . . 8 (𝜑 → (dom (𝐹 ∖ I ) ∖ {𝐼, 𝐽}) ⊆ dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ))
4810difeq1i 4049 . . . . . . . 8 (𝐸 ∖ {𝐼, 𝐽}) = (dom (𝐹 ∖ I ) ∖ {𝐼, 𝐽})
4947, 48, 93sstr4g 3962 . . . . . . 7 (𝜑 → (𝐸 ∖ {𝐼, 𝐽}) ⊆ 𝐴)
50 ssdif0 4280 . . . . . . 7 ((𝐸 ∖ {𝐼, 𝐽}) ⊆ 𝐴 ↔ ((𝐸 ∖ {𝐼, 𝐽}) ∖ 𝐴) = ∅)
5149, 50sylib 221 . . . . . 6 (𝜑 → ((𝐸 ∖ {𝐼, 𝐽}) ∖ 𝐴) = ∅)
5251adantr 484 . . . . 5 ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅) → ((𝐸 ∖ {𝐼, 𝐽}) ∖ 𝐴) = ∅)
53 eqdif 30334 . . . . 5 (((𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅ ∧ ((𝐸 ∖ {𝐼, 𝐽}) ∖ 𝐴) = ∅) → 𝐴 = (𝐸 ∖ {𝐼, 𝐽}))
5446, 52, 53syl2anc 587 . . . 4 ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅) → 𝐴 = (𝐸 ∖ {𝐼, 𝐽}))
5554ex 416 . . 3 (𝜑 → ((𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅ → 𝐴 = (𝐸 ∖ {𝐼, 𝐽})))
5612adantr 484 . . . . 5 ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → 𝐴 ⊆ (𝐸 ∖ {𝐼}))
5714, 49eqsstrrid 3966 . . . . . . . 8 (𝜑 → ((𝐸 ∖ {𝐼}) ∖ {𝐽}) ⊆ 𝐴)
5857adantr 484 . . . . . . 7 ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → ((𝐸 ∖ {𝐼}) ∖ {𝐽}) ⊆ 𝐴)
59 ssundif 4394 . . . . . . 7 ((𝐸 ∖ {𝐼}) ⊆ ({𝐽} ∪ 𝐴) ↔ ((𝐸 ∖ {𝐼}) ∖ {𝐽}) ⊆ 𝐴)
6058, 59sylibr 237 . . . . . 6 ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → (𝐸 ∖ {𝐼}) ⊆ ({𝐽} ∪ 𝐴))
61 ssidd 3940 . . . . . . . . 9 ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → {𝐽} ⊆ {𝐽})
62 simpr 488 . . . . . . . . 9 ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽})
6361, 62sseqtrrd 3958 . . . . . . . 8 ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → {𝐽} ⊆ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})))
6463difss2d 4065 . . . . . . 7 ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → {𝐽} ⊆ 𝐴)
65 ssequn1 4110 . . . . . . 7 ({𝐽} ⊆ 𝐴 ↔ ({𝐽} ∪ 𝐴) = 𝐴)
6664, 65sylib 221 . . . . . 6 ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → ({𝐽} ∪ 𝐴) = 𝐴)
6760, 66sseqtrd 3957 . . . . 5 ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → (𝐸 ∖ {𝐼}) ⊆ 𝐴)
6856, 67eqssd 3934 . . . 4 ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → 𝐴 = (𝐸 ∖ {𝐼}))
6968ex 416 . . 3 (𝜑 → ((𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽} → 𝐴 = (𝐸 ∖ {𝐼})))
7055, 69orim12d 962 . 2 (𝜑 → (((𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅ ∨ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → (𝐴 = (𝐸 ∖ {𝐼, 𝐽}) ∨ 𝐴 = (𝐸 ∖ {𝐼}))))
7145, 70mpd 15 1 (𝜑 → (𝐴 = (𝐸 ∖ {𝐼, 𝐽}) ∨ 𝐴 = (𝐸 ∖ {𝐼})))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111   ≠ wne 2987   ∖ cdif 3880   ∪ cun 3881   ⊆ wss 3883  ∅c0 4246  {csn 4528  {cpr 4530   I cid 5428  dom cdm 5523   ∘ ccom 5527   Fn wfn 6327  ⟶wf 6328  –1-1-onto→wf1o 6331  ‘cfv 6332  Basecbs 16495  SymGrpcsymg 18508  pmTrspcpmtr 18582 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5158  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454  ax-cnex 10600  ax-resscn 10601  ax-1cn 10602  ax-icn 10603  ax-addcl 10604  ax-addrcl 10605  ax-mulcl 10606  ax-mulrcl 10607  ax-mulcom 10608  ax-addass 10609  ax-mulass 10610  ax-distr 10611  ax-i2m1 10612  ax-1ne0 10613  ax-1rid 10614  ax-rnegex 10615  ax-rrecex 10616  ax-cnre 10617  ax-pre-lttri 10618  ax-pre-lttrn 10619  ax-pre-ltadd 10620  ax-pre-mulgt0 10621 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4805  df-int 4843  df-iun 4887  df-br 5035  df-opab 5097  df-mpt 5115  df-tr 5141  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7574  df-1st 7684  df-2nd 7685  df-wrecs 7948  df-recs 8009  df-rdg 8047  df-1o 8103  df-2o 8104  df-oadd 8107  df-er 8290  df-map 8409  df-en 8511  df-dom 8512  df-sdom 8513  df-fin 8514  df-pnf 10684  df-mnf 10685  df-xr 10686  df-ltxr 10687  df-le 10688  df-sub 10879  df-neg 10880  df-nn 11644  df-2 11706  df-3 11707  df-4 11708  df-5 11709  df-6 11710  df-7 11711  df-8 11712  df-9 11713  df-n0 11904  df-z 11990  df-uz 12252  df-fz 12906  df-struct 16497  df-ndx 16498  df-slot 16499  df-base 16501  df-sets 16502  df-ress 16503  df-plusg 16590  df-tset 16596  df-efmnd 18046  df-symg 18509  df-pmtr 18583 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator