Proof of Theorem cycpmconjslem1
| Step | Hyp | Ref
| Expression |
| 1 | | resco 6270 |
. . . . 5
⊢ ((◡𝑊 ∘ (𝑀‘𝑊)) ↾ ran 𝑊) = (◡𝑊 ∘ ((𝑀‘𝑊) ↾ ran 𝑊)) |
| 2 | 1 | coeq1i 5870 |
. . . 4
⊢ (((◡𝑊 ∘ (𝑀‘𝑊)) ↾ ran 𝑊) ∘ 𝑊) = ((◡𝑊 ∘ ((𝑀‘𝑊) ↾ ran 𝑊)) ∘ 𝑊) |
| 3 | | ssid 4006 |
. . . . 5
⊢ ran 𝑊 ⊆ ran 𝑊 |
| 4 | | cores 6269 |
. . . . 5
⊢ (ran
𝑊 ⊆ ran 𝑊 → (((◡𝑊 ∘ (𝑀‘𝑊)) ↾ ran 𝑊) ∘ 𝑊) = ((◡𝑊 ∘ (𝑀‘𝑊)) ∘ 𝑊)) |
| 5 | 3, 4 | ax-mp 5 |
. . . 4
⊢ (((◡𝑊 ∘ (𝑀‘𝑊)) ↾ ran 𝑊) ∘ 𝑊) = ((◡𝑊 ∘ (𝑀‘𝑊)) ∘ 𝑊) |
| 6 | | coass 6285 |
. . . 4
⊢ ((◡𝑊 ∘ ((𝑀‘𝑊) ↾ ran 𝑊)) ∘ 𝑊) = (◡𝑊 ∘ (((𝑀‘𝑊) ↾ ran 𝑊) ∘ 𝑊)) |
| 7 | 2, 5, 6 | 3eqtr3i 2773 |
. . 3
⊢ ((◡𝑊 ∘ (𝑀‘𝑊)) ∘ 𝑊) = (◡𝑊 ∘ (((𝑀‘𝑊) ↾ ran 𝑊) ∘ 𝑊)) |
| 8 | | cycpmconjs.m |
. . . . . . 7
⊢ 𝑀 = (toCyc‘𝐷) |
| 9 | | cycpmconjslem1.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
| 10 | | cycpmconjslem1.w |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ Word 𝐷) |
| 11 | | cycpmconjslem1.1 |
. . . . . . 7
⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷) |
| 12 | 8, 9, 10, 11 | tocycfvres1 33130 |
. . . . . 6
⊢ (𝜑 → ((𝑀‘𝑊) ↾ ran 𝑊) = ((𝑊 cyclShift 1) ∘ ◡𝑊)) |
| 13 | 12 | coeq1d 5872 |
. . . . 5
⊢ (𝜑 → (((𝑀‘𝑊) ↾ ran 𝑊) ∘ 𝑊) = (((𝑊 cyclShift 1) ∘ ◡𝑊) ∘ 𝑊)) |
| 14 | | coass 6285 |
. . . . . 6
⊢ (((𝑊 cyclShift 1) ∘ ◡𝑊) ∘ 𝑊) = ((𝑊 cyclShift 1) ∘ (◡𝑊 ∘ 𝑊)) |
| 15 | | f1f1orn 6859 |
. . . . . . . . 9
⊢ (𝑊:dom 𝑊–1-1→𝐷 → 𝑊:dom 𝑊–1-1-onto→ran
𝑊) |
| 16 | | f1ococnv1 6877 |
. . . . . . . . 9
⊢ (𝑊:dom 𝑊–1-1-onto→ran
𝑊 → (◡𝑊 ∘ 𝑊) = ( I ↾ dom 𝑊)) |
| 17 | 11, 15, 16 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (◡𝑊 ∘ 𝑊) = ( I ↾ dom 𝑊)) |
| 18 | 17 | coeq2d 5873 |
. . . . . . 7
⊢ (𝜑 → ((𝑊 cyclShift 1) ∘ (◡𝑊 ∘ 𝑊)) = ((𝑊 cyclShift 1) ∘ ( I ↾ dom 𝑊))) |
| 19 | | coires1 6284 |
. . . . . . 7
⊢ ((𝑊 cyclShift 1) ∘ ( I
↾ dom 𝑊)) = ((𝑊 cyclShift 1) ↾ dom 𝑊) |
| 20 | 18, 19 | eqtr2di 2794 |
. . . . . 6
⊢ (𝜑 → ((𝑊 cyclShift 1) ↾ dom 𝑊) = ((𝑊 cyclShift 1) ∘ (◡𝑊 ∘ 𝑊))) |
| 21 | 14, 20 | eqtr4id 2796 |
. . . . 5
⊢ (𝜑 → (((𝑊 cyclShift 1) ∘ ◡𝑊) ∘ 𝑊) = ((𝑊 cyclShift 1) ↾ dom 𝑊)) |
| 22 | | 1zzd 12648 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℤ) |
| 23 | | cshwfn 14839 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐷 ∧ 1 ∈ ℤ) → (𝑊 cyclShift 1) Fn
(0..^(♯‘𝑊))) |
| 24 | 10, 22, 23 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝑊 cyclShift 1) Fn (0..^(♯‘𝑊))) |
| 25 | | wrddm 14559 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝐷 → dom 𝑊 = (0..^(♯‘𝑊))) |
| 26 | 10, 25 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → dom 𝑊 = (0..^(♯‘𝑊))) |
| 27 | 26 | fneq2d 6662 |
. . . . . . 7
⊢ (𝜑 → ((𝑊 cyclShift 1) Fn dom 𝑊 ↔ (𝑊 cyclShift 1) Fn (0..^(♯‘𝑊)))) |
| 28 | 24, 27 | mpbird 257 |
. . . . . 6
⊢ (𝜑 → (𝑊 cyclShift 1) Fn dom 𝑊) |
| 29 | | fnresdm 6687 |
. . . . . 6
⊢ ((𝑊 cyclShift 1) Fn dom 𝑊 → ((𝑊 cyclShift 1) ↾ dom 𝑊) = (𝑊 cyclShift 1)) |
| 30 | 28, 29 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝑊 cyclShift 1) ↾ dom 𝑊) = (𝑊 cyclShift 1)) |
| 31 | 13, 21, 30 | 3eqtrd 2781 |
. . . 4
⊢ (𝜑 → (((𝑀‘𝑊) ↾ ran 𝑊) ∘ 𝑊) = (𝑊 cyclShift 1)) |
| 32 | 31 | coeq2d 5873 |
. . 3
⊢ (𝜑 → (◡𝑊 ∘ (((𝑀‘𝑊) ↾ ran 𝑊) ∘ 𝑊)) = (◡𝑊 ∘ (𝑊 cyclShift 1))) |
| 33 | 7, 32 | eqtrid 2789 |
. 2
⊢ (𝜑 → ((◡𝑊 ∘ (𝑀‘𝑊)) ∘ 𝑊) = (◡𝑊 ∘ (𝑊 cyclShift 1))) |
| 34 | | wrdfn 14566 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐷 → 𝑊 Fn (0..^(♯‘𝑊))) |
| 35 | 10, 34 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑊 Fn (0..^(♯‘𝑊))) |
| 36 | | df-f 6565 |
. . . . 5
⊢ (𝑊:(0..^(♯‘𝑊))⟶ran 𝑊 ↔ (𝑊 Fn (0..^(♯‘𝑊)) ∧ ran 𝑊 ⊆ ran 𝑊)) |
| 37 | 35, 3, 36 | sylanblrc 590 |
. . . 4
⊢ (𝜑 → 𝑊:(0..^(♯‘𝑊))⟶ran 𝑊) |
| 38 | | iswrdi 14556 |
. . . 4
⊢ (𝑊:(0..^(♯‘𝑊))⟶ran 𝑊 → 𝑊 ∈ Word ran 𝑊) |
| 39 | 37, 38 | syl 17 |
. . 3
⊢ (𝜑 → 𝑊 ∈ Word ran 𝑊) |
| 40 | | f1ocnv 6860 |
. . . 4
⊢ (𝑊:dom 𝑊–1-1-onto→ran
𝑊 → ◡𝑊:ran 𝑊–1-1-onto→dom
𝑊) |
| 41 | | f1of 6848 |
. . . 4
⊢ (◡𝑊:ran 𝑊–1-1-onto→dom
𝑊 → ◡𝑊:ran 𝑊⟶dom 𝑊) |
| 42 | 11, 15, 40, 41 | 4syl 19 |
. . 3
⊢ (𝜑 → ◡𝑊:ran 𝑊⟶dom 𝑊) |
| 43 | | cshco 14875 |
. . 3
⊢ ((𝑊 ∈ Word ran 𝑊 ∧ 1 ∈ ℤ ∧
◡𝑊:ran 𝑊⟶dom 𝑊) → (◡𝑊 ∘ (𝑊 cyclShift 1)) = ((◡𝑊 ∘ 𝑊) cyclShift 1)) |
| 44 | 39, 22, 42, 43 | syl3anc 1373 |
. 2
⊢ (𝜑 → (◡𝑊 ∘ (𝑊 cyclShift 1)) = ((◡𝑊 ∘ 𝑊) cyclShift 1)) |
| 45 | | cycpmconjslem1.2 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝑊) = 𝑃) |
| 46 | 45 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → (0..^(♯‘𝑊)) = (0..^𝑃)) |
| 47 | 26, 46 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → dom 𝑊 = (0..^𝑃)) |
| 48 | 47 | reseq2d 5997 |
. . . 4
⊢ (𝜑 → ( I ↾ dom 𝑊) = ( I ↾ (0..^𝑃))) |
| 49 | 17, 48 | eqtrd 2777 |
. . 3
⊢ (𝜑 → (◡𝑊 ∘ 𝑊) = ( I ↾ (0..^𝑃))) |
| 50 | 49 | oveq1d 7446 |
. 2
⊢ (𝜑 → ((◡𝑊 ∘ 𝑊) cyclShift 1) = (( I ↾ (0..^𝑃)) cyclShift
1)) |
| 51 | 33, 44, 50 | 3eqtrd 2781 |
1
⊢ (𝜑 → ((◡𝑊 ∘ (𝑀‘𝑊)) ∘ 𝑊) = (( I ↾ (0..^𝑃)) cyclShift 1)) |