Metamath Proof Explorer

Theorem cycpmfv3

Description: Values outside of the orbit are unchanged by a cycle. (Contributed by Thierry Arnoux, 22-Sep-2023)

Ref Expression
Hypotheses tocycval.1 ⊢ 𝐶 = ( toCyc ‘ 𝐷 )
tocycfv.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
tocycfv.w ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
tocycfv.1 ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
cycpmfv3.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
cycpmfv3.2 ⊢ ( 𝜑 → ¬ 𝑋 ∈ ran 𝑊 )
Assertion cycpmfv3 ( 𝜑 → ( ( 𝐶 ‘ 𝑊 ) ‘ 𝑋 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 tocycval.1 ⊢ 𝐶 = ( toCyc ‘ 𝐷 )
2 tocycfv.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
3 tocycfv.w ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
4 tocycfv.1 ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
5 cycpmfv3.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
6 cycpmfv3.2 ⊢ ( 𝜑 → ¬ 𝑋 ∈ ran 𝑊 )
7 1 2 3 4 tocycfv ⊢ ( 𝜑 → ( 𝐶 ‘ 𝑊 ) = ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) )
8 7 fveq1d ⊢ ( 𝜑 → ( ( 𝐶 ‘ 𝑊 ) ‘ 𝑋 ) = ( ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) ‘ 𝑋 ) )
9 f1oi ⊢ ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) : ( 𝐷 ∖ ran 𝑊 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑊 )
10 f1ofn ⊢ ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) : ( 𝐷 ∖ ran 𝑊 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑊 ) → ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) Fn ( 𝐷 ∖ ran 𝑊 ) )
11 9 10 mp1i ⊢ ( 𝜑 → ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) Fn ( 𝐷 ∖ ran 𝑊 ) )
12 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
13 cshwf ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 1 ∈ ℤ ) → ( 𝑊 cyclShift 1 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐷 )
14 3 12 13 syl2anc ⊢ ( 𝜑 → ( 𝑊 cyclShift 1 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐷 )
15 14 ffnd ⊢ ( 𝜑 → ( 𝑊 cyclShift 1 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
16 df-f1 ⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 ↔ ( 𝑊 : dom 𝑊 ⟶ 𝐷 ∧ Fun ◡ 𝑊 ) )
17 4 16 sylib ⊢ ( 𝜑 → ( 𝑊 : dom 𝑊 ⟶ 𝐷 ∧ Fun ◡ 𝑊 ) )
18 17 simprd ⊢ ( 𝜑 → Fun ◡ 𝑊 )
19 18 funfnd ⊢ ( 𝜑 → ◡ 𝑊 Fn dom ◡ 𝑊 )
20 df-rn ⊢ ran 𝑊 = dom ◡ 𝑊
21 20 fneq2i ⊢ ( ◡ 𝑊 Fn ran 𝑊 ↔ ◡ 𝑊 Fn dom ◡ 𝑊 )
22 19 21 sylibr ⊢ ( 𝜑 → ◡ 𝑊 Fn ran 𝑊 )
23 dfdm4 ⊢ dom 𝑊 = ran ◡ 𝑊
24 23 eqimss2i ⊢ ran ◡ 𝑊 ⊆ dom 𝑊
25 wrdfn ⊢ ( 𝑊 ∈ Word 𝐷 → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
26 3 25 syl ⊢ ( 𝜑 → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
27 26 fndmd ⊢ ( 𝜑 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
28 24 27 sseqtrid ⊢ ( 𝜑 → ran ◡ 𝑊 ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
29 fnco ⊢ ( ( ( 𝑊 cyclShift 1 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ◡ 𝑊 Fn ran 𝑊 ∧ ran ◡ 𝑊 ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) Fn ran 𝑊 )
30 15 22 28 29 syl3anc ⊢ ( 𝜑 → ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) Fn ran 𝑊 )
31 disjdifr ⊢ ( ( 𝐷 ∖ ran 𝑊 ) ∩ ran 𝑊 ) = ∅
32 31 a1i ⊢ ( 𝜑 → ( ( 𝐷 ∖ ran 𝑊 ) ∩ ran 𝑊 ) = ∅ )
33 5 6 eldifd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐷 ∖ ran 𝑊 ) )
34 fvun1 ⊢ ( ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) Fn ( 𝐷 ∖ ran 𝑊 ) ∧ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) Fn ran 𝑊 ∧ ( ( ( 𝐷 ∖ ran 𝑊 ) ∩ ran 𝑊 ) = ∅ ∧ 𝑋 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ) → ( ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) ‘ 𝑋 ) = ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ‘ 𝑋 ) )
35 11 30 32 33 34 syl112anc ⊢ ( 𝜑 → ( ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) ‘ 𝑋 ) = ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ‘ 𝑋 ) )
36 fvresi ⊢ ( 𝑋 ∈ ( 𝐷 ∖ ran 𝑊 ) → ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ‘ 𝑋 ) = 𝑋 )
37 33 36 syl ⊢ ( 𝜑 → ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ‘ 𝑋 ) = 𝑋 )
38 8 35 37 3eqtrd ⊢ ( 𝜑 → ( ( 𝐶 ‘ 𝑊 ) ‘ 𝑋 ) = 𝑋 )