Step | Hyp | Ref
| Expression |
1 | | un23 4068 |
. 2
⊢ (((𝑊 “ (0..^𝐸)) ∪ {𝐼}) ∪ (𝑊 “ (𝐸..^(♯‘𝑊)))) = (((𝑊 “ (0..^𝐸)) ∪ (𝑊 “ (𝐸..^(♯‘𝑊)))) ∪ {𝐼}) |
2 | | cycpmco2.1 |
. . . . 5
⊢ 𝑈 = (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) |
3 | | cycpmco2.w |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ dom 𝑀) |
4 | | cycpmco2.e |
. . . . . . 7
⊢ 𝐸 = ((◡𝑊‘𝐽) + 1) |
5 | | ovexd 7217 |
. . . . . . 7
⊢ (𝜑 → ((◡𝑊‘𝐽) + 1) ∈ V) |
6 | 4, 5 | eqeltrid 2838 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ V) |
7 | | cycpmco2.i |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊)) |
8 | 7 | eldifad 3865 |
. . . . . . 7
⊢ (𝜑 → 𝐼 ∈ 𝐷) |
9 | 8 | s1cld 14058 |
. . . . . 6
⊢ (𝜑 → 〈“𝐼”〉 ∈ Word 𝐷) |
10 | | splval 14214 |
. . . . . 6
⊢ ((𝑊 ∈ dom 𝑀 ∧ (𝐸 ∈ V ∧ 𝐸 ∈ V ∧ 〈“𝐼”〉 ∈ Word 𝐷)) → (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) |
11 | 3, 6, 6, 9, 10 | syl13anc 1373 |
. . . . 5
⊢ (𝜑 → (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) |
12 | 2, 11 | syl5eq 2786 |
. . . 4
⊢ (𝜑 → 𝑈 = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) |
13 | 12 | rneqd 5791 |
. . 3
⊢ (𝜑 → ran 𝑈 = ran (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) |
14 | | ssrab2 3979 |
. . . . . . 7
⊢ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ⊆ Word 𝐷 |
15 | | cycpmco2.d |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
16 | | cycpmco2.c |
. . . . . . . . . . 11
⊢ 𝑀 = (toCyc‘𝐷) |
17 | | cycpmco2.s |
. . . . . . . . . . 11
⊢ 𝑆 = (SymGrp‘𝐷) |
18 | | eqid 2739 |
. . . . . . . . . . 11
⊢
(Base‘𝑆) =
(Base‘𝑆) |
19 | 16, 17, 18 | tocycf 30973 |
. . . . . . . . . 10
⊢ (𝐷 ∈ 𝑉 → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆)) |
20 | 15, 19 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆)) |
21 | 20 | fdmd 6525 |
. . . . . . . 8
⊢ (𝜑 → dom 𝑀 = {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) |
22 | 3, 21 | eleqtrd 2836 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) |
23 | 14, 22 | sseldi 3885 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ Word 𝐷) |
24 | | pfxcl 14140 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐷 → (𝑊 prefix 𝐸) ∈ Word 𝐷) |
25 | 23, 24 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑊 prefix 𝐸) ∈ Word 𝐷) |
26 | | ccatcl 14027 |
. . . . 5
⊢ (((𝑊 prefix 𝐸) ∈ Word 𝐷 ∧ 〈“𝐼”〉 ∈ Word 𝐷) → ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷) |
27 | 25, 9, 26 | syl2anc 587 |
. . . 4
⊢ (𝜑 → ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷) |
28 | | swrdcl 14108 |
. . . . 5
⊢ (𝑊 ∈ Word 𝐷 → (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷) |
29 | 23, 28 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷) |
30 | | ccatrn 14044 |
. . . 4
⊢ ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷 ∧ (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷) → ran (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉)) = (ran ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∪ ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) |
31 | 27, 29, 30 | syl2anc 587 |
. . 3
⊢ (𝜑 → ran (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉)) = (ran ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∪ ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) |
32 | | ccatrn 14044 |
. . . . . 6
⊢ (((𝑊 prefix 𝐸) ∈ Word 𝐷 ∧ 〈“𝐼”〉 ∈ Word 𝐷) → ran ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) = (ran (𝑊 prefix 𝐸) ∪ ran 〈“𝐼”〉)) |
33 | 25, 9, 32 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → ran ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) = (ran (𝑊 prefix 𝐸) ∪ ran 〈“𝐼”〉)) |
34 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊) |
35 | | dmeq 5756 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑊 → dom 𝑤 = dom 𝑊) |
36 | | eqidd 2740 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑊 → 𝐷 = 𝐷) |
37 | 34, 35, 36 | f1eq123d 6622 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑊 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑊:dom 𝑊–1-1→𝐷)) |
38 | 37 | elrab 3593 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ↔ (𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷)) |
39 | 22, 38 | sylib 221 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷)) |
40 | 39 | simprd 499 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷) |
41 | | f1cnv 6653 |
. . . . . . . . . . . 12
⊢ (𝑊:dom 𝑊–1-1→𝐷 → ◡𝑊:ran 𝑊–1-1-onto→dom
𝑊) |
42 | | f1of 6630 |
. . . . . . . . . . . 12
⊢ (◡𝑊:ran 𝑊–1-1-onto→dom
𝑊 → ◡𝑊:ran 𝑊⟶dom 𝑊) |
43 | 40, 41, 42 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → ◡𝑊:ran 𝑊⟶dom 𝑊) |
44 | | cycpmco2.j |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ ran 𝑊) |
45 | 43, 44 | ffvelrnd 6874 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ dom 𝑊) |
46 | | wrddm 13974 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝐷 → dom 𝑊 = (0..^(♯‘𝑊))) |
47 | 23, 46 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝑊 = (0..^(♯‘𝑊))) |
48 | 45, 47 | eleqtrd 2836 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊))) |
49 | | fzofzp1 13237 |
. . . . . . . . 9
⊢ ((◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊)) → ((◡𝑊‘𝐽) + 1) ∈ (0...(♯‘𝑊))) |
50 | 48, 49 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((◡𝑊‘𝐽) + 1) ∈ (0...(♯‘𝑊))) |
51 | 4, 50 | eqeltrid 2838 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ (0...(♯‘𝑊))) |
52 | | pfxrn3 30802 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ (0...(♯‘𝑊))) → ran (𝑊 prefix 𝐸) = (𝑊 “ (0..^𝐸))) |
53 | 23, 51, 52 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → ran (𝑊 prefix 𝐸) = (𝑊 “ (0..^𝐸))) |
54 | | s1rn 14054 |
. . . . . . 7
⊢ (𝐼 ∈ 𝐷 → ran 〈“𝐼”〉 = {𝐼}) |
55 | 8, 54 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran 〈“𝐼”〉 = {𝐼}) |
56 | 53, 55 | uneq12d 4064 |
. . . . 5
⊢ (𝜑 → (ran (𝑊 prefix 𝐸) ∪ ran 〈“𝐼”〉) = ((𝑊 “ (0..^𝐸)) ∪ {𝐼})) |
57 | 33, 56 | eqtrd 2774 |
. . . 4
⊢ (𝜑 → ran ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) = ((𝑊 “ (0..^𝐸)) ∪ {𝐼})) |
58 | | lencl 13986 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐷 → (♯‘𝑊) ∈
ℕ0) |
59 | | nn0fz0 13108 |
. . . . . . 7
⊢
((♯‘𝑊)
∈ ℕ0 ↔ (♯‘𝑊) ∈ (0...(♯‘𝑊))) |
60 | 59 | biimpi 219 |
. . . . . 6
⊢
((♯‘𝑊)
∈ ℕ0 → (♯‘𝑊) ∈ (0...(♯‘𝑊))) |
61 | 23, 58, 60 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (♯‘𝑊) ∈
(0...(♯‘𝑊))) |
62 | | swrdrn3 30814 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ (0...(♯‘𝑊)) ∧ (♯‘𝑊) ∈
(0...(♯‘𝑊)))
→ ran (𝑊 substr
〈𝐸,
(♯‘𝑊)〉) =
(𝑊 “ (𝐸..^(♯‘𝑊)))) |
63 | 23, 51, 61, 62 | syl3anc 1372 |
. . . 4
⊢ (𝜑 → ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉) = (𝑊 “ (𝐸..^(♯‘𝑊)))) |
64 | 57, 63 | uneq12d 4064 |
. . 3
⊢ (𝜑 → (ran ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∪ ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉)) = (((𝑊 “ (0..^𝐸)) ∪ {𝐼}) ∪ (𝑊 “ (𝐸..^(♯‘𝑊))))) |
65 | 13, 31, 64 | 3eqtrd 2778 |
. 2
⊢ (𝜑 → ran 𝑈 = (((𝑊 “ (0..^𝐸)) ∪ {𝐼}) ∪ (𝑊 “ (𝐸..^(♯‘𝑊))))) |
66 | | fzosplit 13173 |
. . . . . 6
⊢ (𝐸 ∈
(0...(♯‘𝑊))
→ (0..^(♯‘𝑊)) = ((0..^𝐸) ∪ (𝐸..^(♯‘𝑊)))) |
67 | 51, 66 | syl 17 |
. . . . 5
⊢ (𝜑 → (0..^(♯‘𝑊)) = ((0..^𝐸) ∪ (𝐸..^(♯‘𝑊)))) |
68 | 67 | imaeq2d 5913 |
. . . 4
⊢ (𝜑 → (𝑊 “ (0..^(♯‘𝑊))) = (𝑊 “ ((0..^𝐸) ∪ (𝐸..^(♯‘𝑊))))) |
69 | | wrdf 13972 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝐷 → 𝑊:(0..^(♯‘𝑊))⟶𝐷) |
70 | 23, 69 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑊:(0..^(♯‘𝑊))⟶𝐷) |
71 | 70 | ffnd 6515 |
. . . . 5
⊢ (𝜑 → 𝑊 Fn (0..^(♯‘𝑊))) |
72 | | fnima 6477 |
. . . . 5
⊢ (𝑊 Fn (0..^(♯‘𝑊)) → (𝑊 “ (0..^(♯‘𝑊))) = ran 𝑊) |
73 | 71, 72 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑊 “ (0..^(♯‘𝑊))) = ran 𝑊) |
74 | | elfzuz3 13007 |
. . . . . 6
⊢ (𝐸 ∈
(0...(♯‘𝑊))
→ (♯‘𝑊)
∈ (ℤ≥‘𝐸)) |
75 | | fzoss2 13168 |
. . . . . 6
⊢
((♯‘𝑊)
∈ (ℤ≥‘𝐸) → (0..^𝐸) ⊆ (0..^(♯‘𝑊))) |
76 | 51, 74, 75 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (0..^𝐸) ⊆ (0..^(♯‘𝑊))) |
77 | | fz0ssnn0 13105 |
. . . . . . . 8
⊢
(0...(♯‘𝑊)) ⊆
ℕ0 |
78 | 77, 51 | sseldi 3885 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈
ℕ0) |
79 | | nn0uz 12374 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
80 | 78, 79 | eleqtrdi 2844 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈
(ℤ≥‘0)) |
81 | | fzoss1 13167 |
. . . . . 6
⊢ (𝐸 ∈
(ℤ≥‘0) → (𝐸..^(♯‘𝑊)) ⊆ (0..^(♯‘𝑊))) |
82 | 80, 81 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐸..^(♯‘𝑊)) ⊆ (0..^(♯‘𝑊))) |
83 | | unima 6755 |
. . . . 5
⊢ ((𝑊 Fn (0..^(♯‘𝑊)) ∧ (0..^𝐸) ⊆ (0..^(♯‘𝑊)) ∧ (𝐸..^(♯‘𝑊)) ⊆ (0..^(♯‘𝑊))) → (𝑊 “ ((0..^𝐸) ∪ (𝐸..^(♯‘𝑊)))) = ((𝑊 “ (0..^𝐸)) ∪ (𝑊 “ (𝐸..^(♯‘𝑊))))) |
84 | 71, 76, 82, 83 | syl3anc 1372 |
. . . 4
⊢ (𝜑 → (𝑊 “ ((0..^𝐸) ∪ (𝐸..^(♯‘𝑊)))) = ((𝑊 “ (0..^𝐸)) ∪ (𝑊 “ (𝐸..^(♯‘𝑊))))) |
85 | 68, 73, 84 | 3eqtr3d 2782 |
. . 3
⊢ (𝜑 → ran 𝑊 = ((𝑊 “ (0..^𝐸)) ∪ (𝑊 “ (𝐸..^(♯‘𝑊))))) |
86 | 85 | uneq1d 4062 |
. 2
⊢ (𝜑 → (ran 𝑊 ∪ {𝐼}) = (((𝑊 “ (0..^𝐸)) ∪ (𝑊 “ (𝐸..^(♯‘𝑊)))) ∪ {𝐼})) |
87 | 1, 65, 86 | 3eqtr4a 2800 |
1
⊢ (𝜑 → ran 𝑈 = (ran 𝑊 ∪ {𝐼})) |