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

Theorem tocycf 32972
Description: The permutation cycle builder as a function. (Contributed by Thierry Arnoux, 25-Sep-2023.)
Hypotheses
Ref Expression
tocycf.c 𝐶 = (toCyc‘𝐷)
tocycf.s 𝑆 = (SymGrp‘𝐷)
tocycf.b 𝐵 = (Base‘𝑆)
Assertion
Ref Expression
tocycf (𝐷𝑉𝐶:{𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}⟶𝐵)
Distinct variable group:   𝑤,𝐷
Allowed substitution hints:   𝐵(𝑤)   𝐶(𝑤)   𝑆(𝑤)   𝑉(𝑤)

Proof of Theorem tocycf
Dummy variable 𝑢 is distinct from all other variables.
StepHypRef Expression
1 tocycf.c . . 3 𝐶 = (toCyc‘𝐷)
21tocycval 32963 . 2 (𝐷𝑉𝐶 = (𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ↦ (( I ↾ (𝐷 ∖ ran 𝑢)) ∪ ((𝑢 cyclShift 1) ∘ 𝑢))))
3 simpr 483 . . . . . . . . . . 11 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 = ∅) → 𝑢 = ∅)
43rneqd 5943 . . . . . . . . . 10 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 = ∅) → ran 𝑢 = ran ∅)
5 rn0 5931 . . . . . . . . . 10 ran ∅ = ∅
64, 5eqtrdi 2781 . . . . . . . . 9 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 = ∅) → ran 𝑢 = ∅)
76difeq2d 4120 . . . . . . . 8 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 = ∅) → (𝐷 ∖ ran 𝑢) = (𝐷 ∖ ∅))
8 dif0 4376 . . . . . . . 8 (𝐷 ∖ ∅) = 𝐷
97, 8eqtrdi 2781 . . . . . . 7 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 = ∅) → (𝐷 ∖ ran 𝑢) = 𝐷)
109reseq2d 5988 . . . . . 6 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 = ∅) → ( I ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ 𝐷))
113cnveqd 5881 . . . . . . . . 9 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 = ∅) → 𝑢 = ∅)
12 cnv0 6151 . . . . . . . . 9 ∅ = ∅
1311, 12eqtrdi 2781 . . . . . . . 8 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 = ∅) → 𝑢 = ∅)
1413coeq2d 5868 . . . . . . 7 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 = ∅) → ((𝑢 cyclShift 1) ∘ 𝑢) = ((𝑢 cyclShift 1) ∘ ∅))
15 co02 6270 . . . . . . 7 ((𝑢 cyclShift 1) ∘ ∅) = ∅
1614, 15eqtrdi 2781 . . . . . 6 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 = ∅) → ((𝑢 cyclShift 1) ∘ 𝑢) = ∅)
1710, 16uneq12d 4163 . . . . 5 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 = ∅) → (( I ↾ (𝐷 ∖ ran 𝑢)) ∪ ((𝑢 cyclShift 1) ∘ 𝑢)) = (( I ↾ 𝐷) ∪ ∅))
18 un0 4394 . . . . 5 (( I ↾ 𝐷) ∪ ∅) = ( I ↾ 𝐷)
1917, 18eqtrdi 2781 . . . 4 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 = ∅) → (( I ↾ (𝐷 ∖ ran 𝑢)) ∪ ((𝑢 cyclShift 1) ∘ 𝑢)) = ( I ↾ 𝐷))
20 tocycf.s . . . . . . 7 𝑆 = (SymGrp‘𝐷)
2120idresperm 19378 . . . . . 6 (𝐷𝑉 → ( I ↾ 𝐷) ∈ (Base‘𝑆))
22 tocycf.b . . . . . 6 𝐵 = (Base‘𝑆)
2321, 22eleqtrrdi 2836 . . . . 5 (𝐷𝑉 → ( I ↾ 𝐷) ∈ 𝐵)
2423ad2antrr 724 . . . 4 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 = ∅) → ( I ↾ 𝐷) ∈ 𝐵)
2519, 24eqeltrd 2825 . . 3 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 = ∅) → (( I ↾ (𝐷 ∖ ran 𝑢)) ∪ ((𝑢 cyclShift 1) ∘ 𝑢)) ∈ 𝐵)
26 difexg 5333 . . . . . . . . 9 (𝐷𝑉 → (𝐷 ∖ ran 𝑢) ∈ V)
2726resiexd 7232 . . . . . . . 8 (𝐷𝑉 → ( I ↾ (𝐷 ∖ ran 𝑢)) ∈ V)
28 ovex 7456 . . . . . . . . 9 (𝑢 cyclShift 1) ∈ V
29 vex 3465 . . . . . . . . . 10 𝑢 ∈ V
3029cnvex 7937 . . . . . . . . 9 𝑢 ∈ V
3128, 30coex 7942 . . . . . . . 8 ((𝑢 cyclShift 1) ∘ 𝑢) ∈ V
32 unexg 7756 . . . . . . . 8 ((( I ↾ (𝐷 ∖ ran 𝑢)) ∈ V ∧ ((𝑢 cyclShift 1) ∘ 𝑢) ∈ V) → (( I ↾ (𝐷 ∖ ran 𝑢)) ∪ ((𝑢 cyclShift 1) ∘ 𝑢)) ∈ V)
3327, 31, 32sylancl 584 . . . . . . 7 (𝐷𝑉 → (( I ↾ (𝐷 ∖ ran 𝑢)) ∪ ((𝑢 cyclShift 1) ∘ 𝑢)) ∈ V)
3433adantr 479 . . . . . 6 ((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) → (( I ↾ (𝐷 ∖ ran 𝑢)) ∪ ((𝑢 cyclShift 1) ∘ 𝑢)) ∈ V)
352, 34fvmpt2d 7021 . . . . 5 ((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) → (𝐶𝑢) = (( I ↾ (𝐷 ∖ ran 𝑢)) ∪ ((𝑢 cyclShift 1) ∘ 𝑢)))
3635adantr 479 . . . 4 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 ≠ ∅) → (𝐶𝑢) = (( I ↾ (𝐷 ∖ ran 𝑢)) ∪ ((𝑢 cyclShift 1) ∘ 𝑢)))
37 simpll 765 . . . . . 6 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 ≠ ∅) → 𝐷𝑉)
38 simplr 767 . . . . . . . 8 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 ≠ ∅) → 𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
39 id 22 . . . . . . . . . 10 (𝑤 = 𝑢𝑤 = 𝑢)
40 dmeq 5909 . . . . . . . . . 10 (𝑤 = 𝑢 → dom 𝑤 = dom 𝑢)
41 eqidd 2726 . . . . . . . . . 10 (𝑤 = 𝑢𝐷 = 𝐷)
4239, 40, 41f1eq123d 6834 . . . . . . . . 9 (𝑤 = 𝑢 → (𝑤:dom 𝑤1-1𝐷𝑢:dom 𝑢1-1𝐷))
4342elrab 3680 . . . . . . . 8 (𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ↔ (𝑢 ∈ Word 𝐷𝑢:dom 𝑢1-1𝐷))
4438, 43sylib 217 . . . . . . 7 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 ≠ ∅) → (𝑢 ∈ Word 𝐷𝑢:dom 𝑢1-1𝐷))
4544simpld 493 . . . . . 6 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 ≠ ∅) → 𝑢 ∈ Word 𝐷)
4644simprd 494 . . . . . 6 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 ≠ ∅) → 𝑢:dom 𝑢1-1𝐷)
471, 37, 45, 46, 20cycpmcl 32971 . . . . 5 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 ≠ ∅) → (𝐶𝑢) ∈ (Base‘𝑆))
4847, 22eleqtrrdi 2836 . . . 4 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 ≠ ∅) → (𝐶𝑢) ∈ 𝐵)
4936, 48eqeltrrd 2826 . . 3 (((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) ∧ 𝑢 ≠ ∅) → (( I ↾ (𝐷 ∖ ran 𝑢)) ∪ ((𝑢 cyclShift 1) ∘ 𝑢)) ∈ 𝐵)
5025, 49pm2.61dane 3018 . 2 ((𝐷𝑉𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) → (( I ↾ (𝐷 ∖ ran 𝑢)) ∪ ((𝑢 cyclShift 1) ∘ 𝑢)) ∈ 𝐵)
512, 50fmpt3d 7129 1 (𝐷𝑉𝐶:{𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}⟶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1533  wcel 2098  wne 2929  {crab 3418  Vcvv 3461  cdif 3943  cun 3944  c0 4324   I cid 5578  ccnv 5680  dom cdm 5681  ran crn 5682  cres 5683  ccom 5685  wf 6549  1-1wf1 6550  cfv 6553  (class class class)co 7423  1c1 11155  Word cword 14517   cyclShift ccsh 14791  Basecbs 17208  SymGrpcsymg 19359  toCycctocyc 32961
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5368  ax-pr 5432  ax-un 7745  ax-cnex 11210  ax-resscn 11211  ax-1cn 11212  ax-icn 11213  ax-addcl 11214  ax-addrcl 11215  ax-mulcl 11216  ax-mulrcl 11217  ax-mulcom 11218  ax-addass 11219  ax-mulass 11220  ax-distr 11221  ax-i2m1 11222  ax-1ne0 11223  ax-1rid 11224  ax-rnegex 11225  ax-rrecex 11226  ax-cnre 11227  ax-pre-lttri 11228  ax-pre-lttrn 11229  ax-pre-ltadd 11230  ax-pre-mulgt0 11231  ax-pre-sup 11232
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5579  df-eprel 5585  df-po 5593  df-so 5594  df-fr 5636  df-we 5638  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-pred 6311  df-ord 6378  df-on 6379  df-lim 6380  df-suc 6381  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7379  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7876  df-1st 8002  df-2nd 8003  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-1o 8495  df-er 8733  df-map 8856  df-en 8974  df-dom 8975  df-sdom 8976  df-fin 8977  df-sup 9481  df-inf 9482  df-card 9978  df-pnf 11296  df-mnf 11297  df-xr 11298  df-ltxr 11299  df-le 11300  df-sub 11492  df-neg 11493  df-div 11918  df-nn 12260  df-2 12322  df-3 12323  df-4 12324  df-5 12325  df-6 12326  df-7 12327  df-8 12328  df-9 12329  df-n0 12520  df-z 12606  df-uz 12870  df-rp 13024  df-fz 13534  df-fzo 13677  df-fl 13807  df-mod 13885  df-hash 14343  df-word 14518  df-concat 14574  df-substr 14644  df-pfx 14674  df-csh 14792  df-struct 17144  df-sets 17161  df-slot 17179  df-ndx 17191  df-base 17209  df-ress 17238  df-plusg 17274  df-tset 17280  df-efmnd 18854  df-symg 19360  df-tocyc 32962
This theorem is referenced by:  tocyc01  32973  cycpmco2f1  32979  cycpmco2rn  32980  cycpmco2lem1  32981  cycpmco2lem2  32982  cycpmco2lem3  32983  cycpmco2lem4  32984  cycpmco2lem5  32985  cycpmco2lem6  32986  cycpmco2lem7  32987  cycpmco2  32988  cycpm3cl2  32991  cycpmconjv  32997  tocyccntz  32999  cyc3evpm  33005  cycpmgcl  33008  cycpmconjslem2  33010  cyc3conja  33012
  Copyright terms: Public domain W3C validator