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 30779
Description: Lemma for cycpmco2 30783. (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 30776 . 2 (𝜑 → ((𝑀𝑊)‘((𝑀‘⟨“𝐼𝐽”⟩)‘𝐼)) = ((𝑀𝑊)‘𝐽))
103adantr 483 . . . . 5 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → 𝐷𝑉)
11 ssrab2 4035 . . . . . . . . 9 {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ⊆ Word 𝐷
12 eqid 2820 . . . . . . . . . . . . 13 (Base‘𝑆) = (Base‘𝑆)
131, 2, 12tocycf 30767 . . . . . . . . . . . 12 (𝐷𝑉𝑀:{𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}⟶(Base‘𝑆))
143, 13syl 17 . . . . . . . . . . 11 (𝜑𝑀:{𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}⟶(Base‘𝑆))
1514fdmd 6499 . . . . . . . . . 10 (𝜑 → dom 𝑀 = {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
164, 15eleqtrd 2913 . . . . . . . . 9 (𝜑𝑊 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
1711, 16sseldi 3944 . . . . . . . 8 (𝜑𝑊 ∈ Word 𝐷)
185eldifad 3925 . . . . . . . . 9 (𝜑𝐼𝐷)
1918s1cld 13937 . . . . . . . 8 (𝜑 → ⟨“𝐼”⟩ ∈ Word 𝐷)
20 splcl 14094 . . . . . . . 8 ((𝑊 ∈ Word 𝐷 ∧ ⟨“𝐼”⟩ ∈ Word 𝐷) → (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩) ∈ Word 𝐷)
2117, 19, 20syl2anc 586 . . . . . . 7 (𝜑 → (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩) ∈ Word 𝐷)
228, 21eqeltrid 2915 . . . . . 6 (𝜑𝑈 ∈ Word 𝐷)
2322adantr 483 . . . . 5 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → 𝑈 ∈ Word 𝐷)
241, 2, 3, 4, 5, 6, 7, 8cycpmco2f1 30774 . . . . . 6 (𝜑𝑈:dom 𝑈1-1𝐷)
2524adantr 483 . . . . 5 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → 𝑈:dom 𝑈1-1𝐷)
26 simpr 487 . . . . . 6 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → 𝐸 ∈ (0..^(♯‘𝑊)))
271, 2, 3, 4, 5, 6, 7, 8cycpmco2lem3 30778 . . . . . . . 8 (𝜑 → ((♯‘𝑈) − 1) = (♯‘𝑊))
2827oveq2d 7149 . . . . . . 7 (𝜑 → (0..^((♯‘𝑈) − 1)) = (0..^(♯‘𝑊)))
2928adantr 483 . . . . . 6 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (0..^((♯‘𝑈) − 1)) = (0..^(♯‘𝑊)))
3026, 29eleqtrrd 2914 . . . . 5 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → 𝐸 ∈ (0..^((♯‘𝑈) − 1)))
311, 10, 23, 25, 30cycpmfv1 30763 . . . 4 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑀𝑈)‘(𝑈𝐸)) = (𝑈‘(𝐸 + 1)))
321, 2, 3, 4, 5, 6, 7, 8cycpmco2lem2 30777 . . . . . 6 (𝜑 → (𝑈𝐸) = 𝐼)
3332fveq2d 6650 . . . . 5 (𝜑 → ((𝑀𝑈)‘(𝑈𝐸)) = ((𝑀𝑈)‘𝐼))
3433adantr 483 . . . 4 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑀𝑈)‘(𝑈𝐸)) = ((𝑀𝑈)‘𝐼))
3517adantr 483 . . . . . 6 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → 𝑊 ∈ Word 𝐷)
36 lencl 13865 . . . . . . . . 9 (𝑊 ∈ Word 𝐷 → (♯‘𝑊) ∈ ℕ0)
3717, 36syl 17 . . . . . . . 8 (𝜑 → (♯‘𝑊) ∈ ℕ0)
38 nn0fz0 12989 . . . . . . . 8 ((♯‘𝑊) ∈ ℕ0 ↔ (♯‘𝑊) ∈ (0...(♯‘𝑊)))
3937, 38sylib 220 . . . . . . 7 (𝜑 → (♯‘𝑊) ∈ (0...(♯‘𝑊)))
4039adantr 483 . . . . . 6 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (♯‘𝑊) ∈ (0...(♯‘𝑊)))
41 swrdfv0 13991 . . . . . 6 ((𝑊 ∈ Word 𝐷𝐸 ∈ (0..^(♯‘𝑊)) ∧ (♯‘𝑊) ∈ (0...(♯‘𝑊))) → ((𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)‘0) = (𝑊𝐸))
4235, 26, 40, 41syl3anc 1367 . . . . 5 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)‘0) = (𝑊𝐸))
43 ovexd 7168 . . . . . . . . . . 11 (𝜑 → ((𝑊𝐽) + 1) ∈ V)
447, 43eqeltrid 2915 . . . . . . . . . 10 (𝜑𝐸 ∈ V)
45 splval 14093 . . . . . . . . . 10 ((𝑊 ∈ dom 𝑀 ∧ (𝐸 ∈ V ∧ 𝐸 ∈ V ∧ ⟨“𝐼”⟩ ∈ Word 𝐷)) → (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩) = (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)))
464, 44, 44, 19, 45syl13anc 1368 . . . . . . . . 9 (𝜑 → (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩) = (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)))
478, 46syl5eq 2867 . . . . . . . 8 (𝜑𝑈 = (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)))
4847fveq1d 6648 . . . . . . 7 (𝜑 → (𝑈‘(𝐸 + 1)) = ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘(𝐸 + 1)))
4948adantr 483 . . . . . 6 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (𝑈‘(𝐸 + 1)) = ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘(𝐸 + 1)))
50 pfxcl 14019 . . . . . . . . . 10 (𝑊 ∈ Word 𝐷 → (𝑊 prefix 𝐸) ∈ Word 𝐷)
5117, 50syl 17 . . . . . . . . 9 (𝜑 → (𝑊 prefix 𝐸) ∈ Word 𝐷)
52 ccatcl 13906 . . . . . . . . 9 (((𝑊 prefix 𝐸) ∈ Word 𝐷 ∧ ⟨“𝐼”⟩ ∈ Word 𝐷) → ((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ∈ Word 𝐷)
5351, 19, 52syl2anc 586 . . . . . . . 8 (𝜑 → ((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ∈ Word 𝐷)
5453adantr 483 . . . . . . 7 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ∈ Word 𝐷)
55 swrdcl 13987 . . . . . . . . 9 (𝑊 ∈ Word 𝐷 → (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∈ Word 𝐷)
5617, 55syl 17 . . . . . . . 8 (𝜑 → (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∈ Word 𝐷)
5756adantr 483 . . . . . . 7 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∈ Word 𝐷)
58 1z 11991 . . . . . . . . . . 11 1 ∈ ℤ
59 fzoaddel 13074 . . . . . . . . . . 11 ((𝐸 ∈ (0..^(♯‘𝑊)) ∧ 1 ∈ ℤ) → (𝐸 + 1) ∈ ((0 + 1)..^((♯‘𝑊) + 1)))
6058, 59mpan2 689 . . . . . . . . . 10 (𝐸 ∈ (0..^(♯‘𝑊)) → (𝐸 + 1) ∈ ((0 + 1)..^((♯‘𝑊) + 1)))
61 elfzolt2b 13033 . . . . . . . . . 10 ((𝐸 + 1) ∈ ((0 + 1)..^((♯‘𝑊) + 1)) → (𝐸 + 1) ∈ ((𝐸 + 1)..^((♯‘𝑊) + 1)))
6260, 61syl 17 . . . . . . . . 9 (𝐸 ∈ (0..^(♯‘𝑊)) → (𝐸 + 1) ∈ ((𝐸 + 1)..^((♯‘𝑊) + 1)))
6362adantl 484 . . . . . . . 8 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (𝐸 + 1) ∈ ((𝐸 + 1)..^((♯‘𝑊) + 1)))
64 ccatws1len 13954 . . . . . . . . . . . 12 ((𝑊 prefix 𝐸) ∈ Word 𝐷 → (♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) = ((♯‘(𝑊 prefix 𝐸)) + 1))
6551, 64syl 17 . . . . . . . . . . 11 (𝜑 → (♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) = ((♯‘(𝑊 prefix 𝐸)) + 1))
66 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑊𝑤 = 𝑊)
67 dmeq 5748 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑊 → dom 𝑤 = dom 𝑊)
68 eqidd 2821 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑊𝐷 = 𝐷)
6966, 67, 68f1eq123d 6584 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑊 → (𝑤:dom 𝑤1-1𝐷𝑊:dom 𝑊1-1𝐷))
7069elrab3 3661 . . . . . . . . . . . . . . . . . . . . 21 (𝑊 ∈ Word 𝐷 → (𝑊 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ↔ 𝑊:dom 𝑊1-1𝐷))
7170biimpa 479 . . . . . . . . . . . . . . . . . . . 20 ((𝑊 ∈ Word 𝐷𝑊 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}) → 𝑊:dom 𝑊1-1𝐷)
7217, 16, 71syl2anc 586 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑊:dom 𝑊1-1𝐷)
73 f1cnv 6614 . . . . . . . . . . . . . . . . . . 19 (𝑊:dom 𝑊1-1𝐷𝑊:ran 𝑊1-1-onto→dom 𝑊)
7472, 73syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑊:ran 𝑊1-1-onto→dom 𝑊)
75 f1of 6591 . . . . . . . . . . . . . . . . . 18 (𝑊:ran 𝑊1-1-onto→dom 𝑊𝑊:ran 𝑊⟶dom 𝑊)
7674, 75syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑊:ran 𝑊⟶dom 𝑊)
7776, 6ffvelrnd 6828 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑊𝐽) ∈ dom 𝑊)
78 wrddm 13853 . . . . . . . . . . . . . . . . 17 (𝑊 ∈ Word 𝐷 → dom 𝑊 = (0..^(♯‘𝑊)))
7917, 78syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝑊 = (0..^(♯‘𝑊)))
8077, 79eleqtrd 2913 . . . . . . . . . . . . . . 15 (𝜑 → (𝑊𝐽) ∈ (0..^(♯‘𝑊)))
81 fzofzp1 13118 . . . . . . . . . . . . . . 15 ((𝑊𝐽) ∈ (0..^(♯‘𝑊)) → ((𝑊𝐽) + 1) ∈ (0...(♯‘𝑊)))
8280, 81syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝑊𝐽) + 1) ∈ (0...(♯‘𝑊)))
837, 82eqeltrid 2915 . . . . . . . . . . . . 13 (𝜑𝐸 ∈ (0...(♯‘𝑊)))
84 pfxlen 14025 . . . . . . . . . . . . 13 ((𝑊 ∈ Word 𝐷𝐸 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix 𝐸)) = 𝐸)
8517, 83, 84syl2anc 586 . . . . . . . . . . . 12 (𝜑 → (♯‘(𝑊 prefix 𝐸)) = 𝐸)
8685oveq1d 7148 . . . . . . . . . . 11 (𝜑 → ((♯‘(𝑊 prefix 𝐸)) + 1) = (𝐸 + 1))
8765, 86eqtrd 2855 . . . . . . . . . 10 (𝜑 → (♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) = (𝐸 + 1))
8887adantr 483 . . . . . . . . 9 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) = (𝐸 + 1))
8947fveq2d 6650 . . . . . . . . . . 11 (𝜑 → (♯‘𝑈) = (♯‘(((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))))
90 ccatlen 13907 . . . . . . . . . . . . . . 15 ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ∈ Word 𝐷 ∧ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∈ Word 𝐷) → (♯‘(((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))) = ((♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) + (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))))
9153, 56, 90syl2anc 586 . . . . . . . . . . . . . 14 (𝜑 → (♯‘(((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))) = ((♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) + (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))))
92 swrdlen 13989 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ Word 𝐷𝐸 ∈ (0...(♯‘𝑊)) ∧ (♯‘𝑊) ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)) = ((♯‘𝑊) − 𝐸))
9317, 83, 39, 92syl3anc 1367 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)) = ((♯‘𝑊) − 𝐸))
9487, 93oveq12d 7151 . . . . . . . . . . . . . 14 (𝜑 → ((♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) + (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))) = ((𝐸 + 1) + ((♯‘𝑊) − 𝐸)))
9589, 91, 943eqtrd 2859 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝑈) = ((𝐸 + 1) + ((♯‘𝑊) − 𝐸)))
96 fz0ssnn0 12986 . . . . . . . . . . . . . . . . . 18 (0...(♯‘𝑊)) ⊆ ℕ0
9796, 83sseldi 3944 . . . . . . . . . . . . . . . . 17 (𝜑𝐸 ∈ ℕ0)
9897nn0zd 12064 . . . . . . . . . . . . . . . 16 (𝜑𝐸 ∈ ℤ)
9998peano2zd 12069 . . . . . . . . . . . . . . 15 (𝜑 → (𝐸 + 1) ∈ ℤ)
10099zcnd 12067 . . . . . . . . . . . . . 14 (𝜑 → (𝐸 + 1) ∈ ℂ)
10137nn0cnd 11936 . . . . . . . . . . . . . 14 (𝜑 → (♯‘𝑊) ∈ ℂ)
10297nn0cnd 11936 . . . . . . . . . . . . . 14 (𝜑𝐸 ∈ ℂ)
103100, 101, 102addsubassd 10995 . . . . . . . . . . . . 13 (𝜑 → (((𝐸 + 1) + (♯‘𝑊)) − 𝐸) = ((𝐸 + 1) + ((♯‘𝑊) − 𝐸)))
104 1cnd 10614 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℂ)
105102, 104, 101addassd 10641 . . . . . . . . . . . . . 14 (𝜑 → ((𝐸 + 1) + (♯‘𝑊)) = (𝐸 + (1 + (♯‘𝑊))))
106105oveq1d 7148 . . . . . . . . . . . . 13 (𝜑 → (((𝐸 + 1) + (♯‘𝑊)) − 𝐸) = ((𝐸 + (1 + (♯‘𝑊))) − 𝐸))
10795, 103, 1063eqtr2d 2861 . . . . . . . . . . . 12 (𝜑 → (♯‘𝑈) = ((𝐸 + (1 + (♯‘𝑊))) − 𝐸))
108104, 101addcld 10638 . . . . . . . . . . . . 13 (𝜑 → (1 + (♯‘𝑊)) ∈ ℂ)
109102, 108pncan2d 10977 . . . . . . . . . . . 12 (𝜑 → ((𝐸 + (1 + (♯‘𝑊))) − 𝐸) = (1 + (♯‘𝑊)))
110104, 101addcomd 10820 . . . . . . . . . . . 12 (𝜑 → (1 + (♯‘𝑊)) = ((♯‘𝑊) + 1))
111107, 109, 1103eqtrd 2859 . . . . . . . . . . 11 (𝜑 → (♯‘𝑈) = ((♯‘𝑊) + 1))
11289, 111, 913eqtr3rd 2864 . . . . . . . . . 10 (𝜑 → ((♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) + (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))) = ((♯‘𝑊) + 1))
113112adantr 483 . . . . . . . . 9 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) + (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))) = ((♯‘𝑊) + 1))
11488, 113oveq12d 7151 . . . . . . . 8 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩))..^((♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) + (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)))) = ((𝐸 + 1)..^((♯‘𝑊) + 1)))
11563, 114eleqtrrd 2914 . . . . . . 7 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (𝐸 + 1) ∈ ((♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩))..^((♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) + (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)))))
116 ccatval2 13912 . . . . . . 7 ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ∈ Word 𝐷 ∧ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∈ Word 𝐷 ∧ (𝐸 + 1) ∈ ((♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩))..^((♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) + (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))))) → ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘(𝐸 + 1)) = ((𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)‘((𝐸 + 1) − (♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)))))
11754, 57, 115, 116syl3anc 1367 . . . . . 6 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘(𝐸 + 1)) = ((𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)‘((𝐸 + 1) − (♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)))))
11887oveq2d 7149 . . . . . . . . 9 (𝜑 → ((𝐸 + 1) − (♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩))) = ((𝐸 + 1) − (𝐸 + 1)))
119100subidd 10963 . . . . . . . . 9 (𝜑 → ((𝐸 + 1) − (𝐸 + 1)) = 0)
120118, 119eqtrd 2855 . . . . . . . 8 (𝜑 → ((𝐸 + 1) − (♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩))) = 0)
121120fveq2d 6650 . . . . . . 7 (𝜑 → ((𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)‘((𝐸 + 1) − (♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)))) = ((𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)‘0))
122121adantr 483 . . . . . 6 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)‘((𝐸 + 1) − (♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)))) = ((𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)‘0))
12349, 117, 1223eqtrd 2859 . . . . 5 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (𝑈‘(𝐸 + 1)) = ((𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)‘0))
1247fveq2i 6649 . . . . . . 7 (𝑊𝐸) = (𝑊‘((𝑊𝐽) + 1))
125124a1i 11 . . . . . 6 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (𝑊𝐸) = (𝑊‘((𝑊𝐽) + 1)))
12672adantr 483 . . . . . . 7 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → 𝑊:dom 𝑊1-1𝐷)
1277oveq1i 7143 . . . . . . . . . 10 (𝐸 − 1) = (((𝑊𝐽) + 1) − 1)
128 elfzonn0 13066 . . . . . . . . . . . . 13 ((𝑊𝐽) ∈ (0..^(♯‘𝑊)) → (𝑊𝐽) ∈ ℕ0)
12980, 128syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑊𝐽) ∈ ℕ0)
130129nn0cnd 11936 . . . . . . . . . . 11 (𝜑 → (𝑊𝐽) ∈ ℂ)
131130, 104pncand 10976 . . . . . . . . . 10 (𝜑 → (((𝑊𝐽) + 1) − 1) = (𝑊𝐽))
132127, 131syl5req 2868 . . . . . . . . 9 (𝜑 → (𝑊𝐽) = (𝐸 − 1))
133132adantr 483 . . . . . . . 8 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (𝑊𝐽) = (𝐸 − 1))
134 nn0p1gt0 11905 . . . . . . . . . . . . . 14 ((𝑊𝐽) ∈ ℕ0 → 0 < ((𝑊𝐽) + 1))
135129, 134syl 17 . . . . . . . . . . . . 13 (𝜑 → 0 < ((𝑊𝐽) + 1))
136135, 7breqtrrdi 5084 . . . . . . . . . . . 12 (𝜑 → 0 < 𝐸)
137136gt0ne0d 11182 . . . . . . . . . . 11 (𝜑𝐸 ≠ 0)
138137adantr 483 . . . . . . . . . 10 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → 𝐸 ≠ 0)
139 fzo1fzo0n0 13072 . . . . . . . . . 10 (𝐸 ∈ (1..^(♯‘𝑊)) ↔ (𝐸 ∈ (0..^(♯‘𝑊)) ∧ 𝐸 ≠ 0))
14026, 138, 139sylanbrc 585 . . . . . . . . 9 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → 𝐸 ∈ (1..^(♯‘𝑊)))
141 elfzo1elm1fzo0 13122 . . . . . . . . 9 (𝐸 ∈ (1..^(♯‘𝑊)) → (𝐸 − 1) ∈ (0..^((♯‘𝑊) − 1)))
142140, 141syl 17 . . . . . . . 8 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (𝐸 − 1) ∈ (0..^((♯‘𝑊) − 1)))
143133, 142eqeltrd 2911 . . . . . . 7 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (𝑊𝐽) ∈ (0..^((♯‘𝑊) − 1)))
1441, 10, 35, 126, 143cycpmfv1 30763 . . . . . 6 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑀𝑊)‘(𝑊‘(𝑊𝐽))) = (𝑊‘((𝑊𝐽) + 1)))
145 f1f1orn 6602 . . . . . . . . . 10 (𝑊:dom 𝑊1-1𝐷𝑊:dom 𝑊1-1-onto→ran 𝑊)
14672, 145syl 17 . . . . . . . . 9 (𝜑𝑊:dom 𝑊1-1-onto→ran 𝑊)
147 f1ocnvfv2 7011 . . . . . . . . 9 ((𝑊:dom 𝑊1-1-onto→ran 𝑊𝐽 ∈ ran 𝑊) → (𝑊‘(𝑊𝐽)) = 𝐽)
148146, 6, 147syl2anc 586 . . . . . . . 8 (𝜑 → (𝑊‘(𝑊𝐽)) = 𝐽)
149148fveq2d 6650 . . . . . . 7 (𝜑 → ((𝑀𝑊)‘(𝑊‘(𝑊𝐽))) = ((𝑀𝑊)‘𝐽))
150149adantr 483 . . . . . 6 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑀𝑊)‘(𝑊‘(𝑊𝐽))) = ((𝑀𝑊)‘𝐽))
151125, 144, 1503eqtr2rd 2862 . . . . 5 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑀𝑊)‘𝐽) = (𝑊𝐸))
15242, 123, 1513eqtr4d 2865 . . . 4 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → (𝑈‘(𝐸 + 1)) = ((𝑀𝑊)‘𝐽))
15331, 34, 1523eqtr3rd 2864 . . 3 ((𝜑𝐸 ∈ (0..^(♯‘𝑊))) → ((𝑀𝑊)‘𝐽) = ((𝑀𝑈)‘𝐼))
154149adantr 483 . . . . 5 ((𝜑𝐸 = (♯‘𝑊)) → ((𝑀𝑊)‘(𝑊‘(𝑊𝐽))) = ((𝑀𝑊)‘𝐽))
1553adantr 483 . . . . . 6 ((𝜑𝐸 = (♯‘𝑊)) → 𝐷𝑉)
15617adantr 483 . . . . . 6 ((𝜑𝐸 = (♯‘𝑊)) → 𝑊 ∈ Word 𝐷)
15772adantr 483 . . . . . 6 ((𝜑𝐸 = (♯‘𝑊)) → 𝑊:dom 𝑊1-1𝐷)
158136adantr 483 . . . . . . 7 ((𝜑𝐸 = (♯‘𝑊)) → 0 < 𝐸)
159 simpr 487 . . . . . . 7 ((𝜑𝐸 = (♯‘𝑊)) → 𝐸 = (♯‘𝑊))
160158, 159breqtrd 5068 . . . . . 6 ((𝜑𝐸 = (♯‘𝑊)) → 0 < (♯‘𝑊))
161 oveq1 7140 . . . . . . 7 (𝐸 = (♯‘𝑊) → (𝐸 − 1) = ((♯‘𝑊) − 1))
162132, 161sylan9eq 2875 . . . . . 6 ((𝜑𝐸 = (♯‘𝑊)) → (𝑊𝐽) = ((♯‘𝑊) − 1))
1631, 155, 156, 157, 160, 162cycpmfv2 30764 . . . . 5 ((𝜑𝐸 = (♯‘𝑊)) → ((𝑀𝑊)‘(𝑊‘(𝑊𝐽))) = (𝑊‘0))
164154, 163eqtr3d 2857 . . . 4 ((𝜑𝐸 = (♯‘𝑊)) → ((𝑀𝑊)‘𝐽) = (𝑊‘0))
16522adantr 483 . . . . . 6 ((𝜑𝐸 = (♯‘𝑊)) → 𝑈 ∈ Word 𝐷)
16624adantr 483 . . . . . 6 ((𝜑𝐸 = (♯‘𝑊)) → 𝑈:dom 𝑈1-1𝐷)
167 nn0p1gt0 11905 . . . . . . . . 9 ((♯‘𝑊) ∈ ℕ0 → 0 < ((♯‘𝑊) + 1))
16837, 167syl 17 . . . . . . . 8 (𝜑 → 0 < ((♯‘𝑊) + 1))
169168, 111breqtrrd 5070 . . . . . . 7 (𝜑 → 0 < (♯‘𝑈))
170169adantr 483 . . . . . 6 ((𝜑𝐸 = (♯‘𝑊)) → 0 < (♯‘𝑈))
17127adantr 483 . . . . . . 7 ((𝜑𝐸 = (♯‘𝑊)) → ((♯‘𝑈) − 1) = (♯‘𝑊))
172159, 171eqtr4d 2858 . . . . . 6 ((𝜑𝐸 = (♯‘𝑊)) → 𝐸 = ((♯‘𝑈) − 1))
1731, 155, 165, 166, 170, 172cycpmfv2 30764 . . . . 5 ((𝜑𝐸 = (♯‘𝑊)) → ((𝑀𝑈)‘(𝑈𝐸)) = (𝑈‘0))
17447fveq1d 6648 . . . . . 6 (𝜑 → (𝑈‘0) = ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘0))
175174adantr 483 . . . . 5 ((𝜑𝐸 = (♯‘𝑊)) → (𝑈‘0) = ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘0))
176 nn0p1nn 11915 . . . . . . . . . . 11 (𝐸 ∈ ℕ0 → (𝐸 + 1) ∈ ℕ)
17797, 176syl 17 . . . . . . . . . 10 (𝜑 → (𝐸 + 1) ∈ ℕ)
178 lbfzo0 13061 . . . . . . . . . 10 (0 ∈ (0..^(𝐸 + 1)) ↔ (𝐸 + 1) ∈ ℕ)
179177, 178sylibr 236 . . . . . . . . 9 (𝜑 → 0 ∈ (0..^(𝐸 + 1)))
18087oveq2d 7149 . . . . . . . . 9 (𝜑 → (0..^(♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩))) = (0..^(𝐸 + 1)))
181179, 180eleqtrrd 2914 . . . . . . . 8 (𝜑 → 0 ∈ (0..^(♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩))))
182 ccatval1 13910 . . . . . . . 8 ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ∈ Word 𝐷 ∧ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∈ Word 𝐷 ∧ 0 ∈ (0..^(♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)))) → ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘0) = (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)‘0))
18353, 56, 181, 182syl3anc 1367 . . . . . . 7 (𝜑 → ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘0) = (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)‘0))
184 nn0p1nn 11915 . . . . . . . . . . . 12 ((𝑊𝐽) ∈ ℕ0 → ((𝑊𝐽) + 1) ∈ ℕ)
185129, 184syl 17 . . . . . . . . . . 11 (𝜑 → ((𝑊𝐽) + 1) ∈ ℕ)
1867, 185eqeltrid 2915 . . . . . . . . . 10 (𝜑𝐸 ∈ ℕ)
187 lbfzo0 13061 . . . . . . . . . 10 (0 ∈ (0..^𝐸) ↔ 𝐸 ∈ ℕ)
188186, 187sylibr 236 . . . . . . . . 9 (𝜑 → 0 ∈ (0..^𝐸))
18985oveq2d 7149 . . . . . . . . 9 (𝜑 → (0..^(♯‘(𝑊 prefix 𝐸))) = (0..^𝐸))
190188, 189eleqtrrd 2914 . . . . . . . 8 (𝜑 → 0 ∈ (0..^(♯‘(𝑊 prefix 𝐸))))
191 ccatval1 13910 . . . . . . . 8 (((𝑊 prefix 𝐸) ∈ Word 𝐷 ∧ ⟨“𝐼”⟩ ∈ Word 𝐷 ∧ 0 ∈ (0..^(♯‘(𝑊 prefix 𝐸)))) → (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)‘0) = ((𝑊 prefix 𝐸)‘0))
19251, 19, 190, 191syl3anc 1367 . . . . . . 7 (𝜑 → (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)‘0) = ((𝑊 prefix 𝐸)‘0))
193 fzne1 30498 . . . . . . . . . 10 ((𝐸 ∈ (0...(♯‘𝑊)) ∧ 𝐸 ≠ 0) → 𝐸 ∈ ((0 + 1)...(♯‘𝑊)))
19483, 137, 193syl2anc 586 . . . . . . . . 9 (𝜑𝐸 ∈ ((0 + 1)...(♯‘𝑊)))
195 0p1e1 11738 . . . . . . . . . 10 (0 + 1) = 1
196195oveq1i 7143 . . . . . . . . 9 ((0 + 1)...(♯‘𝑊)) = (1...(♯‘𝑊))
197194, 196eleqtrdi 2921 . . . . . . . 8 (𝜑𝐸 ∈ (1...(♯‘𝑊)))
198 pfxfv0 14034 . . . . . . . 8 ((𝑊 ∈ Word 𝐷𝐸 ∈ (1...(♯‘𝑊))) → ((𝑊 prefix 𝐸)‘0) = (𝑊‘0))
19917, 197, 198syl2anc 586 . . . . . . 7 (𝜑 → ((𝑊 prefix 𝐸)‘0) = (𝑊‘0))
200183, 192, 1993eqtrd 2859 . . . . . 6 (𝜑 → ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘0) = (𝑊‘0))
201200adantr 483 . . . . 5 ((𝜑𝐸 = (♯‘𝑊)) → ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘0) = (𝑊‘0))
202173, 175, 2013eqtrd 2859 . . . 4 ((𝜑𝐸 = (♯‘𝑊)) → ((𝑀𝑈)‘(𝑈𝐸)) = (𝑊‘0))
20333adantr 483 . . . 4 ((𝜑𝐸 = (♯‘𝑊)) → ((𝑀𝑈)‘(𝑈𝐸)) = ((𝑀𝑈)‘𝐼))
204164, 202, 2033eqtr2d 2861 . . 3 ((𝜑𝐸 = (♯‘𝑊)) → ((𝑀𝑊)‘𝐽) = ((𝑀𝑈)‘𝐼))
205 elfzr 13134 . . . 4 (𝐸 ∈ (0...(♯‘𝑊)) → (𝐸 ∈ (0..^(♯‘𝑊)) ∨ 𝐸 = (♯‘𝑊)))
20683, 205syl 17 . . 3 (𝜑 → (𝐸 ∈ (0..^(♯‘𝑊)) ∨ 𝐸 = (♯‘𝑊)))
207153, 204, 206mpjaodan 955 . 2 (𝜑 → ((𝑀𝑊)‘𝐽) = ((𝑀𝑈)‘𝐼))
2089, 207eqtrd 2855 1 (𝜑 → ((𝑀𝑊)‘((𝑀‘⟨“𝐼𝐽”⟩)‘𝐼)) = ((𝑀𝑈)‘𝐼))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  wo 843   = wceq 1537  wcel 2114  wne 3006  {crab 3129  Vcvv 3473  cdif 3910  cop 4549  cotp 4551   class class class wbr 5042  ccnv 5530  dom cdm 5531  ran crn 5532  wf 6327  1-1wf1 6328  1-1-ontowf1o 6330  cfv 6331  (class class class)co 7133  0cc0 10515  1c1 10516   + caddc 10518   < clt 10653  cmin 10848  cn 11616  0cn0 11876  cz 11960  ...cfz 12876  ..^cfzo 13017  chash 13675  Word cword 13846   ++ cconcat 13902  ⟨“cs1 13929   substr csubstr 13982   prefix cpfx 14012   splice csplice 14091  ⟨“cs2 14183  Basecbs 16462  SymGrpcsymg 18474  toCycctocyc 30756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439  ax-cnex 10571  ax-resscn 10572  ax-1cn 10573  ax-icn 10574  ax-addcl 10575  ax-addrcl 10576  ax-mulcl 10577  ax-mulrcl 10578  ax-mulcom 10579  ax-addass 10580  ax-mulass 10581  ax-distr 10582  ax-i2m1 10583  ax-1ne0 10584  ax-1rid 10585  ax-rnegex 10586  ax-rrecex 10587  ax-cnre 10588  ax-pre-lttri 10589  ax-pre-lttrn 10590  ax-pre-ltadd 10591  ax-pre-mulgt0 10592  ax-pre-sup 10593
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-nel 3111  df-ral 3130  df-rex 3131  df-reu 3132  df-rmo 3133  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-tp 4548  df-op 4550  df-ot 4552  df-uni 4815  df-int 4853  df-iun 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5436  df-eprel 5441  df-po 5450  df-so 5451  df-fr 5490  df-we 5492  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-riota 7091  df-ov 7136  df-oprab 7137  df-mpo 7138  df-om 7559  df-1st 7667  df-2nd 7668  df-wrecs 7925  df-recs 7986  df-rdg 8024  df-1o 8080  df-oadd 8084  df-er 8267  df-map 8386  df-en 8488  df-dom 8489  df-sdom 8490  df-fin 8491  df-sup 8884  df-inf 8885  df-card 9346  df-pnf 10655  df-mnf 10656  df-xr 10657  df-ltxr 10658  df-le 10659  df-sub 10850  df-neg 10851  df-div 11276  df-nn 11617  df-2 11679  df-3 11680  df-4 11681  df-5 11682  df-6 11683  df-7 11684  df-8 11685  df-9 11686  df-n0 11877  df-z 11961  df-uz 12223  df-rp 12369  df-fz 12877  df-fzo 13018  df-fl 13146  df-mod 13222  df-hash 13676  df-word 13847  df-concat 13903  df-s1 13930  df-substr 13983  df-pfx 14013  df-splice 14092  df-csh 14131  df-s2 14190  df-struct 16464  df-ndx 16465  df-slot 16466  df-base 16468  df-sets 16469  df-ress 16470  df-plusg 16557  df-tset 16563  df-efmnd 18013  df-symg 18475  df-tocyc 30757
This theorem is referenced by:  cycpmco2  30783
  Copyright terms: Public domain W3C validator