Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cycpmco2lem4 Structured version   Visualization version   GIF version

Theorem cycpmco2lem4 31298
Description: Lemma for cycpmco2 31302. (Contributed by Thierry Arnoux, 4-Jan-2024.)
Hypotheses
Ref Expression
cycpmco2.c 𝑀 = (toCyc‘𝐷)
cycpmco2.s 𝑆 = (SymGrp‘𝐷)
cycpmco2.d (𝜑𝐷𝑉)
cycpmco2.w (𝜑𝑊 ∈ dom 𝑀)
cycpmco2.i (𝜑𝐼 ∈ (𝐷 ∖ ran 𝑊))
cycpmco2.j (𝜑𝐽 ∈ ran 𝑊)
cycpmco2.e 𝐸 = ((𝑊𝐽) + 1)
cycpmco2.1 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)
Assertion
Ref Expression
cycpmco2lem4 (𝜑 → ((𝑀𝑊)‘((𝑀‘⟨“𝐼𝐽”⟩)‘𝐼)) = ((𝑀𝑈)‘𝐼))

Proof of Theorem cycpmco2lem4
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef 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 ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)
91, 2, 3, 4, 5, 6, 7, 8cycpmco2lem1 31295 . 2 (𝜑 → ((𝑀𝑊)‘((𝑀‘⟨“𝐼𝐽”⟩)‘𝐼)) = ((𝑀𝑊)‘𝐽))
103adantr 480 . . . . 5 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → 𝐷𝑉)
11 ssrab2 4009 . . . . . . . . 9 {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ⊆ Word 𝐷
12 eqid 2738 . . . . . . . . . . . . 13 (Base‘𝑆) = (Base‘𝑆)
131, 2, 12tocycf 31286 . . . . . . . . . . . 12 (𝐷𝑉𝑀:{𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}⟶(Base‘𝑆))
143, 13syl 17 . . . . . . . . . . 11 (𝜑𝑀:{𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}⟶(Base‘𝑆))
1514fdmd 6595 . . . . . . . . . 10 (𝜑 → dom 𝑀 = {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
164, 15eleqtrd 2841 . . . . . . . . 9 (𝜑𝑊 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
1711, 16sselid 3915 . . . . . . . 8 (𝜑𝑊 ∈ Word 𝐷)
185eldifad 3895 . . . . . . . . 9 (𝜑𝐼𝐷)
1918s1cld 14236 . . . . . . . 8 (𝜑 → ⟨“𝐼”⟩ ∈ Word 𝐷)
20 splcl 14393 . . . . . . . 8 ((𝑊 ∈ Word 𝐷 ∧ ⟨“𝐼”⟩ ∈ Word 𝐷) → (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩) ∈ Word 𝐷)
2117, 19, 20syl2anc 583 . . . . . . 7 (𝜑 → (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩) ∈ Word 𝐷)
228, 21eqeltrid 2843 . . . . . 6 (𝜑𝑈 ∈ Word 𝐷)
2322adantr 480 . . . . 5 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → 𝑈 ∈ Word 𝐷)
241, 2, 3, 4, 5, 6, 7, 8cycpmco2f1 31293 . . . . . 6 (𝜑𝑈:dom 𝑈1-1𝐷)
2524adantr 480 . . . . 5 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → 𝑈:dom 𝑈1-1𝐷)
26 simpr 484 . . . . . 6 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → 𝐸 ∈ (0..^(♯‘𝑊)))
271, 2, 3, 4, 5, 6, 7, 8cycpmco2lem3 31297 . . . . . . . 8 (𝜑 → ((♯‘𝑈) − 1) = (♯‘𝑊))
2827oveq2d 7271 . . . . . . 7 (𝜑 → (0..^((♯‘𝑈) − 1)) = (0..^(♯‘𝑊)))
2928adantr 480 . . . . . 6 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (0..^((♯‘𝑈) − 1)) = (0..^(♯‘𝑊)))
3026, 29eleqtrrd 2842 . . . . 5 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → 𝐸 ∈ (0..^((♯‘𝑈) − 1)))
311, 10, 23, 25, 30cycpmfv1 31282 . . . 4 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑀𝑈)‘(𝑈𝐸)) = (𝑈‘(𝐸 + 1)))
321, 2, 3, 4, 5, 6, 7, 8cycpmco2lem2 31296 . . . . . 6 (𝜑 → (𝑈𝐸) = 𝐼)
3332fveq2d 6760 . . . . 5 (𝜑 → ((𝑀𝑈)‘(𝑈𝐸)) = ((𝑀𝑈)‘𝐼))
3433adantr 480 . . . 4 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑀𝑈)‘(𝑈𝐸)) = ((𝑀𝑈)‘𝐼))
3517adantr 480 . . . . . 6 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → 𝑊 ∈ Word 𝐷)
36 lencl 14164 . . . . . . . . 9 (𝑊 ∈ Word 𝐷 → (♯‘𝑊) ∈ ℕ0)
3717, 36syl 17 . . . . . . . 8 (𝜑 → (♯‘𝑊) ∈ ℕ0)
38 nn0fz0 13283 . . . . . . . 8 ((♯‘𝑊) ∈ ℕ0 ↔ (♯‘𝑊) ∈ (0...(♯‘𝑊)))
3937, 38sylib 217 . . . . . . 7 (𝜑 → (♯‘𝑊) ∈ (0...(♯‘𝑊)))
4039adantr 480 . . . . . 6 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (♯‘𝑊) ∈ (0...(♯‘𝑊)))
41 swrdfv0 14290 . . . . . 6 ((𝑊 ∈ Word 𝐷𝐸 ∈ (0..^(♯‘𝑊)) ∧ (♯‘𝑊) ∈ (0...(♯‘𝑊))) → ((𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)‘0) = (𝑊𝐸))
4235, 26, 40, 41syl3anc 1369 . . . . 5 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)‘0) = (𝑊𝐸))
43 ovexd 7290 . . . . . . . . . . 11 (𝜑 → ((𝑊𝐽) + 1) ∈ V)
447, 43eqeltrid 2843 . . . . . . . . . 10 (𝜑𝐸 ∈ V)
45 splval 14392 . . . . . . . . . 10 ((𝑊 ∈ dom 𝑀 ∧ (𝐸 ∈ V ∧ 𝐸 ∈ V ∧ ⟨“𝐼”⟩ ∈ Word 𝐷)) → (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩) = (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)))
464, 44, 44, 19, 45syl13anc 1370 . . . . . . . . 9 (𝜑 → (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩) = (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)))
478, 46syl5eq 2791 . . . . . . . 8 (𝜑𝑈 = (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)))
4847fveq1d 6758 . . . . . . 7 (𝜑 → (𝑈‘(𝐸 + 1)) = ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘(𝐸 + 1)))
4948adantr 480 . . . . . 6 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (𝑈‘(𝐸 + 1)) = ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘(𝐸 + 1)))
50 pfxcl 14318 . . . . . . . . . 10 (𝑊 ∈ Word 𝐷 → (𝑊 prefix 𝐸) ∈ Word 𝐷)
5117, 50syl 17 . . . . . . . . 9 (𝜑 → (𝑊 prefix 𝐸) ∈ Word 𝐷)
52 ccatcl 14205 . . . . . . . . 9 (((𝑊 prefix 𝐸) ∈ Word 𝐷 ∧ ⟨“𝐼”⟩ ∈ Word 𝐷) → ((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ∈ Word 𝐷)
5351, 19, 52syl2anc 583 . . . . . . . 8 (𝜑 → ((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ∈ Word 𝐷)
5453adantr 480 . . . . . . 7 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ∈ Word 𝐷)
55 swrdcl 14286 . . . . . . . . 9 (𝑊 ∈ Word 𝐷 → (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∈ Word 𝐷)
5617, 55syl 17 . . . . . . . 8 (𝜑 → (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∈ Word 𝐷)
5756adantr 480 . . . . . . 7 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∈ Word 𝐷)
58 1z 12280 . . . . . . . . . . 11 1 ∈ ℤ
59 fzoaddel 13368 . . . . . . . . . . 11 ((𝐸 ∈ (0..^(♯‘𝑊)) ∧ 1 ∈ ℤ) → (𝐸 + 1) ∈ ((0 + 1)..^((♯‘𝑊) + 1)))
6058, 59mpan2 687 . . . . . . . . . 10 (𝐸 ∈ (0..^(♯‘𝑊)) → (𝐸 + 1) ∈ ((0 + 1)..^((♯‘𝑊) + 1)))
61 elfzolt2b 13327 . . . . . . . . . 10 ((𝐸 + 1) ∈ ((0 + 1)..^((♯‘𝑊) + 1)) → (𝐸 + 1) ∈ ((𝐸 + 1)..^((♯‘𝑊) + 1)))
6260, 61syl 17 . . . . . . . . 9 (𝐸 ∈ (0..^(♯‘𝑊)) → (𝐸 + 1) ∈ ((𝐸 + 1)..^((♯‘𝑊) + 1)))
6362adantl 481 . . . . . . . 8 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (𝐸 + 1) ∈ ((𝐸 + 1)..^((♯‘𝑊) + 1)))
64 ccatws1len 14253 . . . . . . . . . . . 12 ((𝑊 prefix 𝐸) ∈ Word 𝐷 → (♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) = ((♯‘(𝑊 prefix 𝐸)) + 1))
6551, 64syl 17 . . . . . . . . . . 11 (𝜑 → (♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) = ((♯‘(𝑊 prefix 𝐸)) + 1))
66 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑊𝑤 = 𝑊)
67 dmeq 5801 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑊 → dom 𝑤 = dom 𝑊)
68 eqidd 2739 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑊𝐷 = 𝐷)
6966, 67, 68f1eq123d 6692 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑊 → (𝑤:dom 𝑤1-1𝐷𝑊:dom 𝑊1-1𝐷))
7069elrab3 3618 . . . . . . . . . . . . . . . . . . . . 21 (𝑊 ∈ Word 𝐷 → (𝑊 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ↔ 𝑊:dom 𝑊1-1𝐷))
7170biimpa 476 . . . . . . . . . . . . . . . . . . . 20 ((𝑊 ∈ Word 𝐷𝑊 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) → 𝑊:dom 𝑊1-1𝐷)
7217, 16, 71syl2anc 583 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑊:dom 𝑊1-1𝐷)
73 f1cnv 6723 . . . . . . . . . . . . . . . . . . 19 (𝑊:dom 𝑊1-1𝐷𝑊:ran 𝑊1-1-onto→dom 𝑊)
7472, 73syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑊:ran 𝑊1-1-onto→dom 𝑊)
75 f1of 6700 . . . . . . . . . . . . . . . . . 18 (𝑊:ran 𝑊1-1-onto→dom 𝑊𝑊:ran 𝑊⟶dom 𝑊)
7674, 75syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑊:ran 𝑊⟶dom 𝑊)
7776, 6ffvelrnd 6944 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑊𝐽) ∈ dom 𝑊)
78 wrddm 14152 . . . . . . . . . . . . . . . . 17 (𝑊 ∈ Word 𝐷 → dom 𝑊 = (0..^(♯‘𝑊)))
7917, 78syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝑊 = (0..^(♯‘𝑊)))
8077, 79eleqtrd 2841 . . . . . . . . . . . . . . 15 (𝜑 → (𝑊𝐽) ∈ (0..^(♯‘𝑊)))
81 fzofzp1 13412 . . . . . . . . . . . . . . 15 ((𝑊𝐽) ∈ (0..^(♯‘𝑊)) → ((𝑊𝐽) + 1) ∈ (0...(♯‘𝑊)))
8280, 81syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝑊𝐽) + 1) ∈ (0...(♯‘𝑊)))
837, 82eqeltrid 2843 . . . . . . . . . . . . 13 (𝜑𝐸 ∈ (0...(♯‘𝑊)))
84 pfxlen 14324 . . . . . . . . . . . . 13 ((𝑊 ∈ Word 𝐷𝐸 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix 𝐸)) = 𝐸)
8517, 83, 84syl2anc 583 . . . . . . . . . . . 12 (𝜑 → (♯‘(𝑊 prefix 𝐸)) = 𝐸)
8685oveq1d 7270 . . . . . . . . . . 11 (𝜑 → ((♯‘(𝑊 prefix 𝐸)) + 1) = (𝐸 + 1))
8765, 86eqtrd 2778 . . . . . . . . . 10 (𝜑 → (♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) = (𝐸 + 1))
8887adantr 480 . . . . . . . . 9 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) = (𝐸 + 1))
8947fveq2d 6760 . . . . . . . . . . 11 (𝜑 → (♯‘𝑈) = (♯‘(((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))))
90 ccatlen 14206 . . . . . . . . . . . . . . 15 ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ∈ Word 𝐷 ∧ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∈ Word 𝐷) → (♯‘(((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))) = ((♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) + (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))))
9153, 56, 90syl2anc 583 . . . . . . . . . . . . . 14 (𝜑 → (♯‘(((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))) = ((♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) + (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))))
92 swrdlen 14288 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ Word 𝐷𝐸 ∈ (0...(♯‘𝑊)) ∧ (♯‘𝑊) ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)) = ((♯‘𝑊) − 𝐸))
9317, 83, 39, 92syl3anc 1369 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)) = ((♯‘𝑊) − 𝐸))
9487, 93oveq12d 7273 . . . . . . . . . . . . . 14 (𝜑 → ((♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) + (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))) = ((𝐸 + 1) + ((♯‘𝑊) − 𝐸)))
9589, 91, 943eqtrd 2782 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝑈) = ((𝐸 + 1) + ((♯‘𝑊) − 𝐸)))
96 fz0ssnn0 13280 . . . . . . . . . . . . . . . . . 18 (0...(♯‘𝑊)) ⊆ ℕ0
9796, 83sselid 3915 . . . . . . . . . . . . . . . . 17 (𝜑𝐸 ∈ ℕ0)
9897nn0zd 12353 . . . . . . . . . . . . . . . 16 (𝜑𝐸 ∈ ℤ)
9998peano2zd 12358 . . . . . . . . . . . . . . 15 (𝜑 → (𝐸 + 1) ∈ ℤ)
10099zcnd 12356 . . . . . . . . . . . . . 14 (𝜑 → (𝐸 + 1) ∈ ℂ)
10137nn0cnd 12225 . . . . . . . . . . . . . 14 (𝜑 → (♯‘𝑊) ∈ ℂ)
10297nn0cnd 12225 . . . . . . . . . . . . . 14 (𝜑𝐸 ∈ ℂ)
103100, 101, 102addsubassd 11282 . . . . . . . . . . . . 13 (𝜑 → (((𝐸 + 1) + (♯‘𝑊)) − 𝐸) = ((𝐸 + 1) + ((♯‘𝑊) − 𝐸)))
104 1cnd 10901 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℂ)
105102, 104, 101addassd 10928 . . . . . . . . . . . . . 14 (𝜑 → ((𝐸 + 1) + (♯‘𝑊)) = (𝐸 + (1 + (♯‘𝑊))))
106105oveq1d 7270 . . . . . . . . . . . . 13 (𝜑 → (((𝐸 + 1) + (♯‘𝑊)) − 𝐸) = ((𝐸 + (1 + (♯‘𝑊))) − 𝐸))
10795, 103, 1063eqtr2d 2784 . . . . . . . . . . . 12 (𝜑 → (♯‘𝑈) = ((𝐸 + (1 + (♯‘𝑊))) − 𝐸))
108104, 101addcld 10925 . . . . . . . . . . . . 13 (𝜑 → (1 + (♯‘𝑊)) ∈ ℂ)
109102, 108pncan2d 11264 . . . . . . . . . . . 12 (𝜑 → ((𝐸 + (1 + (♯‘𝑊))) − 𝐸) = (1 + (♯‘𝑊)))
110104, 101addcomd 11107 . . . . . . . . . . . 12 (𝜑 → (1 + (♯‘𝑊)) = ((♯‘𝑊) + 1))
111107, 109, 1103eqtrd 2782 . . . . . . . . . . 11 (𝜑 → (♯‘𝑈) = ((♯‘𝑊) + 1))
11289, 111, 913eqtr3rd 2787 . . . . . . . . . 10 (𝜑 → ((♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) + (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))) = ((♯‘𝑊) + 1))
113112adantr 480 . . . . . . . . 9 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) + (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))) = ((♯‘𝑊) + 1))
11488, 113oveq12d 7273 . . . . . . . 8 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩))..^((♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) + (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)))) = ((𝐸 + 1)..^((♯‘𝑊) + 1)))
11563, 114eleqtrrd 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 𝐸) ++ ⟨“𝐼”⟩)))))
11754, 57, 115, 116syl3anc 1369 . . . . . 6 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘(𝐸 + 1)) = ((𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)‘((𝐸 + 1) − (♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)))))
11887oveq2d 7271 . . . . . . . . 9 (𝜑 → ((𝐸 + 1) − (♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩))) = ((𝐸 + 1) − (𝐸 + 1)))
119100subidd 11250 . . . . . . . . 9 (𝜑 → ((𝐸 + 1) − (𝐸 + 1)) = 0)
120118, 119eqtrd 2778 . . . . . . . 8 (𝜑 → ((𝐸 + 1) − (♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩))) = 0)
121120fveq2d 6760 . . . . . . 7 (𝜑 → ((𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)‘((𝐸 + 1) − (♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)))) = ((𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)‘0))
122121adantr 480 . . . . . 6 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)‘((𝐸 + 1) − (♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)))) = ((𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)‘0))
12349, 117, 1223eqtrd 2782 . . . . 5 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (𝑈‘(𝐸 + 1)) = ((𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)‘0))
1247fveq2i 6759 . . . . . . 7 (𝑊𝐸) = (𝑊‘((𝑊𝐽) + 1))
125124a1i 11 . . . . . 6 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (𝑊𝐸) = (𝑊‘((𝑊𝐽) + 1)))
12672adantr 480 . . . . . . 7 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → 𝑊:dom 𝑊1-1𝐷)
1277oveq1i 7265 . . . . . . . . . 10 (𝐸 − 1) = (((𝑊𝐽) + 1) − 1)
128 elfzonn0 13360 . . . . . . . . . . . . 13 ((𝑊𝐽) ∈ (0..^(♯‘𝑊)) → (𝑊𝐽) ∈ ℕ0)
12980, 128syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑊𝐽) ∈ ℕ0)
130129nn0cnd 12225 . . . . . . . . . . 11 (𝜑 → (𝑊𝐽) ∈ ℂ)
131130, 104pncand 11263 . . . . . . . . . 10 (𝜑 → (((𝑊𝐽) + 1) − 1) = (𝑊𝐽))
132127, 131eqtr2id 2792 . . . . . . . . 9 (𝜑 → (𝑊𝐽) = (𝐸 − 1))
133132adantr 480 . . . . . . . 8 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (𝑊𝐽) = (𝐸 − 1))
134 nn0p1gt0 12192 . . . . . . . . . . . . . 14 ((𝑊𝐽) ∈ ℕ0 → 0 < ((𝑊𝐽) + 1))
135129, 134syl 17 . . . . . . . . . . . . 13 (𝜑 → 0 < ((𝑊𝐽) + 1))
136135, 7breqtrrdi 5112 . . . . . . . . . . . 12 (𝜑 → 0 < 𝐸)
137136gt0ne0d 11469 . . . . . . . . . . 11 (𝜑𝐸 ≠ 0)
138137adantr 480 . . . . . . . . . 10 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → 𝐸 ≠ 0)
139 fzo1fzo0n0 13366 . . . . . . . . . 10 (𝐸 ∈ (1..^(♯‘𝑊)) ↔ (𝐸 ∈ (0..^(♯‘𝑊)) ∧ 𝐸 ≠ 0))
14026, 138, 139sylanbrc 582 . . . . . . . . 9 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → 𝐸 ∈ (1..^(♯‘𝑊)))
141 elfzo1elm1fzo0 13416 . . . . . . . . 9 (𝐸 ∈ (1..^(♯‘𝑊)) → (𝐸 − 1) ∈ (0..^((♯‘𝑊) − 1)))
142140, 141syl 17 . . . . . . . 8 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (𝐸 − 1) ∈ (0..^((♯‘𝑊) − 1)))
143133, 142eqeltrd 2839 . . . . . . 7 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (𝑊𝐽) ∈ (0..^((♯‘𝑊) − 1)))
1441, 10, 35, 126, 143cycpmfv1 31282 . . . . . 6 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑀𝑊)‘(𝑊‘(𝑊𝐽))) = (𝑊‘((𝑊𝐽) + 1)))
145 f1f1orn 6711 . . . . . . . . . 10 (𝑊:dom 𝑊1-1𝐷𝑊:dom 𝑊1-1-onto→ran 𝑊)
14672, 145syl 17 . . . . . . . . 9 (𝜑𝑊:dom 𝑊1-1-onto→ran 𝑊)
147 f1ocnvfv2 7130 . . . . . . . . 9 ((𝑊:dom 𝑊1-1-onto→ran 𝑊𝐽 ∈ ran 𝑊) → (𝑊‘(𝑊𝐽)) = 𝐽)
148146, 6, 147syl2anc 583 . . . . . . . 8 (𝜑 → (𝑊‘(𝑊𝐽)) = 𝐽)
149148fveq2d 6760 . . . . . . 7 (𝜑 → ((𝑀𝑊)‘(𝑊‘(𝑊𝐽))) = ((𝑀𝑊)‘𝐽))
150149adantr 480 . . . . . 6 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑀𝑊)‘(𝑊‘(𝑊𝐽))) = ((𝑀𝑊)‘𝐽))
151125, 144, 1503eqtr2rd 2785 . . . . 5 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑀𝑊)‘𝐽) = (𝑊𝐸))
15242, 123, 1513eqtr4d 2788 . . . 4 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (𝑈‘(𝐸 + 1)) = ((𝑀𝑊)‘𝐽))
15331, 34, 1523eqtr3rd 2787 . . 3 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑀𝑊)‘𝐽) = ((𝑀𝑈)‘𝐼))
154149adantr 480 . . . . 5 ((𝜑𝐸 = (♯‘𝑊)) → ((𝑀𝑊)‘(𝑊‘(𝑊𝐽))) = ((𝑀𝑊)‘𝐽))
1553adantr 480 . . . . . 6 ((𝜑𝐸 = (♯‘𝑊)) → 𝐷𝑉)
15617adantr 480 . . . . . 6 ((𝜑𝐸 = (♯‘𝑊)) → 𝑊 ∈ Word 𝐷)
15772adantr 480 . . . . . 6 ((𝜑𝐸 = (♯‘𝑊)) → 𝑊:dom 𝑊1-1𝐷)
158136adantr 480 . . . . . . 7 ((𝜑𝐸 = (♯‘𝑊)) → 0 < 𝐸)
159 simpr 484 . . . . . . 7 ((𝜑𝐸 = (♯‘𝑊)) → 𝐸 = (♯‘𝑊))
160158, 159breqtrd 5096 . . . . . 6 ((𝜑𝐸 = (♯‘𝑊)) → 0 < (♯‘𝑊))
161 oveq1 7262 . . . . . . 7 (𝐸 = (♯‘𝑊) → (𝐸 − 1) = ((♯‘𝑊) − 1))
162132, 161sylan9eq 2799 . . . . . 6 ((𝜑𝐸 = (♯‘𝑊)) → (𝑊𝐽) = ((♯‘𝑊) − 1))
1631, 155, 156, 157, 160, 162cycpmfv2 31283 . . . . 5 ((𝜑𝐸 = (♯‘𝑊)) → ((𝑀𝑊)‘(𝑊‘(𝑊𝐽))) = (𝑊‘0))
164154, 163eqtr3d 2780 . . . 4 ((𝜑𝐸 = (♯‘𝑊)) → ((𝑀𝑊)‘𝐽) = (𝑊‘0))
16522adantr 480 . . . . . 6 ((𝜑𝐸 = (♯‘𝑊)) → 𝑈 ∈ Word 𝐷)
16624adantr 480 . . . . . 6 ((𝜑𝐸 = (♯‘𝑊)) → 𝑈:dom 𝑈1-1𝐷)
167 nn0p1gt0 12192 . . . . . . . . 9 ((♯‘𝑊) ∈ ℕ0 → 0 < ((♯‘𝑊) + 1))
16837, 167syl 17 . . . . . . . 8 (𝜑 → 0 < ((♯‘𝑊) + 1))
169168, 111breqtrrd 5098 . . . . . . 7 (𝜑 → 0 < (♯‘𝑈))
170169adantr 480 . . . . . 6 ((𝜑𝐸 = (♯‘𝑊)) → 0 < (♯‘𝑈))
17127adantr 480 . . . . . . 7 ((𝜑𝐸 = (♯‘𝑊)) → ((♯‘𝑈) − 1) = (♯‘𝑊))
172159, 171eqtr4d 2781 . . . . . 6 ((𝜑𝐸 = (♯‘𝑊)) → 𝐸 = ((♯‘𝑈) − 1))
1731, 155, 165, 166, 170, 172cycpmfv2 31283 . . . . 5 ((𝜑𝐸 = (♯‘𝑊)) → ((𝑀𝑈)‘(𝑈𝐸)) = (𝑈‘0))
17447fveq1d 6758 . . . . . 6 (𝜑 → (𝑈‘0) = ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘0))
175174adantr 480 . . . . 5 ((𝜑𝐸 = (♯‘𝑊)) → (𝑈‘0) = ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘0))
176 nn0p1nn 12202 . . . . . . . . . . 11 (𝐸 ∈ ℕ0 → (𝐸 + 1) ∈ ℕ)
17797, 176syl 17 . . . . . . . . . 10 (𝜑 → (𝐸 + 1) ∈ ℕ)
178 lbfzo0 13355 . . . . . . . . . 10 (0 ∈ (0..^(𝐸 + 1)) ↔ (𝐸 + 1) ∈ ℕ)
179177, 178sylibr 233 . . . . . . . . 9 (𝜑 → 0 ∈ (0..^(𝐸 + 1)))
18087oveq2d 7271 . . . . . . . . 9 (𝜑 → (0..^(♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩))) = (0..^(𝐸 + 1)))
181179, 180eleqtrrd 2842 . . . . . . . 8 (𝜑 → 0 ∈ (0..^(♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩))))
182 ccatval1 14209 . . . . . . . 8 ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ∈ Word 𝐷 ∧ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∈ Word 𝐷 ∧ 0 ∈ (0..^(♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)))) → ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘0) = (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)‘0))
18353, 56, 181, 182syl3anc 1369 . . . . . . 7 (𝜑 → ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘0) = (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)‘0))
184 nn0p1nn 12202 . . . . . . . . . . . 12 ((𝑊𝐽) ∈ ℕ0 → ((𝑊𝐽) + 1) ∈ ℕ)
185129, 184syl 17 . . . . . . . . . . 11 (𝜑 → ((𝑊𝐽) + 1) ∈ ℕ)
1867, 185eqeltrid 2843 . . . . . . . . . 10 (𝜑𝐸 ∈ ℕ)
187 lbfzo0 13355 . . . . . . . . . 10 (0 ∈ (0..^𝐸) ↔ 𝐸 ∈ ℕ)
188186, 187sylibr 233 . . . . . . . . 9 (𝜑 → 0 ∈ (0..^𝐸))
18985oveq2d 7271 . . . . . . . . 9 (𝜑 → (0..^(♯‘(𝑊 prefix 𝐸))) = (0..^𝐸))
190188, 189eleqtrrd 2842 . . . . . . . 8 (𝜑 → 0 ∈ (0..^(♯‘(𝑊 prefix 𝐸))))
191 ccatval1 14209 . . . . . . . 8 (((𝑊 prefix 𝐸) ∈ Word 𝐷 ∧ ⟨“𝐼”⟩ ∈ Word 𝐷 ∧ 0 ∈ (0..^(♯‘(𝑊 prefix 𝐸)))) → (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)‘0) = ((𝑊 prefix 𝐸)‘0))
19251, 19, 190, 191syl3anc 1369 . . . . . . 7 (𝜑 → (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)‘0) = ((𝑊 prefix 𝐸)‘0))
193 fzne1 31011 . . . . . . . . . 10 ((𝐸 ∈ (0...(♯‘𝑊)) ∧ 𝐸 ≠ 0) → 𝐸 ∈ ((0 + 1)...(♯‘𝑊)))
19483, 137, 193syl2anc 583 . . . . . . . . 9 (𝜑𝐸 ∈ ((0 + 1)...(♯‘𝑊)))
195 0p1e1 12025 . . . . . . . . . 10 (0 + 1) = 1
196195oveq1i 7265 . . . . . . . . 9 ((0 + 1)...(♯‘𝑊)) = (1...(♯‘𝑊))
197194, 196eleqtrdi 2849 . . . . . . . 8 (𝜑𝐸 ∈ (1...(♯‘𝑊)))
198 pfxfv0 14333 . . . . . . . 8 ((𝑊 ∈ Word 𝐷𝐸 ∈ (1...(♯‘𝑊))) → ((𝑊 prefix 𝐸)‘0) = (𝑊‘0))
19917, 197, 198syl2anc 583 . . . . . . 7 (𝜑 → ((𝑊 prefix 𝐸)‘0) = (𝑊‘0))
200183, 192, 1993eqtrd 2782 . . . . . 6 (𝜑 → ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘0) = (𝑊‘0))
201200adantr 480 . . . . 5 ((𝜑𝐸 = (♯‘𝑊)) → ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘0) = (𝑊‘0))
202173, 175, 2013eqtrd 2782 . . . 4 ((𝜑𝐸 = (♯‘𝑊)) → ((𝑀𝑈)‘(𝑈𝐸)) = (𝑊‘0))
20333adantr 480 . . . 4 ((𝜑𝐸 = (♯‘𝑊)) → ((𝑀𝑈)‘(𝑈𝐸)) = ((𝑀𝑈)‘𝐼))
204164, 202, 2033eqtr2d 2784 . . 3 ((𝜑𝐸 = (♯‘𝑊)) → ((𝑀𝑊)‘𝐽) = ((𝑀𝑈)‘𝐼))
205 elfzr 13428 . . . 4 (𝐸 ∈ (0...(♯‘𝑊)) → (𝐸 ∈ (0..^(♯‘𝑊)) ∨ 𝐸 = (♯‘𝑊)))
20683, 205syl 17 . . 3 (𝜑 → (𝐸 ∈ (0..^(♯‘𝑊)) ∨ 𝐸 = (♯‘𝑊)))
207153, 204, 206mpjaodan 955 . 2 (𝜑 → ((𝑀𝑊)‘𝐽) = ((𝑀𝑈)‘𝐼))
2089, 207eqtrd 2778 1 (𝜑 → ((𝑀𝑊)‘((𝑀‘⟨“𝐼𝐽”⟩)‘𝐼)) = ((𝑀𝑈)‘𝐼))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wo 843   = wceq 1539  wcel 2108  wne 2942  {crab 3067  Vcvv 3422  cdif 3880  cop 4564  cotp 4566   class class class wbr 5070  ccnv 5579  dom cdm 5580  ran crn 5581  wf 6414  1-1wf1 6415  1-1-ontowf1o 6417  cfv 6418  (class class class)co 7255  0cc0 10802  1c1 10803   + caddc 10805   < clt 10940  cmin 11135  cn 11903  0cn0 12163  cz 12249  ...cfz 13168  ..^cfzo 13311  chash 13972  Word cword 14145   ++ cconcat 14201  ⟨“cs1 14228   substr csubstr 14281   prefix cpfx 14311   splice csplice 14390  ⟨“cs2 14482  Basecbs 16840  SymGrpcsymg 18889  toCycctocyc 31275
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879  ax-pre-sup 10880
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-ot 4567  df-uni 4837  df-int 4877  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-1st 7804  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-1o 8267  df-er 8456  df-map 8575  df-en 8692  df-dom 8693  df-sdom 8694  df-fin 8695  df-sup 9131  df-inf 9132  df-card 9628  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-div 11563  df-nn 11904  df-2 11966  df-3 11967  df-4 11968  df-5 11969  df-6 11970  df-7 11971  df-8 11972  df-9 11973  df-n0 12164  df-z 12250  df-uz 12512  df-rp 12660  df-fz 13169  df-fzo 13312  df-fl 13440  df-mod 13518  df-hash 13973  df-word 14146  df-concat 14202  df-s1 14229  df-substr 14282  df-pfx 14312  df-splice 14391  df-csh 14430  df-s2 14489  df-struct 16776  df-sets 16793  df-slot 16811  df-ndx 16823  df-base 16841  df-ress 16868  df-plusg 16901  df-tset 16907  df-efmnd 18423  df-symg 18890  df-tocyc 31276
This theorem is referenced by:  cycpmco2  31302
  Copyright terms: Public domain W3C validator