| Step | Hyp | Ref
| Expression |
| 1 | | cycpmrn.4 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷) |
| 2 | 1 | ad4antr 732 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) → 𝑊:dom 𝑊–1-1→𝐷) |
| 3 | | simpllr 776 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) → 𝑥 ∈ dom 𝑊) |
| 4 | | fzo0ss1 13729 |
. . . . . . . . . . . . 13
⊢
(1..^(♯‘𝑊)) ⊆ (0..^(♯‘𝑊)) |
| 5 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) → 𝑥 ∈
(0..^((♯‘𝑊)
− 1))) |
| 6 | | cycpmrn.3 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑊 ∈ Word 𝐷) |
| 7 | | lencl 14571 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ Word 𝐷 → (♯‘𝑊) ∈
ℕ0) |
| 8 | 6, 7 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (♯‘𝑊) ∈
ℕ0) |
| 9 | 8 | ad4antr 732 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) →
(♯‘𝑊) ∈
ℕ0) |
| 10 | 9 | nn0zd 12639 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) →
(♯‘𝑊) ∈
ℤ) |
| 11 | | 1zzd 12648 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) → 1 ∈
ℤ) |
| 12 | | fzoaddel2 13759 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈
(0..^((♯‘𝑊)
− 1)) ∧ (♯‘𝑊) ∈ ℤ ∧ 1 ∈ ℤ)
→ (𝑥 + 1) ∈
(1..^(♯‘𝑊))) |
| 13 | 5, 10, 11, 12 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) → (𝑥 + 1) ∈
(1..^(♯‘𝑊))) |
| 14 | 4, 13 | sselid 3981 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) → (𝑥 + 1) ∈
(0..^(♯‘𝑊))) |
| 15 | 6 | ad4antr 732 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) → 𝑊 ∈ Word 𝐷) |
| 16 | | wrddm 14559 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ Word 𝐷 → dom 𝑊 = (0..^(♯‘𝑊))) |
| 17 | 15, 16 | syl 17 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) → dom 𝑊 = (0..^(♯‘𝑊))) |
| 18 | 14, 17 | eleqtrrd 2844 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) → (𝑥 + 1) ∈ dom 𝑊) |
| 19 | | fzossz 13719 |
. . . . . . . . . . . . . 14
⊢
(0..^((♯‘𝑊) − 1)) ⊆
ℤ |
| 20 | 19, 5 | sselid 3981 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) → 𝑥 ∈
ℤ) |
| 21 | 20 | zred 12722 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) → 𝑥 ∈
ℝ) |
| 22 | 21 | ltp1d 12198 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) → 𝑥 < (𝑥 + 1)) |
| 23 | 21, 22 | ltned 11397 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) → 𝑥 ≠ (𝑥 + 1)) |
| 24 | | f1veqaeq 7277 |
. . . . . . . . . . . . . 14
⊢ ((𝑊:dom 𝑊–1-1→𝐷 ∧ (𝑥 ∈ dom 𝑊 ∧ (𝑥 + 1) ∈ dom 𝑊)) → ((𝑊‘𝑥) = (𝑊‘(𝑥 + 1)) → 𝑥 = (𝑥 + 1))) |
| 25 | 24 | necon3d 2961 |
. . . . . . . . . . . . 13
⊢ ((𝑊:dom 𝑊–1-1→𝐷 ∧ (𝑥 ∈ dom 𝑊 ∧ (𝑥 + 1) ∈ dom 𝑊)) → (𝑥 ≠ (𝑥 + 1) → (𝑊‘𝑥) ≠ (𝑊‘(𝑥 + 1)))) |
| 26 | 25 | anassrs 467 |
. . . . . . . . . . . 12
⊢ (((𝑊:dom 𝑊–1-1→𝐷 ∧ 𝑥 ∈ dom 𝑊) ∧ (𝑥 + 1) ∈ dom 𝑊) → (𝑥 ≠ (𝑥 + 1) → (𝑊‘𝑥) ≠ (𝑊‘(𝑥 + 1)))) |
| 27 | 26 | imp 406 |
. . . . . . . . . . 11
⊢ ((((𝑊:dom 𝑊–1-1→𝐷 ∧ 𝑥 ∈ dom 𝑊) ∧ (𝑥 + 1) ∈ dom 𝑊) ∧ 𝑥 ≠ (𝑥 + 1)) → (𝑊‘𝑥) ≠ (𝑊‘(𝑥 + 1))) |
| 28 | 2, 3, 18, 23, 27 | syl1111anc 841 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) → (𝑊‘𝑥) ≠ (𝑊‘(𝑥 + 1))) |
| 29 | | cycpmrn.1 |
. . . . . . . . . . 11
⊢ 𝑀 = (toCyc‘𝐷) |
| 30 | | cycpmrn.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
| 31 | 30 | ad4antr 732 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) → 𝐷 ∈ 𝑉) |
| 32 | 29, 31, 15, 2, 5 | cycpmfv1 33133 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) → ((𝑀‘𝑊)‘(𝑊‘𝑥)) = (𝑊‘(𝑥 + 1))) |
| 33 | 28, 32 | neeqtrrd 3015 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) → (𝑊‘𝑥) ≠ ((𝑀‘𝑊)‘(𝑊‘𝑥))) |
| 34 | 33 | necomd 2996 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) → ((𝑀‘𝑊)‘(𝑊‘𝑥)) ≠ (𝑊‘𝑥)) |
| 35 | | simplr 769 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) → 𝑦 = (𝑊‘𝑥)) |
| 36 | 35 | fveq2d 6910 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) → ((𝑀‘𝑊)‘𝑦) = ((𝑀‘𝑊)‘(𝑊‘𝑥))) |
| 37 | 34, 36, 35 | 3netr4d 3018 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − 1))) → ((𝑀‘𝑊)‘𝑦) ≠ 𝑦) |
| 38 | 1 | ad4antr 732 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 = ((♯‘𝑊) − 1)) → 𝑊:dom 𝑊–1-1→𝐷) |
| 39 | 6 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) → 𝑊 ∈ Word 𝐷) |
| 40 | | eldmne0 32638 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ dom 𝑊 → 𝑊 ≠ ∅) |
| 41 | 40 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) → 𝑊 ≠ ∅) |
| 42 | | lennncl 14572 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈
ℕ) |
| 43 | 39, 41, 42 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) → (♯‘𝑊) ∈ ℕ) |
| 44 | | lbfzo0 13739 |
. . . . . . . . . . . 12
⊢ (0 ∈
(0..^(♯‘𝑊))
↔ (♯‘𝑊)
∈ ℕ) |
| 45 | 43, 44 | sylibr 234 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) → 0 ∈ (0..^(♯‘𝑊))) |
| 46 | 39, 16 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) → dom 𝑊 = (0..^(♯‘𝑊))) |
| 47 | 45, 46 | eleqtrrd 2844 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) → 0 ∈ dom 𝑊) |
| 48 | 47 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 = ((♯‘𝑊) − 1)) → 0 ∈ dom 𝑊) |
| 49 | | simpllr 776 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 = ((♯‘𝑊) − 1)) → 𝑥 ∈ dom 𝑊) |
| 50 | | 0red 11264 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈
ℝ) |
| 51 | | cycpmrn.5 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 <
(♯‘𝑊)) |
| 52 | | 1red 11262 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈
ℝ) |
| 53 | 8 | nn0red 12588 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (♯‘𝑊) ∈
ℝ) |
| 54 | 52, 53 | posdifd 11850 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 <
(♯‘𝑊) ↔ 0
< ((♯‘𝑊)
− 1))) |
| 55 | 51, 54 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 <
((♯‘𝑊) −
1)) |
| 56 | 50, 55 | ltned 11397 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≠
((♯‘𝑊) −
1)) |
| 57 | 56 | ad4antr 732 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 = ((♯‘𝑊) − 1)) → 0 ≠
((♯‘𝑊) −
1)) |
| 58 | | simpr 484 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 = ((♯‘𝑊) − 1)) → 𝑥 = ((♯‘𝑊) − 1)) |
| 59 | 57, 58 | neeqtrrd 3015 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 = ((♯‘𝑊) − 1)) → 0 ≠ 𝑥) |
| 60 | | f1veqaeq 7277 |
. . . . . . . . . . . 12
⊢ ((𝑊:dom 𝑊–1-1→𝐷 ∧ (0 ∈ dom 𝑊 ∧ 𝑥 ∈ dom 𝑊)) → ((𝑊‘0) = (𝑊‘𝑥) → 0 = 𝑥)) |
| 61 | 60 | necon3d 2961 |
. . . . . . . . . . 11
⊢ ((𝑊:dom 𝑊–1-1→𝐷 ∧ (0 ∈ dom 𝑊 ∧ 𝑥 ∈ dom 𝑊)) → (0 ≠ 𝑥 → (𝑊‘0) ≠ (𝑊‘𝑥))) |
| 62 | 61 | anassrs 467 |
. . . . . . . . . 10
⊢ (((𝑊:dom 𝑊–1-1→𝐷 ∧ 0 ∈ dom 𝑊) ∧ 𝑥 ∈ dom 𝑊) → (0 ≠ 𝑥 → (𝑊‘0) ≠ (𝑊‘𝑥))) |
| 63 | 62 | imp 406 |
. . . . . . . . 9
⊢ ((((𝑊:dom 𝑊–1-1→𝐷 ∧ 0 ∈ dom 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 0 ≠ 𝑥) → (𝑊‘0) ≠ (𝑊‘𝑥)) |
| 64 | 38, 48, 49, 59, 63 | syl1111anc 841 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 = ((♯‘𝑊) − 1)) → (𝑊‘0) ≠ (𝑊‘𝑥)) |
| 65 | | simplr 769 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 = ((♯‘𝑊) − 1)) → 𝑦 = (𝑊‘𝑥)) |
| 66 | 65 | fveq2d 6910 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 = ((♯‘𝑊) − 1)) → ((𝑀‘𝑊)‘𝑦) = ((𝑀‘𝑊)‘(𝑊‘𝑥))) |
| 67 | 30 | ad4antr 732 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 = ((♯‘𝑊) − 1)) → 𝐷 ∈ 𝑉) |
| 68 | 6 | ad4antr 732 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 = ((♯‘𝑊) − 1)) → 𝑊 ∈ Word 𝐷) |
| 69 | 43 | nngt0d 12315 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) → 0 < (♯‘𝑊)) |
| 70 | 69 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 = ((♯‘𝑊) − 1)) → 0 <
(♯‘𝑊)) |
| 71 | 29, 67, 68, 38, 70, 58 | cycpmfv2 33134 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 = ((♯‘𝑊) − 1)) → ((𝑀‘𝑊)‘(𝑊‘𝑥)) = (𝑊‘0)) |
| 72 | 66, 71 | eqtrd 2777 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 = ((♯‘𝑊) − 1)) → ((𝑀‘𝑊)‘𝑦) = (𝑊‘0)) |
| 73 | 64, 72, 65 | 3netr4d 3018 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) ∧ 𝑥 = ((♯‘𝑊) − 1)) → ((𝑀‘𝑊)‘𝑦) ≠ 𝑦) |
| 74 | | simplr 769 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) → 𝑥 ∈ dom 𝑊) |
| 75 | 74, 46 | eleqtrd 2843 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) → 𝑥 ∈ (0..^(♯‘𝑊))) |
| 76 | | 0z 12624 |
. . . . . . . . . . 11
⊢ 0 ∈
ℤ |
| 77 | | 0p1e1 12388 |
. . . . . . . . . . . . . 14
⊢ (0 + 1) =
1 |
| 78 | 77 | fveq2i 6909 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘(0 + 1)) =
(ℤ≥‘1) |
| 79 | | nnuz 12921 |
. . . . . . . . . . . . 13
⊢ ℕ =
(ℤ≥‘1) |
| 80 | 78, 79 | eqtr4i 2768 |
. . . . . . . . . . . 12
⊢
(ℤ≥‘(0 + 1)) = ℕ |
| 81 | 43, 80 | eleqtrrdi 2852 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) → (♯‘𝑊) ∈ (ℤ≥‘(0 +
1))) |
| 82 | | fzosplitsnm1 13779 |
. . . . . . . . . . 11
⊢ ((0
∈ ℤ ∧ (♯‘𝑊) ∈ (ℤ≥‘(0 +
1))) → (0..^(♯‘𝑊)) = ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1)})) |
| 83 | 76, 81, 82 | sylancr 587 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) → (0..^(♯‘𝑊)) = ((0..^((♯‘𝑊) − 1)) ∪
{((♯‘𝑊) −
1)})) |
| 84 | 75, 83 | eleqtrd 2843 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) → 𝑥 ∈ ((0..^((♯‘𝑊) − 1)) ∪
{((♯‘𝑊) −
1)})) |
| 85 | | elun 4153 |
. . . . . . . . 9
⊢ (𝑥 ∈
((0..^((♯‘𝑊)
− 1)) ∪ {((♯‘𝑊) − 1)}) ↔ (𝑥 ∈ (0..^((♯‘𝑊) − 1)) ∨ 𝑥 ∈ {((♯‘𝑊) − 1)})) |
| 86 | 84, 85 | sylib 218 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) → (𝑥 ∈ (0..^((♯‘𝑊) − 1)) ∨ 𝑥 ∈ {((♯‘𝑊) − 1)})) |
| 87 | | velsn 4642 |
. . . . . . . . 9
⊢ (𝑥 ∈ {((♯‘𝑊) − 1)} ↔ 𝑥 = ((♯‘𝑊) − 1)) |
| 88 | 87 | orbi2i 913 |
. . . . . . . 8
⊢ ((𝑥 ∈
(0..^((♯‘𝑊)
− 1)) ∨ 𝑥 ∈
{((♯‘𝑊) −
1)}) ↔ (𝑥 ∈
(0..^((♯‘𝑊)
− 1)) ∨ 𝑥 =
((♯‘𝑊) −
1))) |
| 89 | 86, 88 | sylib 218 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) → (𝑥 ∈ (0..^((♯‘𝑊) − 1)) ∨ 𝑥 = ((♯‘𝑊) − 1))) |
| 90 | 37, 73, 89 | mpjaodan 961 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ ran 𝑊) ∧ 𝑥 ∈ dom 𝑊) ∧ 𝑦 = (𝑊‘𝑥)) → ((𝑀‘𝑊)‘𝑦) ≠ 𝑦) |
| 91 | | f1fun 6806 |
. . . . . . . 8
⊢ (𝑊:dom 𝑊–1-1→𝐷 → Fun 𝑊) |
| 92 | | elrnrexdmb 7110 |
. . . . . . . 8
⊢ (Fun
𝑊 → (𝑦 ∈ ran 𝑊 ↔ ∃𝑥 ∈ dom 𝑊 𝑦 = (𝑊‘𝑥))) |
| 93 | 1, 91, 92 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ ran 𝑊 ↔ ∃𝑥 ∈ dom 𝑊 𝑦 = (𝑊‘𝑥))) |
| 94 | 93 | biimpa 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑊) → ∃𝑥 ∈ dom 𝑊 𝑦 = (𝑊‘𝑥)) |
| 95 | 90, 94 | r19.29a 3162 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑊) → ((𝑀‘𝑊)‘𝑦) ≠ 𝑦) |
| 96 | | eqid 2737 |
. . . . . . . . . 10
⊢
(SymGrp‘𝐷) =
(SymGrp‘𝐷) |
| 97 | 29, 30, 6, 1, 96 | cycpmcl 33136 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀‘𝑊) ∈ (Base‘(SymGrp‘𝐷))) |
| 98 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘(SymGrp‘𝐷)) = (Base‘(SymGrp‘𝐷)) |
| 99 | 96, 98 | elsymgbas 19391 |
. . . . . . . . . 10
⊢ (𝐷 ∈ 𝑉 → ((𝑀‘𝑊) ∈ (Base‘(SymGrp‘𝐷)) ↔ (𝑀‘𝑊):𝐷–1-1-onto→𝐷)) |
| 100 | 30, 99 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑀‘𝑊) ∈ (Base‘(SymGrp‘𝐷)) ↔ (𝑀‘𝑊):𝐷–1-1-onto→𝐷)) |
| 101 | 97, 100 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → (𝑀‘𝑊):𝐷–1-1-onto→𝐷) |
| 102 | | f1ofn 6849 |
. . . . . . . 8
⊢ ((𝑀‘𝑊):𝐷–1-1-onto→𝐷 → (𝑀‘𝑊) Fn 𝐷) |
| 103 | 101, 102 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑀‘𝑊) Fn 𝐷) |
| 104 | 103 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑊) → (𝑀‘𝑊) Fn 𝐷) |
| 105 | | wrdf 14557 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝐷 → 𝑊:(0..^(♯‘𝑊))⟶𝐷) |
| 106 | | frn 6743 |
. . . . . . . 8
⊢ (𝑊:(0..^(♯‘𝑊))⟶𝐷 → ran 𝑊 ⊆ 𝐷) |
| 107 | 6, 105, 106 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → ran 𝑊 ⊆ 𝐷) |
| 108 | 107 | sselda 3983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑊) → 𝑦 ∈ 𝐷) |
| 109 | | fnelnfp 7197 |
. . . . . 6
⊢ (((𝑀‘𝑊) Fn 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑦 ∈ dom ((𝑀‘𝑊) ∖ I ) ↔ ((𝑀‘𝑊)‘𝑦) ≠ 𝑦)) |
| 110 | 104, 108,
109 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑊) → (𝑦 ∈ dom ((𝑀‘𝑊) ∖ I ) ↔ ((𝑀‘𝑊)‘𝑦) ≠ 𝑦)) |
| 111 | 95, 110 | mpbird 257 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑊) → 𝑦 ∈ dom ((𝑀‘𝑊) ∖ I )) |
| 112 | 111 | ex 412 |
. . 3
⊢ (𝜑 → (𝑦 ∈ ran 𝑊 → 𝑦 ∈ dom ((𝑀‘𝑊) ∖ I ))) |
| 113 | 112 | ssrdv 3989 |
. 2
⊢ (𝜑 → ran 𝑊 ⊆ dom ((𝑀‘𝑊) ∖ I )) |
| 114 | 29, 30, 6, 1 | tocycfv 33129 |
. . . . 5
⊢ (𝜑 → (𝑀‘𝑊) = (( I ↾ (𝐷 ∖ ran 𝑊)) ∪ ((𝑊 cyclShift 1) ∘ ◡𝑊))) |
| 115 | 114 | difeq1d 4125 |
. . . 4
⊢ (𝜑 → ((𝑀‘𝑊) ∖ I ) = ((( I ↾ (𝐷 ∖ ran 𝑊)) ∪ ((𝑊 cyclShift 1) ∘ ◡𝑊)) ∖ I )) |
| 116 | 115 | dmeqd 5916 |
. . 3
⊢ (𝜑 → dom ((𝑀‘𝑊) ∖ I ) = dom ((( I ↾ (𝐷 ∖ ran 𝑊)) ∪ ((𝑊 cyclShift 1) ∘ ◡𝑊)) ∖ I )) |
| 117 | | difundir 4291 |
. . . . . 6
⊢ ((( I
↾ (𝐷 ∖ ran
𝑊)) ∪ ((𝑊 cyclShift 1) ∘ ◡𝑊)) ∖ I ) = ((( I ↾ (𝐷 ∖ ran 𝑊)) ∖ I ) ∪ (((𝑊 cyclShift 1) ∘ ◡𝑊) ∖ I )) |
| 118 | | resdifcom 6016 |
. . . . . . . 8
⊢ (( I
↾ (𝐷 ∖ ran
𝑊)) ∖ I ) = (( I
∖ I ) ↾ (𝐷
∖ ran 𝑊)) |
| 119 | | difid 4376 |
. . . . . . . . 9
⊢ ( I
∖ I ) = ∅ |
| 120 | 119 | reseq1i 5993 |
. . . . . . . 8
⊢ (( I
∖ I ) ↾ (𝐷
∖ ran 𝑊)) = (∅
↾ (𝐷 ∖ ran
𝑊)) |
| 121 | | 0res 32616 |
. . . . . . . 8
⊢ (∅
↾ (𝐷 ∖ ran
𝑊)) =
∅ |
| 122 | 118, 120,
121 | 3eqtri 2769 |
. . . . . . 7
⊢ (( I
↾ (𝐷 ∖ ran
𝑊)) ∖ I ) =
∅ |
| 123 | 122 | uneq1i 4164 |
. . . . . 6
⊢ ((( I
↾ (𝐷 ∖ ran
𝑊)) ∖ I ) ∪
(((𝑊 cyclShift 1) ∘
◡𝑊) ∖ I )) = (∅ ∪ (((𝑊 cyclShift 1) ∘ ◡𝑊) ∖ I )) |
| 124 | | 0un 4396 |
. . . . . 6
⊢ (∅
∪ (((𝑊 cyclShift 1)
∘ ◡𝑊) ∖ I )) = (((𝑊 cyclShift 1) ∘ ◡𝑊) ∖ I ) |
| 125 | 117, 123,
124 | 3eqtri 2769 |
. . . . 5
⊢ ((( I
↾ (𝐷 ∖ ran
𝑊)) ∪ ((𝑊 cyclShift 1) ∘ ◡𝑊)) ∖ I ) = (((𝑊 cyclShift 1) ∘ ◡𝑊) ∖ I ) |
| 126 | 125 | dmeqi 5915 |
. . . 4
⊢ dom ((( I
↾ (𝐷 ∖ ran
𝑊)) ∪ ((𝑊 cyclShift 1) ∘ ◡𝑊)) ∖ I ) = dom (((𝑊 cyclShift 1) ∘ ◡𝑊) ∖ I ) |
| 127 | | difss 4136 |
. . . . . 6
⊢ (((𝑊 cyclShift 1) ∘ ◡𝑊) ∖ I ) ⊆ ((𝑊 cyclShift 1) ∘ ◡𝑊) |
| 128 | | dmss 5913 |
. . . . . 6
⊢ ((((𝑊 cyclShift 1) ∘ ◡𝑊) ∖ I ) ⊆ ((𝑊 cyclShift 1) ∘ ◡𝑊) → dom (((𝑊 cyclShift 1) ∘ ◡𝑊) ∖ I ) ⊆ dom ((𝑊 cyclShift 1) ∘ ◡𝑊)) |
| 129 | 127, 128 | ax-mp 5 |
. . . . 5
⊢ dom
(((𝑊 cyclShift 1) ∘
◡𝑊) ∖ I ) ⊆ dom ((𝑊 cyclShift 1) ∘ ◡𝑊) |
| 130 | | dmcoss 5985 |
. . . . . 6
⊢ dom
((𝑊 cyclShift 1) ∘
◡𝑊) ⊆ dom ◡𝑊 |
| 131 | | df-rn 5696 |
. . . . . 6
⊢ ran 𝑊 = dom ◡𝑊 |
| 132 | 130, 131 | sseqtrri 4033 |
. . . . 5
⊢ dom
((𝑊 cyclShift 1) ∘
◡𝑊) ⊆ ran 𝑊 |
| 133 | 129, 132 | sstri 3993 |
. . . 4
⊢ dom
(((𝑊 cyclShift 1) ∘
◡𝑊) ∖ I ) ⊆ ran 𝑊 |
| 134 | 126, 133 | eqsstri 4030 |
. . 3
⊢ dom ((( I
↾ (𝐷 ∖ ran
𝑊)) ∪ ((𝑊 cyclShift 1) ∘ ◡𝑊)) ∖ I ) ⊆ ran 𝑊 |
| 135 | 116, 134 | eqsstrdi 4028 |
. 2
⊢ (𝜑 → dom ((𝑀‘𝑊) ∖ I ) ⊆ ran 𝑊) |
| 136 | 113, 135 | eqssd 4001 |
1
⊢ (𝜑 → ran 𝑊 = dom ((𝑀‘𝑊) ∖ I )) |