Metamath Proof Explorer

Theorem tocycval

Description: Value of the cycle builder. (Contributed by Thierry Arnoux, 22-Sep-2023)

Ref Expression
Hypothesis tocycval.1 ⊢ C = toCyc ⁡ D
Assertion tocycval ⊢ D ∈ V → C = w ∈ u ∈ Word D | u : dom ⁡ u ⟶ 1-1 D ⟼ I ↾ D ∖ ran ⁡ w ∪ w cyclShift 1 ∘ w -1

Proof

Step Hyp Ref Expression
1 tocycval.1 ⊢ C = toCyc ⁡ D
2 df-tocyc ⊢ toCyc = d ∈ V ⟼ w ∈ u ∈ Word d | u : dom ⁡ u ⟶ 1-1 d ⟼ I ↾ d ∖ ran ⁡ w ∪ w cyclShift 1 ∘ w -1
3 wrdeq ⊢ d = D → Word d = Word D
4 f1eq3 ⊢ d = D → u : dom ⁡ u ⟶ 1-1 d ↔ u : dom ⁡ u ⟶ 1-1 D
5 3 4 rabeqbidv ⊢ d = D → u ∈ Word d | u : dom ⁡ u ⟶ 1-1 d = u ∈ Word D | u : dom ⁡ u ⟶ 1-1 D
6 difeq1 ⊢ d = D → d ∖ ran ⁡ w = D ∖ ran ⁡ w
7 6 reseq2d ⊢ d = D → I ↾ d ∖ ran ⁡ w = I ↾ D ∖ ran ⁡ w
8 7 uneq1d ⊢ d = D → I ↾ d ∖ ran ⁡ w ∪ w cyclShift 1 ∘ w -1 = I ↾ D ∖ ran ⁡ w ∪ w cyclShift 1 ∘ w -1
9 5 8 mpteq12dv ⊢ d = D → w ∈ u ∈ Word d | u : dom ⁡ u ⟶ 1-1 d ⟼ I ↾ d ∖ ran ⁡ w ∪ w cyclShift 1 ∘ w -1 = w ∈ u ∈ Word D | u : dom ⁡ u ⟶ 1-1 D ⟼ I ↾ D ∖ ran ⁡ w ∪ w cyclShift 1 ∘ w -1
10 elex ⊢ D ∈ V → D ∈ V
11 eqid ⊢ u ∈ Word D | u : dom ⁡ u ⟶ 1-1 D = u ∈ Word D | u : dom ⁡ u ⟶ 1-1 D
12 wrdexg ⊢ D ∈ V → Word D ∈ V
13 11 12 rabexd ⊢ D ∈ V → u ∈ Word D | u : dom ⁡ u ⟶ 1-1 D ∈ V
14 13 mptexd ⊢ D ∈ V → w ∈ u ∈ Word D | u : dom ⁡ u ⟶ 1-1 D ⟼ I ↾ D ∖ ran ⁡ w ∪ w cyclShift 1 ∘ w -1 ∈ V
15 2 9 10 14 fvmptd3 ⊢ D ∈ V → toCyc ⁡ D = w ∈ u ∈ Word D | u : dom ⁡ u ⟶ 1-1 D ⟼ I ↾ D ∖ ran ⁡ w ∪ w cyclShift 1 ∘ w -1
16 1 15 eqtrid ⊢ D ∈ V → C = w ∈ u ∈ Word D | u : dom ⁡ u ⟶ 1-1 D ⟼ I ↾ D ∖ ran ⁡ w ∪ w cyclShift 1 ∘ w -1