Metamath Proof Explorer

Theorem cycpmfvlem

Description: Lemma for cycpmfv1 and cycpmfv2 . (Contributed by Thierry Arnoux, 22-Sep-2023)

Ref Expression
Hypotheses tocycval.1 ⊢ 𝐶 = ( toCyc ‘ 𝐷 )
tocycfv.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
tocycfv.w ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
tocycfv.1 ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
cycpmfvlem.1 ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
Assertion cycpmfvlem ( 𝜑 → ( ( 𝐶 ‘ 𝑊 ) ‘ ( 𝑊 ‘ 𝑁 ) ) = ( ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ‘ ( 𝑊 ‘ 𝑁 ) ) )

Proof

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