Step | Hyp | Ref
| Expression |
1 | | cycpmco2.c |
. . 3
⊢ 𝑀 = (toCyc‘𝐷) |
2 | | cycpmco2.s |
. . 3
⊢ 𝑆 = (SymGrp‘𝐷) |
3 | | cycpmco2.d |
. . 3
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
4 | | cycpmco2.w |
. . 3
⊢ (𝜑 → 𝑊 ∈ dom 𝑀) |
5 | | cycpmco2.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊)) |
6 | | cycpmco2.j |
. . 3
⊢ (𝜑 → 𝐽 ∈ ran 𝑊) |
7 | | cycpmco2.e |
. . 3
⊢ 𝐸 = ((◡𝑊‘𝐽) + 1) |
8 | | cycpmco2.1 |
. . 3
⊢ 𝑈 = (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | cycpmco2lem1 31295 |
. 2
⊢ (𝜑 → ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝐼)) = ((𝑀‘𝑊)‘𝐽)) |
10 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → 𝐷 ∈ 𝑉) |
11 | | ssrab2 4009 |
. . . . . . . . 9
⊢ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ⊆ Word 𝐷 |
12 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑆) =
(Base‘𝑆) |
13 | 1, 2, 12 | tocycf 31286 |
. . . . . . . . . . . 12
⊢ (𝐷 ∈ 𝑉 → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆)) |
14 | 3, 13 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆)) |
15 | 14 | fdmd 6595 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝑀 = {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) |
16 | 4, 15 | eleqtrd 2841 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) |
17 | 11, 16 | sselid 3915 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ Word 𝐷) |
18 | 5 | eldifad 3895 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ 𝐷) |
19 | 18 | s1cld 14236 |
. . . . . . . 8
⊢ (𝜑 → 〈“𝐼”〉 ∈ Word 𝐷) |
20 | | splcl 14393 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐷 ∧ 〈“𝐼”〉 ∈ Word 𝐷) → (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) ∈ Word 𝐷) |
21 | 17, 19, 20 | syl2anc 583 |
. . . . . . 7
⊢ (𝜑 → (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) ∈ Word 𝐷) |
22 | 8, 21 | eqeltrid 2843 |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ Word 𝐷) |
23 | 22 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → 𝑈 ∈ Word 𝐷) |
24 | 1, 2, 3, 4, 5, 6, 7, 8 | cycpmco2f1 31293 |
. . . . . 6
⊢ (𝜑 → 𝑈:dom 𝑈–1-1→𝐷) |
25 | 24 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → 𝑈:dom 𝑈–1-1→𝐷) |
26 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → 𝐸 ∈ (0..^(♯‘𝑊))) |
27 | 1, 2, 3, 4, 5, 6, 7, 8 | cycpmco2lem3 31297 |
. . . . . . . 8
⊢ (𝜑 → ((♯‘𝑈) − 1) =
(♯‘𝑊)) |
28 | 27 | oveq2d 7271 |
. . . . . . 7
⊢ (𝜑 → (0..^((♯‘𝑈) − 1)) =
(0..^(♯‘𝑊))) |
29 | 28 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) →
(0..^((♯‘𝑈)
− 1)) = (0..^(♯‘𝑊))) |
30 | 26, 29 | eleqtrrd 2842 |
. . . . 5
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → 𝐸 ∈ (0..^((♯‘𝑈) − 1))) |
31 | 1, 10, 23, 25, 30 | cycpmfv1 31282 |
. . . 4
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑀‘𝑈)‘(𝑈‘𝐸)) = (𝑈‘(𝐸 + 1))) |
32 | 1, 2, 3, 4, 5, 6, 7, 8 | cycpmco2lem2 31296 |
. . . . . 6
⊢ (𝜑 → (𝑈‘𝐸) = 𝐼) |
33 | 32 | fveq2d 6760 |
. . . . 5
⊢ (𝜑 → ((𝑀‘𝑈)‘(𝑈‘𝐸)) = ((𝑀‘𝑈)‘𝐼)) |
34 | 33 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑀‘𝑈)‘(𝑈‘𝐸)) = ((𝑀‘𝑈)‘𝐼)) |
35 | 17 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → 𝑊 ∈ Word 𝐷) |
36 | | lencl 14164 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝐷 → (♯‘𝑊) ∈
ℕ0) |
37 | 17, 36 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝑊) ∈
ℕ0) |
38 | | nn0fz0 13283 |
. . . . . . . 8
⊢
((♯‘𝑊)
∈ ℕ0 ↔ (♯‘𝑊) ∈ (0...(♯‘𝑊))) |
39 | 37, 38 | sylib 217 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝑊) ∈
(0...(♯‘𝑊))) |
40 | 39 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → (♯‘𝑊) ∈
(0...(♯‘𝑊))) |
41 | | swrdfv0 14290 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ (0..^(♯‘𝑊)) ∧ (♯‘𝑊) ∈
(0...(♯‘𝑊)))
→ ((𝑊 substr
〈𝐸,
(♯‘𝑊)〉)‘0) = (𝑊‘𝐸)) |
42 | 35, 26, 40, 41 | syl3anc 1369 |
. . . . 5
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑊 substr 〈𝐸, (♯‘𝑊)〉)‘0) = (𝑊‘𝐸)) |
43 | | ovexd 7290 |
. . . . . . . . . . 11
⊢ (𝜑 → ((◡𝑊‘𝐽) + 1) ∈ V) |
44 | 7, 43 | eqeltrid 2843 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ V) |
45 | | splval 14392 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ dom 𝑀 ∧ (𝐸 ∈ V ∧ 𝐸 ∈ V ∧ 〈“𝐼”〉 ∈ Word 𝐷)) → (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) |
46 | 4, 44, 44, 19, 45 | syl13anc 1370 |
. . . . . . . . 9
⊢ (𝜑 → (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) |
47 | 8, 46 | syl5eq 2791 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) |
48 | 47 | fveq1d 6758 |
. . . . . . 7
⊢ (𝜑 → (𝑈‘(𝐸 + 1)) = ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))‘(𝐸 + 1))) |
49 | 48 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → (𝑈‘(𝐸 + 1)) = ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))‘(𝐸 + 1))) |
50 | | pfxcl 14318 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝐷 → (𝑊 prefix 𝐸) ∈ Word 𝐷) |
51 | 17, 50 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑊 prefix 𝐸) ∈ Word 𝐷) |
52 | | ccatcl 14205 |
. . . . . . . . 9
⊢ (((𝑊 prefix 𝐸) ∈ Word 𝐷 ∧ 〈“𝐼”〉 ∈ Word 𝐷) → ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷) |
53 | 51, 19, 52 | syl2anc 583 |
. . . . . . . 8
⊢ (𝜑 → ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷) |
54 | 53 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷) |
55 | | swrdcl 14286 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝐷 → (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷) |
56 | 17, 55 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷) |
57 | 56 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷) |
58 | | 1z 12280 |
. . . . . . . . . . 11
⊢ 1 ∈
ℤ |
59 | | fzoaddel 13368 |
. . . . . . . . . . 11
⊢ ((𝐸 ∈
(0..^(♯‘𝑊))
∧ 1 ∈ ℤ) → (𝐸 + 1) ∈ ((0 +
1)..^((♯‘𝑊) +
1))) |
60 | 58, 59 | mpan2 687 |
. . . . . . . . . 10
⊢ (𝐸 ∈
(0..^(♯‘𝑊))
→ (𝐸 + 1) ∈ ((0 +
1)..^((♯‘𝑊) +
1))) |
61 | | elfzolt2b 13327 |
. . . . . . . . . 10
⊢ ((𝐸 + 1) ∈ ((0 +
1)..^((♯‘𝑊) +
1)) → (𝐸 + 1) ∈
((𝐸 +
1)..^((♯‘𝑊) +
1))) |
62 | 60, 61 | syl 17 |
. . . . . . . . 9
⊢ (𝐸 ∈
(0..^(♯‘𝑊))
→ (𝐸 + 1) ∈
((𝐸 +
1)..^((♯‘𝑊) +
1))) |
63 | 62 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → (𝐸 + 1) ∈ ((𝐸 + 1)..^((♯‘𝑊) + 1))) |
64 | | ccatws1len 14253 |
. . . . . . . . . . . 12
⊢ ((𝑊 prefix 𝐸) ∈ Word 𝐷 → (♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) = ((♯‘(𝑊 prefix 𝐸)) + 1)) |
65 | 51, 64 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) = ((♯‘(𝑊 prefix 𝐸)) + 1)) |
66 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊) |
67 | | dmeq 5801 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑊 → dom 𝑤 = dom 𝑊) |
68 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑊 → 𝐷 = 𝐷) |
69 | 66, 67, 68 | f1eq123d 6692 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = 𝑊 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑊:dom 𝑊–1-1→𝐷)) |
70 | 69 | elrab3 3618 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑊 ∈ Word 𝐷 → (𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ↔ 𝑊:dom 𝑊–1-1→𝐷)) |
71 | 70 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) → 𝑊:dom 𝑊–1-1→𝐷) |
72 | 17, 16, 71 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷) |
73 | | f1cnv 6723 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑊:dom 𝑊–1-1→𝐷 → ◡𝑊:ran 𝑊–1-1-onto→dom
𝑊) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ◡𝑊:ran 𝑊–1-1-onto→dom
𝑊) |
75 | | f1of 6700 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝑊:ran 𝑊–1-1-onto→dom
𝑊 → ◡𝑊:ran 𝑊⟶dom 𝑊) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ◡𝑊:ran 𝑊⟶dom 𝑊) |
77 | 76, 6 | ffvelrnd 6944 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ dom 𝑊) |
78 | | wrddm 14152 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ Word 𝐷 → dom 𝑊 = (0..^(♯‘𝑊))) |
79 | 17, 78 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝑊 = (0..^(♯‘𝑊))) |
80 | 77, 79 | eleqtrd 2841 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊))) |
81 | | fzofzp1 13412 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊)) → ((◡𝑊‘𝐽) + 1) ∈ (0...(♯‘𝑊))) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((◡𝑊‘𝐽) + 1) ∈ (0...(♯‘𝑊))) |
83 | 7, 82 | eqeltrid 2843 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐸 ∈ (0...(♯‘𝑊))) |
84 | | pfxlen 14324 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix 𝐸)) = 𝐸) |
85 | 17, 83, 84 | syl2anc 583 |
. . . . . . . . . . . 12
⊢ (𝜑 → (♯‘(𝑊 prefix 𝐸)) = 𝐸) |
86 | 85 | oveq1d 7270 |
. . . . . . . . . . 11
⊢ (𝜑 → ((♯‘(𝑊 prefix 𝐸)) + 1) = (𝐸 + 1)) |
87 | 65, 86 | eqtrd 2778 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) = (𝐸 + 1)) |
88 | 87 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) →
(♯‘((𝑊 prefix
𝐸) ++ 〈“𝐼”〉)) = (𝐸 + 1)) |
89 | 47 | fveq2d 6760 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝑈) = (♯‘(((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉)))) |
90 | | ccatlen 14206 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷 ∧ (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷) → (♯‘(((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) = ((♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) + (♯‘(𝑊 substr 〈𝐸, (♯‘𝑊)〉)))) |
91 | 53, 56, 90 | syl2anc 583 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (♯‘(((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) = ((♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) + (♯‘(𝑊 substr 〈𝐸, (♯‘𝑊)〉)))) |
92 | | swrdlen 14288 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ (0...(♯‘𝑊)) ∧ (♯‘𝑊) ∈
(0...(♯‘𝑊)))
→ (♯‘(𝑊
substr 〈𝐸,
(♯‘𝑊)〉)) =
((♯‘𝑊) −
𝐸)) |
93 | 17, 83, 39, 92 | syl3anc 1369 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘(𝑊 substr 〈𝐸, (♯‘𝑊)〉)) = ((♯‘𝑊) − 𝐸)) |
94 | 87, 93 | oveq12d 7273 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) + (♯‘(𝑊 substr 〈𝐸, (♯‘𝑊)〉))) = ((𝐸 + 1) + ((♯‘𝑊) − 𝐸))) |
95 | 89, 91, 94 | 3eqtrd 2782 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘𝑈) = ((𝐸 + 1) + ((♯‘𝑊) − 𝐸))) |
96 | | fz0ssnn0 13280 |
. . . . . . . . . . . . . . . . . 18
⊢
(0...(♯‘𝑊)) ⊆
ℕ0 |
97 | 96, 83 | sselid 3915 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐸 ∈
ℕ0) |
98 | 97 | nn0zd 12353 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐸 ∈ ℤ) |
99 | 98 | peano2zd 12358 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐸 + 1) ∈ ℤ) |
100 | 99 | zcnd 12356 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐸 + 1) ∈ ℂ) |
101 | 37 | nn0cnd 12225 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (♯‘𝑊) ∈
ℂ) |
102 | 97 | nn0cnd 12225 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 ∈ ℂ) |
103 | 100, 101,
102 | addsubassd 11282 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝐸 + 1) + (♯‘𝑊)) − 𝐸) = ((𝐸 + 1) + ((♯‘𝑊) − 𝐸))) |
104 | | 1cnd 10901 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℂ) |
105 | 102, 104,
101 | addassd 10928 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐸 + 1) + (♯‘𝑊)) = (𝐸 + (1 + (♯‘𝑊)))) |
106 | 105 | oveq1d 7270 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝐸 + 1) + (♯‘𝑊)) − 𝐸) = ((𝐸 + (1 + (♯‘𝑊))) − 𝐸)) |
107 | 95, 103, 106 | 3eqtr2d 2784 |
. . . . . . . . . . . 12
⊢ (𝜑 → (♯‘𝑈) = ((𝐸 + (1 + (♯‘𝑊))) − 𝐸)) |
108 | 104, 101 | addcld 10925 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 + (♯‘𝑊)) ∈
ℂ) |
109 | 102, 108 | pncan2d 11264 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐸 + (1 + (♯‘𝑊))) − 𝐸) = (1 + (♯‘𝑊))) |
110 | 104, 101 | addcomd 11107 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 + (♯‘𝑊)) = ((♯‘𝑊) + 1)) |
111 | 107, 109,
110 | 3eqtrd 2782 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝑈) = ((♯‘𝑊) + 1)) |
112 | 89, 111, 91 | 3eqtr3rd 2787 |
. . . . . . . . . 10
⊢ (𝜑 → ((♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) + (♯‘(𝑊 substr 〈𝐸, (♯‘𝑊)〉))) = ((♯‘𝑊) + 1)) |
113 | 112 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) →
((♯‘((𝑊 prefix
𝐸) ++ 〈“𝐼”〉)) +
(♯‘(𝑊 substr
〈𝐸,
(♯‘𝑊)〉)))
= ((♯‘𝑊) +
1)) |
114 | 88, 113 | oveq12d 7273 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) →
((♯‘((𝑊 prefix
𝐸) ++ 〈“𝐼”〉))..^((♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) + (♯‘(𝑊 substr 〈𝐸, (♯‘𝑊)〉)))) = ((𝐸 + 1)..^((♯‘𝑊) + 1))) |
115 | 63, 114 | eleqtrrd 2842 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → (𝐸 + 1) ∈ ((♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉))..^((♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) + (♯‘(𝑊 substr 〈𝐸, (♯‘𝑊)〉))))) |
116 | | ccatval2 14211 |
. . . . . . 7
⊢ ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷 ∧ (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷 ∧ (𝐸 + 1) ∈ ((♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉))..^((♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) + (♯‘(𝑊 substr 〈𝐸, (♯‘𝑊)〉))))) → ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))‘(𝐸 + 1)) = ((𝑊 substr 〈𝐸, (♯‘𝑊)〉)‘((𝐸 + 1) − (♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉))))) |
117 | 54, 57, 115, 116 | syl3anc 1369 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))‘(𝐸 + 1)) = ((𝑊 substr 〈𝐸, (♯‘𝑊)〉)‘((𝐸 + 1) − (♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉))))) |
118 | 87 | oveq2d 7271 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸 + 1) − (♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉))) = ((𝐸 + 1) − (𝐸 + 1))) |
119 | 100 | subidd 11250 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸 + 1) − (𝐸 + 1)) = 0) |
120 | 118, 119 | eqtrd 2778 |
. . . . . . . 8
⊢ (𝜑 → ((𝐸 + 1) − (♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉))) = 0) |
121 | 120 | fveq2d 6760 |
. . . . . . 7
⊢ (𝜑 → ((𝑊 substr 〈𝐸, (♯‘𝑊)〉)‘((𝐸 + 1) − (♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)))) = ((𝑊 substr 〈𝐸, (♯‘𝑊)〉)‘0)) |
122 | 121 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑊 substr 〈𝐸, (♯‘𝑊)〉)‘((𝐸 + 1) − (♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)))) = ((𝑊 substr 〈𝐸, (♯‘𝑊)〉)‘0)) |
123 | 49, 117, 122 | 3eqtrd 2782 |
. . . . 5
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → (𝑈‘(𝐸 + 1)) = ((𝑊 substr 〈𝐸, (♯‘𝑊)〉)‘0)) |
124 | 7 | fveq2i 6759 |
. . . . . . 7
⊢ (𝑊‘𝐸) = (𝑊‘((◡𝑊‘𝐽) + 1)) |
125 | 124 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → (𝑊‘𝐸) = (𝑊‘((◡𝑊‘𝐽) + 1))) |
126 | 72 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → 𝑊:dom 𝑊–1-1→𝐷) |
127 | 7 | oveq1i 7265 |
. . . . . . . . . 10
⊢ (𝐸 − 1) = (((◡𝑊‘𝐽) + 1) − 1) |
128 | | elfzonn0 13360 |
. . . . . . . . . . . . 13
⊢ ((◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊)) → (◡𝑊‘𝐽) ∈
ℕ0) |
129 | 80, 128 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡𝑊‘𝐽) ∈
ℕ0) |
130 | 129 | nn0cnd 12225 |
. . . . . . . . . . 11
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ ℂ) |
131 | 130, 104 | pncand 11263 |
. . . . . . . . . 10
⊢ (𝜑 → (((◡𝑊‘𝐽) + 1) − 1) = (◡𝑊‘𝐽)) |
132 | 127, 131 | eqtr2id 2792 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝑊‘𝐽) = (𝐸 − 1)) |
133 | 132 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → (◡𝑊‘𝐽) = (𝐸 − 1)) |
134 | | nn0p1gt0 12192 |
. . . . . . . . . . . . . 14
⊢ ((◡𝑊‘𝐽) ∈ ℕ0 → 0 <
((◡𝑊‘𝐽) + 1)) |
135 | 129, 134 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < ((◡𝑊‘𝐽) + 1)) |
136 | 135, 7 | breqtrrdi 5112 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 𝐸) |
137 | 136 | gt0ne0d 11469 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ≠ 0) |
138 | 137 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → 𝐸 ≠ 0) |
139 | | fzo1fzo0n0 13366 |
. . . . . . . . . 10
⊢ (𝐸 ∈
(1..^(♯‘𝑊))
↔ (𝐸 ∈
(0..^(♯‘𝑊))
∧ 𝐸 ≠
0)) |
140 | 26, 138, 139 | sylanbrc 582 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → 𝐸 ∈ (1..^(♯‘𝑊))) |
141 | | elfzo1elm1fzo0 13416 |
. . . . . . . . 9
⊢ (𝐸 ∈
(1..^(♯‘𝑊))
→ (𝐸 − 1) ∈
(0..^((♯‘𝑊)
− 1))) |
142 | 140, 141 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → (𝐸 − 1) ∈
(0..^((♯‘𝑊)
− 1))) |
143 | 133, 142 | eqeltrd 2839 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → (◡𝑊‘𝐽) ∈ (0..^((♯‘𝑊) − 1))) |
144 | 1, 10, 35, 126, 143 | cycpmfv1 31282 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑀‘𝑊)‘(𝑊‘(◡𝑊‘𝐽))) = (𝑊‘((◡𝑊‘𝐽) + 1))) |
145 | | f1f1orn 6711 |
. . . . . . . . . 10
⊢ (𝑊:dom 𝑊–1-1→𝐷 → 𝑊:dom 𝑊–1-1-onto→ran
𝑊) |
146 | 72, 145 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊:dom 𝑊–1-1-onto→ran
𝑊) |
147 | | f1ocnvfv2 7130 |
. . . . . . . . 9
⊢ ((𝑊:dom 𝑊–1-1-onto→ran
𝑊 ∧ 𝐽 ∈ ran 𝑊) → (𝑊‘(◡𝑊‘𝐽)) = 𝐽) |
148 | 146, 6, 147 | syl2anc 583 |
. . . . . . . 8
⊢ (𝜑 → (𝑊‘(◡𝑊‘𝐽)) = 𝐽) |
149 | 148 | fveq2d 6760 |
. . . . . . 7
⊢ (𝜑 → ((𝑀‘𝑊)‘(𝑊‘(◡𝑊‘𝐽))) = ((𝑀‘𝑊)‘𝐽)) |
150 | 149 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑀‘𝑊)‘(𝑊‘(◡𝑊‘𝐽))) = ((𝑀‘𝑊)‘𝐽)) |
151 | 125, 144,
150 | 3eqtr2rd 2785 |
. . . . 5
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑀‘𝑊)‘𝐽) = (𝑊‘𝐸)) |
152 | 42, 123, 151 | 3eqtr4d 2788 |
. . . 4
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → (𝑈‘(𝐸 + 1)) = ((𝑀‘𝑊)‘𝐽)) |
153 | 31, 34, 152 | 3eqtr3rd 2787 |
. . 3
⊢ ((𝜑 ∧ 𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑀‘𝑊)‘𝐽) = ((𝑀‘𝑈)‘𝐼)) |
154 | 149 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐸 = (♯‘𝑊)) → ((𝑀‘𝑊)‘(𝑊‘(◡𝑊‘𝐽))) = ((𝑀‘𝑊)‘𝐽)) |
155 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐸 = (♯‘𝑊)) → 𝐷 ∈ 𝑉) |
156 | 17 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐸 = (♯‘𝑊)) → 𝑊 ∈ Word 𝐷) |
157 | 72 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐸 = (♯‘𝑊)) → 𝑊:dom 𝑊–1-1→𝐷) |
158 | 136 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐸 = (♯‘𝑊)) → 0 < 𝐸) |
159 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐸 = (♯‘𝑊)) → 𝐸 = (♯‘𝑊)) |
160 | 158, 159 | breqtrd 5096 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐸 = (♯‘𝑊)) → 0 < (♯‘𝑊)) |
161 | | oveq1 7262 |
. . . . . . 7
⊢ (𝐸 = (♯‘𝑊) → (𝐸 − 1) = ((♯‘𝑊) − 1)) |
162 | 132, 161 | sylan9eq 2799 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐸 = (♯‘𝑊)) → (◡𝑊‘𝐽) = ((♯‘𝑊) − 1)) |
163 | 1, 155, 156, 157, 160, 162 | cycpmfv2 31283 |
. . . . 5
⊢ ((𝜑 ∧ 𝐸 = (♯‘𝑊)) → ((𝑀‘𝑊)‘(𝑊‘(◡𝑊‘𝐽))) = (𝑊‘0)) |
164 | 154, 163 | eqtr3d 2780 |
. . . 4
⊢ ((𝜑 ∧ 𝐸 = (♯‘𝑊)) → ((𝑀‘𝑊)‘𝐽) = (𝑊‘0)) |
165 | 22 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐸 = (♯‘𝑊)) → 𝑈 ∈ Word 𝐷) |
166 | 24 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐸 = (♯‘𝑊)) → 𝑈:dom 𝑈–1-1→𝐷) |
167 | | nn0p1gt0 12192 |
. . . . . . . . 9
⊢
((♯‘𝑊)
∈ ℕ0 → 0 < ((♯‘𝑊) + 1)) |
168 | 37, 167 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 0 <
((♯‘𝑊) +
1)) |
169 | 168, 111 | breqtrrd 5098 |
. . . . . . 7
⊢ (𝜑 → 0 <
(♯‘𝑈)) |
170 | 169 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐸 = (♯‘𝑊)) → 0 < (♯‘𝑈)) |
171 | 27 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐸 = (♯‘𝑊)) → ((♯‘𝑈) − 1) = (♯‘𝑊)) |
172 | 159, 171 | eqtr4d 2781 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐸 = (♯‘𝑊)) → 𝐸 = ((♯‘𝑈) − 1)) |
173 | 1, 155, 165, 166, 170, 172 | cycpmfv2 31283 |
. . . . 5
⊢ ((𝜑 ∧ 𝐸 = (♯‘𝑊)) → ((𝑀‘𝑈)‘(𝑈‘𝐸)) = (𝑈‘0)) |
174 | 47 | fveq1d 6758 |
. . . . . 6
⊢ (𝜑 → (𝑈‘0) = ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))‘0)) |
175 | 174 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐸 = (♯‘𝑊)) → (𝑈‘0) = ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))‘0)) |
176 | | nn0p1nn 12202 |
. . . . . . . . . . 11
⊢ (𝐸 ∈ ℕ0
→ (𝐸 + 1) ∈
ℕ) |
177 | 97, 176 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸 + 1) ∈ ℕ) |
178 | | lbfzo0 13355 |
. . . . . . . . . 10
⊢ (0 ∈
(0..^(𝐸 + 1)) ↔ (𝐸 + 1) ∈
ℕ) |
179 | 177, 178 | sylibr 233 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ (0..^(𝐸 + 1))) |
180 | 87 | oveq2d 7271 |
. . . . . . . . 9
⊢ (𝜑 →
(0..^(♯‘((𝑊
prefix 𝐸) ++
〈“𝐼”〉))) = (0..^(𝐸 + 1))) |
181 | 179, 180 | eleqtrrd 2842 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
(0..^(♯‘((𝑊
prefix 𝐸) ++
〈“𝐼”〉)))) |
182 | | ccatval1 14209 |
. . . . . . . 8
⊢ ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷 ∧ (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷 ∧ 0 ∈ (0..^(♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)))) → ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))‘0) = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)‘0)) |
183 | 53, 56, 181, 182 | syl3anc 1369 |
. . . . . . 7
⊢ (𝜑 → ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))‘0) = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)‘0)) |
184 | | nn0p1nn 12202 |
. . . . . . . . . . . 12
⊢ ((◡𝑊‘𝐽) ∈ ℕ0 → ((◡𝑊‘𝐽) + 1) ∈ ℕ) |
185 | 129, 184 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((◡𝑊‘𝐽) + 1) ∈ ℕ) |
186 | 7, 185 | eqeltrid 2843 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ ℕ) |
187 | | lbfzo0 13355 |
. . . . . . . . . 10
⊢ (0 ∈
(0..^𝐸) ↔ 𝐸 ∈
ℕ) |
188 | 186, 187 | sylibr 233 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ (0..^𝐸)) |
189 | 85 | oveq2d 7271 |
. . . . . . . . 9
⊢ (𝜑 → (0..^(♯‘(𝑊 prefix 𝐸))) = (0..^𝐸)) |
190 | 188, 189 | eleqtrrd 2842 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
(0..^(♯‘(𝑊
prefix 𝐸)))) |
191 | | ccatval1 14209 |
. . . . . . . 8
⊢ (((𝑊 prefix 𝐸) ∈ Word 𝐷 ∧ 〈“𝐼”〉 ∈ Word 𝐷 ∧ 0 ∈ (0..^(♯‘(𝑊 prefix 𝐸)))) → (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)‘0) = ((𝑊 prefix 𝐸)‘0)) |
192 | 51, 19, 190, 191 | syl3anc 1369 |
. . . . . . 7
⊢ (𝜑 → (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)‘0) = ((𝑊 prefix 𝐸)‘0)) |
193 | | fzne1 31011 |
. . . . . . . . . 10
⊢ ((𝐸 ∈
(0...(♯‘𝑊))
∧ 𝐸 ≠ 0) →
𝐸 ∈ ((0 +
1)...(♯‘𝑊))) |
194 | 83, 137, 193 | syl2anc 583 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ ((0 + 1)...(♯‘𝑊))) |
195 | | 0p1e1 12025 |
. . . . . . . . . 10
⊢ (0 + 1) =
1 |
196 | 195 | oveq1i 7265 |
. . . . . . . . 9
⊢ ((0 +
1)...(♯‘𝑊)) =
(1...(♯‘𝑊)) |
197 | 194, 196 | eleqtrdi 2849 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ (1...(♯‘𝑊))) |
198 | | pfxfv0 14333 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ (1...(♯‘𝑊))) → ((𝑊 prefix 𝐸)‘0) = (𝑊‘0)) |
199 | 17, 197, 198 | syl2anc 583 |
. . . . . . 7
⊢ (𝜑 → ((𝑊 prefix 𝐸)‘0) = (𝑊‘0)) |
200 | 183, 192,
199 | 3eqtrd 2782 |
. . . . . 6
⊢ (𝜑 → ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))‘0) = (𝑊‘0)) |
201 | 200 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐸 = (♯‘𝑊)) → ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))‘0) = (𝑊‘0)) |
202 | 173, 175,
201 | 3eqtrd 2782 |
. . . 4
⊢ ((𝜑 ∧ 𝐸 = (♯‘𝑊)) → ((𝑀‘𝑈)‘(𝑈‘𝐸)) = (𝑊‘0)) |
203 | 33 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐸 = (♯‘𝑊)) → ((𝑀‘𝑈)‘(𝑈‘𝐸)) = ((𝑀‘𝑈)‘𝐼)) |
204 | 164, 202,
203 | 3eqtr2d 2784 |
. . 3
⊢ ((𝜑 ∧ 𝐸 = (♯‘𝑊)) → ((𝑀‘𝑊)‘𝐽) = ((𝑀‘𝑈)‘𝐼)) |
205 | | elfzr 13428 |
. . . 4
⊢ (𝐸 ∈
(0...(♯‘𝑊))
→ (𝐸 ∈
(0..^(♯‘𝑊))
∨ 𝐸 =
(♯‘𝑊))) |
206 | 83, 205 | syl 17 |
. . 3
⊢ (𝜑 → (𝐸 ∈ (0..^(♯‘𝑊)) ∨ 𝐸 = (♯‘𝑊))) |
207 | 153, 204,
206 | mpjaodan 955 |
. 2
⊢ (𝜑 → ((𝑀‘𝑊)‘𝐽) = ((𝑀‘𝑈)‘𝐼)) |
208 | 9, 207 | eqtrd 2778 |
1
⊢ (𝜑 → ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝐼)) = ((𝑀‘𝑈)‘𝐼)) |