Metamath Proof Explorer

Theorem tocycf

Description: The permutation cycle builder as a function. (Contributed by Thierry Arnoux, 25-Sep-2023)

Ref Expression
Hypotheses tocycf.c ⊢C=toCyc⁡D
tocycf.s ⊢S=SymGrp⁡D
tocycf.b ⊢B=BaseS
Assertion tocycf ⊢D∈V→C:w∈WordD|w:dom⁡w⟶1-1D⟶B

Proof

Step Hyp Ref Expression
1 tocycf.c ⊢C=toCyc⁡D
2 tocycf.s ⊢S=SymGrp⁡D
3 tocycf.b ⊢B=BaseS
4 1 tocycval ⊢D∈V→C=u∈w∈WordD|w:dom⁡w⟶1-1D⟼I↾D∖ran⁡u∪ucyclShift1∘u-1
5 simpr ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u=∅→u=∅
6 5 rneqd ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u=∅→ran⁡u=ran⁡∅
7 rn0 ⊢ran⁡∅=∅
8 6 7 eqtrdi ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u=∅→ran⁡u=∅
9 8 difeq2d ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u=∅→D∖ran⁡u=D∖∅
10 dif0 ⊢D∖∅=D
11 9 10 eqtrdi ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u=∅→D∖ran⁡u=D
12 11 reseq2d ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u=∅→I↾D∖ran⁡u=I↾D
13 5 cnveqd ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u=∅→u-1=∅-1
14 cnv0 ⊢∅-1=∅
15 13 14 eqtrdi ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u=∅→u-1=∅
16 15 coeq2d ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u=∅→ucyclShift1∘u-1=ucyclShift1∘∅
17 co02 ⊢ucyclShift1∘∅=∅
18 16 17 eqtrdi ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u=∅→ucyclShift1∘u-1=∅
19 12 18 uneq12d ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u=∅→I↾D∖ran⁡u∪ucyclShift1∘u-1=I↾D∪∅
20 un0 ⊢I↾D∪∅=I↾D
21 19 20 eqtrdi ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u=∅→I↾D∖ran⁡u∪ucyclShift1∘u-1=I↾D
22 2 idresperm ⊢D∈V→I↾D∈BaseS
23 22 3 eleqtrrdi ⊢D∈V→I↾D∈B
24 23 ad2antrr ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u=∅→I↾D∈B
25 21 24 eqeltrd ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u=∅→I↾D∖ran⁡u∪ucyclShift1∘u-1∈B
26 difexg ⊢D∈V→D∖ran⁡u∈V
27 26 resiexd ⊢D∈V→I↾D∖ran⁡u∈V
28 ovex ⊢ucyclShift1∈V
29 vex ⊢u∈V
30 29 cnvex ⊢u-1∈V
31 28 30 coex ⊢ucyclShift1∘u-1∈V
32 unexg ⊢I↾D∖ran⁡u∈V∧ucyclShift1∘u-1∈V→I↾D∖ran⁡u∪ucyclShift1∘u-1∈V
33 27 31 32 sylancl ⊢D∈V→I↾D∖ran⁡u∪ucyclShift1∘u-1∈V
34 33 adantr ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D→I↾D∖ran⁡u∪ucyclShift1∘u-1∈V
35 4 34 fvmpt2d ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D→C⁡u=I↾D∖ran⁡u∪ucyclShift1∘u-1
36 35 adantr ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u≠∅→C⁡u=I↾D∖ran⁡u∪ucyclShift1∘u-1
37 simpll ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u≠∅→D∈V
38 simplr ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u≠∅→u∈w∈WordD|w:dom⁡w⟶1-1D
39 id ⊢w=u→w=u
40 dmeq ⊢w=u→dom⁡w=dom⁡u
41 eqidd ⊢w=u→D=D
42 39 40 41 f1eq123d ⊢w=u→w:dom⁡w⟶1-1D↔u:dom⁡u⟶1-1D
43 42 elrab ⊢u∈w∈WordD|w:dom⁡w⟶1-1D↔u∈WordD∧u:dom⁡u⟶1-1D
44 38 43 sylib ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u≠∅→u∈WordD∧u:dom⁡u⟶1-1D
45 44 simpld ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u≠∅→u∈WordD
46 44 simprd ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u≠∅→u:dom⁡u⟶1-1D
47 1 37 45 46 2 cycpmcl ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u≠∅→C⁡u∈BaseS
48 47 3 eleqtrrdi ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u≠∅→C⁡u∈B
49 36 48 eqeltrrd ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D∧u≠∅→I↾D∖ran⁡u∪ucyclShift1∘u-1∈B
50 25 49 pm2.61dane ⊢D∈V∧u∈w∈WordD|w:dom⁡w⟶1-1D→I↾D∖ran⁡u∪ucyclShift1∘u-1∈B
51 4 50 fmpt3d ⊢D∈V→C:w∈WordD|w:dom⁡w⟶1-1D⟶B