Proof of Theorem cycpmfv2
| Step | Hyp | Ref
| Expression |
| 1 | | tocycval.1 |
. . 3
⊢ 𝐶 = (toCyc‘𝐷) |
| 2 | | tocycfv.d |
. . 3
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
| 3 | | tocycfv.w |
. . 3
⊢ (𝜑 → 𝑊 ∈ Word 𝐷) |
| 4 | | tocycfv.1 |
. . 3
⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷) |
| 5 | | cycpmfv2.2 |
. . . 4
⊢ (𝜑 → 𝑁 = ((♯‘𝑊) − 1)) |
| 6 | | lencl 14571 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝐷 → (♯‘𝑊) ∈
ℕ0) |
| 7 | 3, 6 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝑊) ∈
ℕ0) |
| 8 | | cycpmfv2.1 |
. . . . . . 7
⊢ (𝜑 → 0 <
(♯‘𝑊)) |
| 9 | | elnnnn0b 12570 |
. . . . . . 7
⊢
((♯‘𝑊)
∈ ℕ ↔ ((♯‘𝑊) ∈ ℕ0 ∧ 0 <
(♯‘𝑊))) |
| 10 | 7, 8, 9 | sylanbrc 583 |
. . . . . 6
⊢ (𝜑 → (♯‘𝑊) ∈
ℕ) |
| 11 | | elfz1end 13594 |
. . . . . 6
⊢
((♯‘𝑊)
∈ ℕ ↔ (♯‘𝑊) ∈ (1...(♯‘𝑊))) |
| 12 | 10, 11 | sylib 218 |
. . . . 5
⊢ (𝜑 → (♯‘𝑊) ∈
(1...(♯‘𝑊))) |
| 13 | | fz1fzo0m1 13750 |
. . . . 5
⊢
((♯‘𝑊)
∈ (1...(♯‘𝑊)) → ((♯‘𝑊) − 1) ∈
(0..^(♯‘𝑊))) |
| 14 | 12, 13 | syl 17 |
. . . 4
⊢ (𝜑 → ((♯‘𝑊) − 1) ∈
(0..^(♯‘𝑊))) |
| 15 | 5, 14 | eqeltrd 2841 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝑊))) |
| 16 | 1, 2, 3, 4, 15 | cycpmfvlem 33132 |
. 2
⊢ (𝜑 → ((𝐶‘𝑊)‘(𝑊‘𝑁)) = (((𝑊 cyclShift 1) ∘ ◡𝑊)‘(𝑊‘𝑁))) |
| 17 | | df-f1 6566 |
. . . . 5
⊢ (𝑊:dom 𝑊–1-1→𝐷 ↔ (𝑊:dom 𝑊⟶𝐷 ∧ Fun ◡𝑊)) |
| 18 | 4, 17 | sylib 218 |
. . . 4
⊢ (𝜑 → (𝑊:dom 𝑊⟶𝐷 ∧ Fun ◡𝑊)) |
| 19 | 18 | simprd 495 |
. . 3
⊢ (𝜑 → Fun ◡𝑊) |
| 20 | | wrdfn 14566 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐷 → 𝑊 Fn (0..^(♯‘𝑊))) |
| 21 | 3, 20 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑊 Fn (0..^(♯‘𝑊))) |
| 22 | | fnfvelrn 7100 |
. . . . 5
⊢ ((𝑊 Fn (0..^(♯‘𝑊)) ∧ 𝑁 ∈ (0..^(♯‘𝑊))) → (𝑊‘𝑁) ∈ ran 𝑊) |
| 23 | 21, 15, 22 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝑊‘𝑁) ∈ ran 𝑊) |
| 24 | | df-rn 5696 |
. . . 4
⊢ ran 𝑊 = dom ◡𝑊 |
| 25 | 23, 24 | eleqtrdi 2851 |
. . 3
⊢ (𝜑 → (𝑊‘𝑁) ∈ dom ◡𝑊) |
| 26 | | fvco 7007 |
. . 3
⊢ ((Fun
◡𝑊 ∧ (𝑊‘𝑁) ∈ dom ◡𝑊) → (((𝑊 cyclShift 1) ∘ ◡𝑊)‘(𝑊‘𝑁)) = ((𝑊 cyclShift 1)‘(◡𝑊‘(𝑊‘𝑁)))) |
| 27 | 19, 25, 26 | syl2anc 584 |
. 2
⊢ (𝜑 → (((𝑊 cyclShift 1) ∘ ◡𝑊)‘(𝑊‘𝑁)) = ((𝑊 cyclShift 1)‘(◡𝑊‘(𝑊‘𝑁)))) |
| 28 | | f1f1orn 6859 |
. . . . . 6
⊢ (𝑊:dom 𝑊–1-1→𝐷 → 𝑊:dom 𝑊–1-1-onto→ran
𝑊) |
| 29 | 4, 28 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑊:dom 𝑊–1-1-onto→ran
𝑊) |
| 30 | 21 | fndmd 6673 |
. . . . . 6
⊢ (𝜑 → dom 𝑊 = (0..^(♯‘𝑊))) |
| 31 | 15, 30 | eleqtrrd 2844 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ dom 𝑊) |
| 32 | | f1ocnvfv1 7296 |
. . . . 5
⊢ ((𝑊:dom 𝑊–1-1-onto→ran
𝑊 ∧ 𝑁 ∈ dom 𝑊) → (◡𝑊‘(𝑊‘𝑁)) = 𝑁) |
| 33 | 29, 31, 32 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (◡𝑊‘(𝑊‘𝑁)) = 𝑁) |
| 34 | 33 | fveq2d 6910 |
. . 3
⊢ (𝜑 → ((𝑊 cyclShift 1)‘(◡𝑊‘(𝑊‘𝑁))) = ((𝑊 cyclShift 1)‘𝑁)) |
| 35 | | 1zzd 12648 |
. . . 4
⊢ (𝜑 → 1 ∈
ℤ) |
| 36 | | cshwidxmod 14841 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐷 ∧ 1 ∈ ℤ ∧ 𝑁 ∈
(0..^(♯‘𝑊)))
→ ((𝑊 cyclShift
1)‘𝑁) = (𝑊‘((𝑁 + 1) mod (♯‘𝑊)))) |
| 37 | 3, 35, 15, 36 | syl3anc 1373 |
. . 3
⊢ (𝜑 → ((𝑊 cyclShift 1)‘𝑁) = (𝑊‘((𝑁 + 1) mod (♯‘𝑊)))) |
| 38 | | fzossfz 13718 |
. . . . . . . 8
⊢
(0..^(♯‘𝑊)) ⊆ (0...(♯‘𝑊)) |
| 39 | | fzssz 13566 |
. . . . . . . 8
⊢
(0...(♯‘𝑊)) ⊆ ℤ |
| 40 | 38, 39 | sstri 3993 |
. . . . . . 7
⊢
(0..^(♯‘𝑊)) ⊆ ℤ |
| 41 | 40, 15 | sselid 3981 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 42 | 41 | zred 12722 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 43 | 10 | nnrpd 13075 |
. . . . 5
⊢ (𝜑 → (♯‘𝑊) ∈
ℝ+) |
| 44 | 5 | oveq1d 7446 |
. . . . . 6
⊢ (𝜑 → (𝑁 mod (♯‘𝑊)) = (((♯‘𝑊) − 1) mod (♯‘𝑊))) |
| 45 | | zmodidfzoimp 13941 |
. . . . . . 7
⊢
(((♯‘𝑊)
− 1) ∈ (0..^(♯‘𝑊)) → (((♯‘𝑊) − 1) mod (♯‘𝑊)) = ((♯‘𝑊) − 1)) |
| 46 | 14, 45 | syl 17 |
. . . . . 6
⊢ (𝜑 → (((♯‘𝑊) − 1) mod
(♯‘𝑊)) =
((♯‘𝑊) −
1)) |
| 47 | 44, 46 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → (𝑁 mod (♯‘𝑊)) = ((♯‘𝑊) − 1)) |
| 48 | | modm1p1mod0 13963 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧
(♯‘𝑊) ∈
ℝ+) → ((𝑁 mod (♯‘𝑊)) = ((♯‘𝑊) − 1) → ((𝑁 + 1) mod (♯‘𝑊)) = 0)) |
| 49 | 48 | imp 406 |
. . . . 5
⊢ (((𝑁 ∈ ℝ ∧
(♯‘𝑊) ∈
ℝ+) ∧ (𝑁 mod (♯‘𝑊)) = ((♯‘𝑊) − 1)) → ((𝑁 + 1) mod (♯‘𝑊)) = 0) |
| 50 | 42, 43, 47, 49 | syl21anc 838 |
. . . 4
⊢ (𝜑 → ((𝑁 + 1) mod (♯‘𝑊)) = 0) |
| 51 | 50 | fveq2d 6910 |
. . 3
⊢ (𝜑 → (𝑊‘((𝑁 + 1) mod (♯‘𝑊))) = (𝑊‘0)) |
| 52 | 34, 37, 51 | 3eqtrd 2781 |
. 2
⊢ (𝜑 → ((𝑊 cyclShift 1)‘(◡𝑊‘(𝑊‘𝑁))) = (𝑊‘0)) |
| 53 | 16, 27, 52 | 3eqtrd 2781 |
1
⊢ (𝜑 → ((𝐶‘𝑊)‘(𝑊‘𝑁)) = (𝑊‘0)) |