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 = Base S
Assertion tocycf ⊢ D ∈ V → C : w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D ⟶ B

Proof

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