Metamath Proof Explorer


Theorem tocycval

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

Ref Expression
Hypothesis tocycval.1 𝐶 = ( toCyc ‘ 𝐷 )
Assertion tocycval ( 𝐷𝑉𝐶 = ( 𝑤 ∈ { 𝑢 ∈ Word 𝐷𝑢 : dom 𝑢1-1𝐷 } ↦ ( ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ 𝑤 ) ) ) )

Proof

Step Hyp Ref Expression
1 tocycval.1 𝐶 = ( toCyc ‘ 𝐷 )
2 df-tocyc toCyc = ( 𝑑 ∈ V ↦ ( 𝑤 ∈ { 𝑢 ∈ Word 𝑑𝑢 : dom 𝑢1-1𝑑 } ↦ ( ( I ↾ ( 𝑑 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ 𝑤 ) ) ) )
3 wrdeq ( 𝑑 = 𝐷 → Word 𝑑 = Word 𝐷 )
4 f1eq3 ( 𝑑 = 𝐷 → ( 𝑢 : dom 𝑢1-1𝑑𝑢 : dom 𝑢1-1𝐷 ) )
5 3 4 rabeqbidv ( 𝑑 = 𝐷 → { 𝑢 ∈ Word 𝑑𝑢 : dom 𝑢1-1𝑑 } = { 𝑢 ∈ Word 𝐷𝑢 : dom 𝑢1-1𝐷 } )
6 difeq1 ( 𝑑 = 𝐷 → ( 𝑑 ∖ ran 𝑤 ) = ( 𝐷 ∖ ran 𝑤 ) )
7 6 reseq2d ( 𝑑 = 𝐷 → ( I ↾ ( 𝑑 ∖ ran 𝑤 ) ) = ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) )
8 7 uneq1d ( 𝑑 = 𝐷 → ( ( I ↾ ( 𝑑 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ 𝑤 ) ) = ( ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ 𝑤 ) ) )
9 5 8 mpteq12dv ( 𝑑 = 𝐷 → ( 𝑤 ∈ { 𝑢 ∈ Word 𝑑𝑢 : dom 𝑢1-1𝑑 } ↦ ( ( I ↾ ( 𝑑 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ 𝑤 ) ) ) = ( 𝑤 ∈ { 𝑢 ∈ Word 𝐷𝑢 : dom 𝑢1-1𝐷 } ↦ ( ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ 𝑤 ) ) ) )
10 elex ( 𝐷𝑉𝐷 ∈ V )
11 eqid { 𝑢 ∈ Word 𝐷𝑢 : dom 𝑢1-1𝐷 } = { 𝑢 ∈ Word 𝐷𝑢 : dom 𝑢1-1𝐷 }
12 wrdexg ( 𝐷𝑉 → Word 𝐷 ∈ V )
13 11 12 rabexd ( 𝐷𝑉 → { 𝑢 ∈ Word 𝐷𝑢 : dom 𝑢1-1𝐷 } ∈ V )
14 13 mptexd ( 𝐷𝑉 → ( 𝑤 ∈ { 𝑢 ∈ Word 𝐷𝑢 : dom 𝑢1-1𝐷 } ↦ ( ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ 𝑤 ) ) ) ∈ V )
15 2 9 10 14 fvmptd3 ( 𝐷𝑉 → ( toCyc ‘ 𝐷 ) = ( 𝑤 ∈ { 𝑢 ∈ Word 𝐷𝑢 : dom 𝑢1-1𝐷 } ↦ ( ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ 𝑤 ) ) ) )
16 1 15 syl5eq ( 𝐷𝑉𝐶 = ( 𝑤 ∈ { 𝑢 ∈ Word 𝐷𝑢 : dom 𝑢1-1𝐷 } ↦ ( ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ 𝑤 ) ) ) )