Step | Hyp | Ref
| Expression |
1 | | ssrab2 4009 |
. . . . 5
⊢ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ⊆ Word 𝐷 |
2 | | cycpmco2.w |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ dom 𝑀) |
3 | | cycpmco2.d |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
4 | | cycpmco2.c |
. . . . . . . . 9
⊢ 𝑀 = (toCyc‘𝐷) |
5 | | cycpmco2.s |
. . . . . . . . 9
⊢ 𝑆 = (SymGrp‘𝐷) |
6 | | eqid 2738 |
. . . . . . . . 9
⊢
(Base‘𝑆) =
(Base‘𝑆) |
7 | 4, 5, 6 | tocycf 31286 |
. . . . . . . 8
⊢ (𝐷 ∈ 𝑉 → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆)) |
8 | 3, 7 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆)) |
9 | 8 | fdmd 6595 |
. . . . . 6
⊢ (𝜑 → dom 𝑀 = {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) |
10 | 2, 9 | eleqtrd 2841 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) |
11 | 1, 10 | sselid 3915 |
. . . 4
⊢ (𝜑 → 𝑊 ∈ Word 𝐷) |
12 | | lencl 14164 |
. . . 4
⊢ (𝑊 ∈ Word 𝐷 → (♯‘𝑊) ∈
ℕ0) |
13 | 11, 12 | syl 17 |
. . 3
⊢ (𝜑 → (♯‘𝑊) ∈
ℕ0) |
14 | 13 | nn0cnd 12225 |
. 2
⊢ (𝜑 → (♯‘𝑊) ∈
ℂ) |
15 | | 1cnd 10901 |
. 2
⊢ (𝜑 → 1 ∈
ℂ) |
16 | | cycpmco2.1 |
. . . . . . 7
⊢ 𝑈 = (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) |
17 | | cycpmco2.e |
. . . . . . . . 9
⊢ 𝐸 = ((◡𝑊‘𝐽) + 1) |
18 | | ovexd 7290 |
. . . . . . . . 9
⊢ (𝜑 → ((◡𝑊‘𝐽) + 1) ∈ V) |
19 | 17, 18 | eqeltrid 2843 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ V) |
20 | | cycpmco2.i |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊)) |
21 | 20 | eldifad 3895 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ 𝐷) |
22 | 21 | s1cld 14236 |
. . . . . . . 8
⊢ (𝜑 → 〈“𝐼”〉 ∈ Word 𝐷) |
23 | | splval 14392 |
. . . . . . . 8
⊢ ((𝑊 ∈ dom 𝑀 ∧ (𝐸 ∈ V ∧ 𝐸 ∈ V ∧ 〈“𝐼”〉 ∈ Word 𝐷)) → (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) |
24 | 2, 19, 19, 22, 23 | syl13anc 1370 |
. . . . . . 7
⊢ (𝜑 → (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) |
25 | 16, 24 | syl5eq 2791 |
. . . . . 6
⊢ (𝜑 → 𝑈 = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) |
26 | 25 | fveq2d 6760 |
. . . . 5
⊢ (𝜑 → (♯‘𝑈) = (♯‘(((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉)))) |
27 | | pfxcl 14318 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝐷 → (𝑊 prefix 𝐸) ∈ Word 𝐷) |
28 | 11, 27 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑊 prefix 𝐸) ∈ Word 𝐷) |
29 | | ccatcl 14205 |
. . . . . . 7
⊢ (((𝑊 prefix 𝐸) ∈ Word 𝐷 ∧ 〈“𝐼”〉 ∈ Word 𝐷) → ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷) |
30 | 28, 22, 29 | syl2anc 583 |
. . . . . 6
⊢ (𝜑 → ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷) |
31 | | swrdcl 14286 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝐷 → (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷) |
32 | 11, 31 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷) |
33 | | ccatlen 14206 |
. . . . . 6
⊢ ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷 ∧ (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷) → (♯‘(((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) = ((♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) + (♯‘(𝑊 substr 〈𝐸, (♯‘𝑊)〉)))) |
34 | 30, 32, 33 | syl2anc 583 |
. . . . 5
⊢ (𝜑 → (♯‘(((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) = ((♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) + (♯‘(𝑊 substr 〈𝐸, (♯‘𝑊)〉)))) |
35 | | ccatws1len 14253 |
. . . . . . . 8
⊢ ((𝑊 prefix 𝐸) ∈ Word 𝐷 → (♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) = ((♯‘(𝑊 prefix 𝐸)) + 1)) |
36 | 28, 35 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) = ((♯‘(𝑊 prefix 𝐸)) + 1)) |
37 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊) |
38 | | dmeq 5801 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑊 → dom 𝑤 = dom 𝑊) |
39 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑊 → 𝐷 = 𝐷) |
40 | 37, 38, 39 | f1eq123d 6692 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑊 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑊:dom 𝑊–1-1→𝐷)) |
41 | 40 | elrab 3617 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ↔ (𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷)) |
42 | 10, 41 | sylib 217 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷)) |
43 | | f1cnv 6723 |
. . . . . . . . . . . . . . 15
⊢ (𝑊:dom 𝑊–1-1→𝐷 → ◡𝑊:ran 𝑊–1-1-onto→dom
𝑊) |
44 | 42, 43 | simpl2im 503 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ◡𝑊:ran 𝑊–1-1-onto→dom
𝑊) |
45 | | f1of 6700 |
. . . . . . . . . . . . . 14
⊢ (◡𝑊:ran 𝑊–1-1-onto→dom
𝑊 → ◡𝑊:ran 𝑊⟶dom 𝑊) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ◡𝑊:ran 𝑊⟶dom 𝑊) |
47 | | cycpmco2.j |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 ∈ ran 𝑊) |
48 | 46, 47 | ffvelrnd 6944 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ dom 𝑊) |
49 | | wrddm 14152 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ Word 𝐷 → dom 𝑊 = (0..^(♯‘𝑊))) |
50 | 11, 49 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom 𝑊 = (0..^(♯‘𝑊))) |
51 | 48, 50 | eleqtrd 2841 |
. . . . . . . . . . 11
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊))) |
52 | | fzofzp1 13412 |
. . . . . . . . . . 11
⊢ ((◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊)) → ((◡𝑊‘𝐽) + 1) ∈ (0...(♯‘𝑊))) |
53 | 51, 52 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((◡𝑊‘𝐽) + 1) ∈ (0...(♯‘𝑊))) |
54 | 17, 53 | eqeltrid 2843 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ (0...(♯‘𝑊))) |
55 | | pfxlen 14324 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix 𝐸)) = 𝐸) |
56 | 11, 54, 55 | syl2anc 583 |
. . . . . . . 8
⊢ (𝜑 → (♯‘(𝑊 prefix 𝐸)) = 𝐸) |
57 | 56 | oveq1d 7270 |
. . . . . . 7
⊢ (𝜑 → ((♯‘(𝑊 prefix 𝐸)) + 1) = (𝐸 + 1)) |
58 | 36, 57 | eqtrd 2778 |
. . . . . 6
⊢ (𝜑 → (♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) = (𝐸 + 1)) |
59 | | nn0fz0 13283 |
. . . . . . . 8
⊢
((♯‘𝑊)
∈ ℕ0 ↔ (♯‘𝑊) ∈ (0...(♯‘𝑊))) |
60 | 13, 59 | sylib 217 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝑊) ∈
(0...(♯‘𝑊))) |
61 | | swrdlen 14288 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ (0...(♯‘𝑊)) ∧ (♯‘𝑊) ∈
(0...(♯‘𝑊)))
→ (♯‘(𝑊
substr 〈𝐸,
(♯‘𝑊)〉)) =
((♯‘𝑊) −
𝐸)) |
62 | 11, 54, 60, 61 | syl3anc 1369 |
. . . . . 6
⊢ (𝜑 → (♯‘(𝑊 substr 〈𝐸, (♯‘𝑊)〉)) = ((♯‘𝑊) − 𝐸)) |
63 | 58, 62 | oveq12d 7273 |
. . . . 5
⊢ (𝜑 → ((♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) + (♯‘(𝑊 substr 〈𝐸, (♯‘𝑊)〉))) = ((𝐸 + 1) + ((♯‘𝑊) − 𝐸))) |
64 | 26, 34, 63 | 3eqtrd 2782 |
. . . 4
⊢ (𝜑 → (♯‘𝑈) = ((𝐸 + 1) + ((♯‘𝑊) − 𝐸))) |
65 | | fz0ssnn0 13280 |
. . . . . . . . 9
⊢
(0...(♯‘𝑊)) ⊆
ℕ0 |
66 | 65, 54 | sselid 3915 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈
ℕ0) |
67 | 66 | nn0zd 12353 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ ℤ) |
68 | 67 | peano2zd 12358 |
. . . . . 6
⊢ (𝜑 → (𝐸 + 1) ∈ ℤ) |
69 | 68 | zcnd 12356 |
. . . . 5
⊢ (𝜑 → (𝐸 + 1) ∈ ℂ) |
70 | 66 | nn0cnd 12225 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ ℂ) |
71 | 69, 14, 70 | addsubassd 11282 |
. . . 4
⊢ (𝜑 → (((𝐸 + 1) + (♯‘𝑊)) − 𝐸) = ((𝐸 + 1) + ((♯‘𝑊) − 𝐸))) |
72 | 70, 15, 14 | addassd 10928 |
. . . . 5
⊢ (𝜑 → ((𝐸 + 1) + (♯‘𝑊)) = (𝐸 + (1 + (♯‘𝑊)))) |
73 | 72 | oveq1d 7270 |
. . . 4
⊢ (𝜑 → (((𝐸 + 1) + (♯‘𝑊)) − 𝐸) = ((𝐸 + (1 + (♯‘𝑊))) − 𝐸)) |
74 | 64, 71, 73 | 3eqtr2d 2784 |
. . 3
⊢ (𝜑 → (♯‘𝑈) = ((𝐸 + (1 + (♯‘𝑊))) − 𝐸)) |
75 | 15, 14 | addcld 10925 |
. . . 4
⊢ (𝜑 → (1 + (♯‘𝑊)) ∈
ℂ) |
76 | 70, 75 | pncan2d 11264 |
. . 3
⊢ (𝜑 → ((𝐸 + (1 + (♯‘𝑊))) − 𝐸) = (1 + (♯‘𝑊))) |
77 | 15, 14 | addcomd 11107 |
. . 3
⊢ (𝜑 → (1 + (♯‘𝑊)) = ((♯‘𝑊) + 1)) |
78 | 74, 76, 77 | 3eqtrd 2782 |
. 2
⊢ (𝜑 → (♯‘𝑈) = ((♯‘𝑊) + 1)) |
79 | 14, 15, 78 | mvrraddd 11317 |
1
⊢ (𝜑 → ((♯‘𝑈) − 1) =
(♯‘𝑊)) |