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

Theorem cycpmco2lem5 30765
Description: Lemma for cycpmco2 30768. (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 ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)
cycpmco2lem.1 (𝜑𝐾 ∈ ran 𝑊)
cycpmco2lem5.1 (𝜑 → (𝑈𝐾) = ((♯‘𝑈) − 1))
Assertion
Ref Expression
cycpmco2lem5 (𝜑 → ((𝑀𝑈)‘𝐾) = ((𝑀𝑊)‘𝐾))

Proof of Theorem cycpmco2lem5
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 cycpmco2lem.1 . . . . 5 (𝜑𝐾 ∈ ran 𝑊)
21adantr 483 . . . 4 ((𝜑 ∧ (♯‘𝑊) = 𝐸) → 𝐾 ∈ ran 𝑊)
3 cycpmco2.1 . . . . . . . . . . . . . . 15 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)
4 cycpmco2.w . . . . . . . . . . . . . . . 16 (𝜑𝑊 ∈ dom 𝑀)
5 cycpmco2.e . . . . . . . . . . . . . . . . 17 𝐸 = ((𝑊𝐽) + 1)
6 ovexd 7183 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑊𝐽) + 1) ∈ V)
75, 6eqeltrid 2915 . . . . . . . . . . . . . . . 16 (𝜑𝐸 ∈ V)
8 cycpmco2.i . . . . . . . . . . . . . . . . . 18 (𝜑𝐼 ∈ (𝐷 ∖ ran 𝑊))
98eldifad 3946 . . . . . . . . . . . . . . . . 17 (𝜑𝐼𝐷)
109s1cld 13949 . . . . . . . . . . . . . . . 16 (𝜑 → ⟨“𝐼”⟩ ∈ Word 𝐷)
11 splval 14105 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ dom 𝑀 ∧ (𝐸 ∈ V ∧ 𝐸 ∈ V ∧ ⟨“𝐼”⟩ ∈ Word 𝐷)) → (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩) = (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)))
124, 7, 7, 10, 11syl13anc 1367 . . . . . . . . . . . . . . 15 (𝜑 → (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩) = (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)))
133, 12syl5eq 2866 . . . . . . . . . . . . . 14 (𝜑𝑈 = (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)))
1413fveq2d 6667 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝑈) = (♯‘(((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))))
15 ssrab2 4054 . . . . . . . . . . . . . . . . 17 {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ⊆ Word 𝐷
16 cycpmco2.d . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐷𝑉)
17 cycpmco2.c . . . . . . . . . . . . . . . . . . . . 21 𝑀 = (toCyc‘𝐷)
18 cycpmco2.s . . . . . . . . . . . . . . . . . . . . 21 𝑆 = (SymGrp‘𝐷)
19 eqid 2819 . . . . . . . . . . . . . . . . . . . . 21 (Base‘𝑆) = (Base‘𝑆)
2017, 18, 19tocycf 30752 . . . . . . . . . . . . . . . . . . . 20 (𝐷𝑉𝑀:{𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}⟶(Base‘𝑆))
2116, 20syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀:{𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}⟶(Base‘𝑆))
2221fdmd 6516 . . . . . . . . . . . . . . . . . 18 (𝜑 → dom 𝑀 = {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
234, 22eleqtrd 2913 . . . . . . . . . . . . . . . . 17 (𝜑𝑊 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
2415, 23sseldi 3963 . . . . . . . . . . . . . . . 16 (𝜑𝑊 ∈ Word 𝐷)
25 pfxcl 14031 . . . . . . . . . . . . . . . 16 (𝑊 ∈ Word 𝐷 → (𝑊 prefix 𝐸) ∈ Word 𝐷)
2624, 25syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑊 prefix 𝐸) ∈ Word 𝐷)
27 ccatcl 13918 . . . . . . . . . . . . . . 15 (((𝑊 prefix 𝐸) ∈ Word 𝐷 ∧ ⟨“𝐼”⟩ ∈ Word 𝐷) → ((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ∈ Word 𝐷)
2826, 10, 27syl2anc 586 . . . . . . . . . . . . . 14 (𝜑 → ((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ∈ Word 𝐷)
29 swrdcl 13999 . . . . . . . . . . . . . . 15 (𝑊 ∈ Word 𝐷 → (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∈ Word 𝐷)
3024, 29syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∈ Word 𝐷)
31 ccatlen 13919 . . . . . . . . . . . . . 14 ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ∈ Word 𝐷 ∧ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∈ Word 𝐷) → (♯‘(((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))) = ((♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) + (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))))
3228, 30, 31syl2anc 586 . . . . . . . . . . . . 13 (𝜑 → (♯‘(((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))) = ((♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) + (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))))
33 ccatws1len 13966 . . . . . . . . . . . . . . . 16 ((𝑊 prefix 𝐸) ∈ Word 𝐷 → (♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) = ((♯‘(𝑊 prefix 𝐸)) + 1))
3426, 33syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) = ((♯‘(𝑊 prefix 𝐸)) + 1))
35 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = 𝑊𝑤 = 𝑊)
36 dmeq 5765 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = 𝑊 → dom 𝑤 = dom 𝑊)
37 eqidd 2820 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = 𝑊𝐷 = 𝐷)
3835, 36, 37f1eq123d 6601 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = 𝑊 → (𝑤:dom 𝑤1-1𝐷𝑊:dom 𝑊1-1𝐷))
3938elrab 3678 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑊 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ↔ (𝑊 ∈ Word 𝐷𝑊:dom 𝑊1-1𝐷))
4023, 39sylib 220 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑊 ∈ Word 𝐷𝑊:dom 𝑊1-1𝐷))
4140simprd 498 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑊:dom 𝑊1-1𝐷)
42 f1cnv 6631 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑊:dom 𝑊1-1𝐷𝑊:ran 𝑊1-1-onto→dom 𝑊)
4341, 42syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑊:ran 𝑊1-1-onto→dom 𝑊)
44 f1of 6608 . . . . . . . . . . . . . . . . . . . . . 22 (𝑊:ran 𝑊1-1-onto→dom 𝑊𝑊:ran 𝑊⟶dom 𝑊)
4543, 44syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑊:ran 𝑊⟶dom 𝑊)
46 cycpmco2.j . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐽 ∈ ran 𝑊)
4745, 46ffvelrnd 6845 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑊𝐽) ∈ dom 𝑊)
48 wrddm 13860 . . . . . . . . . . . . . . . . . . . . 21 (𝑊 ∈ Word 𝐷 → dom 𝑊 = (0..^(♯‘𝑊)))
4924, 48syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → dom 𝑊 = (0..^(♯‘𝑊)))
5047, 49eleqtrd 2913 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑊𝐽) ∈ (0..^(♯‘𝑊)))
51 fzofzp1 13126 . . . . . . . . . . . . . . . . . . 19 ((𝑊𝐽) ∈ (0..^(♯‘𝑊)) → ((𝑊𝐽) + 1) ∈ (0...(♯‘𝑊)))
5250, 51syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑊𝐽) + 1) ∈ (0...(♯‘𝑊)))
535, 52eqeltrid 2915 . . . . . . . . . . . . . . . . 17 (𝜑𝐸 ∈ (0...(♯‘𝑊)))
54 pfxlen 14037 . . . . . . . . . . . . . . . . 17 ((𝑊 ∈ Word 𝐷𝐸 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix 𝐸)) = 𝐸)
5524, 53, 54syl2anc 586 . . . . . . . . . . . . . . . 16 (𝜑 → (♯‘(𝑊 prefix 𝐸)) = 𝐸)
5655oveq1d 7163 . . . . . . . . . . . . . . 15 (𝜑 → ((♯‘(𝑊 prefix 𝐸)) + 1) = (𝐸 + 1))
5734, 56eqtrd 2854 . . . . . . . . . . . . . 14 (𝜑 → (♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) = (𝐸 + 1))
58 lencl 13875 . . . . . . . . . . . . . . . . 17 (𝑊 ∈ Word 𝐷 → (♯‘𝑊) ∈ ℕ0)
5924, 58syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (♯‘𝑊) ∈ ℕ0)
60 nn0fz0 12997 . . . . . . . . . . . . . . . 16 ((♯‘𝑊) ∈ ℕ0 ↔ (♯‘𝑊) ∈ (0...(♯‘𝑊)))
6159, 60sylib 220 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘𝑊) ∈ (0...(♯‘𝑊)))
62 swrdlen 14001 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Word 𝐷𝐸 ∈ (0...(♯‘𝑊)) ∧ (♯‘𝑊) ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)) = ((♯‘𝑊) − 𝐸))
6324, 53, 61, 62syl3anc 1366 . . . . . . . . . . . . . 14 (𝜑 → (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)) = ((♯‘𝑊) − 𝐸))
6457, 63oveq12d 7166 . . . . . . . . . . . . 13 (𝜑 → ((♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)) + (♯‘(𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))) = ((𝐸 + 1) + ((♯‘𝑊) − 𝐸)))
6514, 32, 643eqtrd 2858 . . . . . . . . . . . 12 (𝜑 → (♯‘𝑈) = ((𝐸 + 1) + ((♯‘𝑊) − 𝐸)))
66 fz0ssnn0 12994 . . . . . . . . . . . . . . . . 17 (0...(♯‘𝑊)) ⊆ ℕ0
6766, 53sseldi 3963 . . . . . . . . . . . . . . . 16 (𝜑𝐸 ∈ ℕ0)
6867nn0zd 12077 . . . . . . . . . . . . . . 15 (𝜑𝐸 ∈ ℤ)
6968peano2zd 12082 . . . . . . . . . . . . . 14 (𝜑 → (𝐸 + 1) ∈ ℤ)
7069zcnd 12080 . . . . . . . . . . . . 13 (𝜑 → (𝐸 + 1) ∈ ℂ)
7159nn0cnd 11949 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝑊) ∈ ℂ)
7267nn0cnd 11949 . . . . . . . . . . . . 13 (𝜑𝐸 ∈ ℂ)
7370, 71, 72addsubassd 11009 . . . . . . . . . . . 12 (𝜑 → (((𝐸 + 1) + (♯‘𝑊)) − 𝐸) = ((𝐸 + 1) + ((♯‘𝑊) − 𝐸)))
74 1cnd 10628 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℂ)
7572, 74, 71addassd 10655 . . . . . . . . . . . . 13 (𝜑 → ((𝐸 + 1) + (♯‘𝑊)) = (𝐸 + (1 + (♯‘𝑊))))
7675oveq1d 7163 . . . . . . . . . . . 12 (𝜑 → (((𝐸 + 1) + (♯‘𝑊)) − 𝐸) = ((𝐸 + (1 + (♯‘𝑊))) − 𝐸))
7765, 73, 763eqtr2d 2860 . . . . . . . . . . 11 (𝜑 → (♯‘𝑈) = ((𝐸 + (1 + (♯‘𝑊))) − 𝐸))
7874, 71addcld 10652 . . . . . . . . . . . 12 (𝜑 → (1 + (♯‘𝑊)) ∈ ℂ)
7972, 78pncan2d 10991 . . . . . . . . . . 11 (𝜑 → ((𝐸 + (1 + (♯‘𝑊))) − 𝐸) = (1 + (♯‘𝑊)))
8074, 71addcomd 10834 . . . . . . . . . . 11 (𝜑 → (1 + (♯‘𝑊)) = ((♯‘𝑊) + 1))
8177, 79, 803eqtrd 2858 . . . . . . . . . 10 (𝜑 → (♯‘𝑈) = ((♯‘𝑊) + 1))
82 oveq1 7155 . . . . . . . . . 10 ((♯‘𝑊) = 𝐸 → ((♯‘𝑊) + 1) = (𝐸 + 1))
8381, 82sylan9eq 2874 . . . . . . . . 9 ((𝜑 ∧ (♯‘𝑊) = 𝐸) → (♯‘𝑈) = (𝐸 + 1))
8483oveq1d 7163 . . . . . . . 8 ((𝜑 ∧ (♯‘𝑊) = 𝐸) → ((♯‘𝑈) − 1) = ((𝐸 + 1) − 1))
8572, 74pncand 10990 . . . . . . . . 9 (𝜑 → ((𝐸 + 1) − 1) = 𝐸)
8685adantr 483 . . . . . . . 8 ((𝜑 ∧ (♯‘𝑊) = 𝐸) → ((𝐸 + 1) − 1) = 𝐸)
8784, 86eqtrd 2854 . . . . . . 7 ((𝜑 ∧ (♯‘𝑊) = 𝐸) → ((♯‘𝑈) − 1) = 𝐸)
8887fveq2d 6667 . . . . . 6 ((𝜑 ∧ (♯‘𝑊) = 𝐸) → (𝑈‘((♯‘𝑈) − 1)) = (𝑈𝐸))
89 cycpmco2lem5.1 . . . . . . . . 9 (𝜑 → (𝑈𝐾) = ((♯‘𝑈) − 1))
9089fveq2d 6667 . . . . . . . 8 (𝜑 → (𝑈‘(𝑈𝐾)) = (𝑈‘((♯‘𝑈) − 1)))
9117, 18, 16, 4, 8, 46, 5, 3cycpmco2f1 30759 . . . . . . . . . . 11 (𝜑𝑈:dom 𝑈1-1𝐷)
92 f1f1orn 6619 . . . . . . . . . . 11 (𝑈:dom 𝑈1-1𝐷𝑈:dom 𝑈1-1-onto→ran 𝑈)
9391, 92syl 17 . . . . . . . . . 10 (𝜑𝑈:dom 𝑈1-1-onto→ran 𝑈)
94 ssun1 4146 . . . . . . . . . . . 12 ran 𝑊 ⊆ (ran 𝑊 ∪ {𝐼})
9517, 18, 16, 4, 8, 46, 5, 3cycpmco2rn 30760 . . . . . . . . . . . 12 (𝜑 → ran 𝑈 = (ran 𝑊 ∪ {𝐼}))
9694, 95sseqtrrid 4018 . . . . . . . . . . 11 (𝜑 → ran 𝑊 ⊆ ran 𝑈)
9796sselda 3965 . . . . . . . . . 10 ((𝜑𝐾 ∈ ran 𝑊) → 𝐾 ∈ ran 𝑈)
98 f1ocnvfv2 7026 . . . . . . . . . 10 ((𝑈:dom 𝑈1-1-onto→ran 𝑈𝐾 ∈ ran 𝑈) → (𝑈‘(𝑈𝐾)) = 𝐾)
9993, 97, 98syl2an2r 683 . . . . . . . . 9 ((𝜑𝐾 ∈ ran 𝑊) → (𝑈‘(𝑈𝐾)) = 𝐾)
1001, 99mpdan 685 . . . . . . . 8 (𝜑 → (𝑈‘(𝑈𝐾)) = 𝐾)
10190, 100eqtr3d 2856 . . . . . . 7 (𝜑 → (𝑈‘((♯‘𝑈) − 1)) = 𝐾)
102101adantr 483 . . . . . 6 ((𝜑 ∧ (♯‘𝑊) = 𝐸) → (𝑈‘((♯‘𝑈) − 1)) = 𝐾)
10317, 18, 16, 4, 8, 46, 5, 3cycpmco2lem2 30762 . . . . . . 7 (𝜑 → (𝑈𝐸) = 𝐼)
104103adantr 483 . . . . . 6 ((𝜑 ∧ (♯‘𝑊) = 𝐸) → (𝑈𝐸) = 𝐼)
10588, 102, 1043eqtr3d 2862 . . . . 5 ((𝜑 ∧ (♯‘𝑊) = 𝐸) → 𝐾 = 𝐼)
1068eldifbd 3947 . . . . . 6 (𝜑 → ¬ 𝐼 ∈ ran 𝑊)
107106adantr 483 . . . . 5 ((𝜑 ∧ (♯‘𝑊) = 𝐸) → ¬ 𝐼 ∈ ran 𝑊)
108105, 107eqneltrd 2930 . . . 4 ((𝜑 ∧ (♯‘𝑊) = 𝐸) → ¬ 𝐾 ∈ ran 𝑊)
1092, 108pm2.21dd 197 . . 3 ((𝜑 ∧ (♯‘𝑊) = 𝐸) → ((𝑀𝑈)‘(𝑈‘((♯‘𝑈) − 1))) = ((𝑀𝑊)‘(𝑈‘((♯‘𝑈) − 1))))
110 splcl 14106 . . . . . . . 8 ((𝑊 ∈ Word 𝐷 ∧ ⟨“𝐼”⟩ ∈ Word 𝐷) → (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩) ∈ Word 𝐷)
11124, 10, 110syl2anc 586 . . . . . . 7 (𝜑 → (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩) ∈ Word 𝐷)
1123, 111eqeltrid 2915 . . . . . 6 (𝜑𝑈 ∈ Word 𝐷)
113 nn0p1gt0 11918 . . . . . . . 8 ((♯‘𝑊) ∈ ℕ0 → 0 < ((♯‘𝑊) + 1))
11459, 113syl 17 . . . . . . 7 (𝜑 → 0 < ((♯‘𝑊) + 1))
115114, 81breqtrrd 5085 . . . . . 6 (𝜑 → 0 < (♯‘𝑈))
116 eqidd 2820 . . . . . 6 (𝜑 → ((♯‘𝑈) − 1) = ((♯‘𝑈) − 1))
11717, 16, 112, 91, 115, 116cycpmfv2 30749 . . . . 5 (𝜑 → ((𝑀𝑈)‘(𝑈‘((♯‘𝑈) − 1))) = (𝑈‘0))
118117adantr 483 . . . 4 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → ((𝑀𝑈)‘(𝑈‘((♯‘𝑈) − 1))) = (𝑈‘0))
119 f1f 6568 . . . . . . . . . . . 12 (𝑊:dom 𝑊1-1𝐷𝑊:dom 𝑊𝐷)
12041, 119syl 17 . . . . . . . . . . 11 (𝜑𝑊:dom 𝑊𝐷)
121120frnd 6514 . . . . . . . . . 10 (𝜑 → ran 𝑊𝐷)
12216, 121ssexd 5219 . . . . . . . . 9 (𝜑 → ran 𝑊 ∈ V)
12346ne0d 4299 . . . . . . . . 9 (𝜑 → ran 𝑊 ≠ ∅)
124 hashgt0 13741 . . . . . . . . 9 ((ran 𝑊 ∈ V ∧ ran 𝑊 ≠ ∅) → 0 < (♯‘ran 𝑊))
125122, 123, 124syl2anc 586 . . . . . . . 8 (𝜑 → 0 < (♯‘ran 𝑊))
1264dmexd 7607 . . . . . . . . 9 (𝜑 → dom 𝑊 ∈ V)
127 hashf1rn 13705 . . . . . . . . 9 ((dom 𝑊 ∈ V ∧ 𝑊:dom 𝑊1-1𝐷) → (♯‘𝑊) = (♯‘ran 𝑊))
128126, 41, 127syl2anc 586 . . . . . . . 8 (𝜑 → (♯‘𝑊) = (♯‘ran 𝑊))
129125, 128breqtrrd 5085 . . . . . . 7 (𝜑 → 0 < (♯‘𝑊))
130 eqidd 2820 . . . . . . 7 (𝜑 → ((♯‘𝑊) − 1) = ((♯‘𝑊) − 1))
13117, 16, 24, 41, 129, 130cycpmfv2 30749 . . . . . 6 (𝜑 → ((𝑀𝑊)‘(𝑊‘((♯‘𝑊) − 1))) = (𝑊‘0))
132131adantr 483 . . . . 5 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → ((𝑀𝑊)‘(𝑊‘((♯‘𝑊) − 1))) = (𝑊‘0))
1333a1i 11 . . . . . . . 8 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩))
13417, 18, 16, 4, 8, 46, 5, 3cycpmco2lem3 30763 . . . . . . . . . 10 (𝜑 → ((♯‘𝑈) − 1) = (♯‘𝑊))
13572, 74addcomd 10834 . . . . . . . . . . . 12 (𝜑 → (𝐸 + 1) = (1 + 𝐸))
136135oveq2d 7164 . . . . . . . . . . 11 (𝜑 → ((((♯‘𝑊) − 1) − 𝐸) + (𝐸 + 1)) = ((((♯‘𝑊) − 1) − 𝐸) + (1 + 𝐸)))
13771, 74subcld 10989 . . . . . . . . . . . 12 (𝜑 → ((♯‘𝑊) − 1) ∈ ℂ)
138137, 72, 74nppcan3d 11016 . . . . . . . . . . 11 (𝜑 → ((((♯‘𝑊) − 1) − 𝐸) + (1 + 𝐸)) = (((♯‘𝑊) − 1) + 1))
13971, 74npcand 10993 . . . . . . . . . . 11 (𝜑 → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊))
140136, 138, 1393eqtrd 2858 . . . . . . . . . 10 (𝜑 → ((((♯‘𝑊) − 1) − 𝐸) + (𝐸 + 1)) = (♯‘𝑊))
141134, 140eqtr4d 2857 . . . . . . . . 9 (𝜑 → ((♯‘𝑈) − 1) = ((((♯‘𝑊) − 1) − 𝐸) + (𝐸 + 1)))
142141adantr 483 . . . . . . . 8 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → ((♯‘𝑈) − 1) = ((((♯‘𝑊) − 1) − 𝐸) + (𝐸 + 1)))
143133, 142fveq12d 6670 . . . . . . 7 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → (𝑈‘((♯‘𝑈) − 1)) = ((𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)‘((((♯‘𝑊) − 1) − 𝐸) + (𝐸 + 1))))
14424adantr 483 . . . . . . . 8 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → 𝑊 ∈ Word 𝐷)
145 nn0fz0 12997 . . . . . . . . . 10 (𝐸 ∈ ℕ0𝐸 ∈ (0...𝐸))
14667, 145sylib 220 . . . . . . . . 9 (𝜑𝐸 ∈ (0...𝐸))
147146adantr 483 . . . . . . . 8 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → 𝐸 ∈ (0...𝐸))
14853adantr 483 . . . . . . . 8 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → 𝐸 ∈ (0...(♯‘𝑊)))
14910adantr 483 . . . . . . . 8 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → ⟨“𝐼”⟩ ∈ Word 𝐷)
15071adantr 483 . . . . . . . . . 10 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → (♯‘𝑊) ∈ ℂ)
151 1cnd 10628 . . . . . . . . . 10 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → 1 ∈ ℂ)
15272adantr 483 . . . . . . . . . 10 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → 𝐸 ∈ ℂ)
153150, 151, 152sub32d 11021 . . . . . . . . 9 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → (((♯‘𝑊) − 1) − 𝐸) = (((♯‘𝑊) − 𝐸) − 1))
154 fznn0sub 12931 . . . . . . . . . . . . 13 (𝐸 ∈ (0...(♯‘𝑊)) → ((♯‘𝑊) − 𝐸) ∈ ℕ0)
15553, 154syl 17 . . . . . . . . . . . 12 (𝜑 → ((♯‘𝑊) − 𝐸) ∈ ℕ0)
156155adantr 483 . . . . . . . . . . 11 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → ((♯‘𝑊) − 𝐸) ∈ ℕ0)
157 simpr 487 . . . . . . . . . . 11 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → (♯‘𝑊) ≠ 𝐸)
158150, 152, 156, 157subne0nn 30530 . . . . . . . . . 10 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → ((♯‘𝑊) − 𝐸) ∈ ℕ)
159 fzo0end 13121 . . . . . . . . . 10 (((♯‘𝑊) − 𝐸) ∈ ℕ → (((♯‘𝑊) − 𝐸) − 1) ∈ (0..^((♯‘𝑊) − 𝐸)))
160158, 159syl 17 . . . . . . . . 9 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → (((♯‘𝑊) − 𝐸) − 1) ∈ (0..^((♯‘𝑊) − 𝐸)))
161153, 160eqeltrd 2911 . . . . . . . 8 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → (((♯‘𝑊) − 1) − 𝐸) ∈ (0..^((♯‘𝑊) − 𝐸)))
162 s1len 13952 . . . . . . . . . . 11 (♯‘⟨“𝐼”⟩) = 1
163162eqcomi 2828 . . . . . . . . . 10 1 = (♯‘⟨“𝐼”⟩)
164163oveq2i 7159 . . . . . . . . 9 (𝐸 + 1) = (𝐸 + (♯‘⟨“𝐼”⟩))
165164a1i 11 . . . . . . . 8 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → (𝐸 + 1) = (𝐸 + (♯‘⟨“𝐼”⟩)))
166144, 147, 148, 149, 161, 165splfv3 30625 . . . . . . 7 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → ((𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)‘((((♯‘𝑊) − 1) − 𝐸) + (𝐸 + 1))) = (𝑊‘((((♯‘𝑊) − 1) − 𝐸) + 𝐸)))
167137, 72npcand 10993 . . . . . . . . 9 (𝜑 → ((((♯‘𝑊) − 1) − 𝐸) + 𝐸) = ((♯‘𝑊) − 1))
168167fveq2d 6667 . . . . . . . 8 (𝜑 → (𝑊‘((((♯‘𝑊) − 1) − 𝐸) + 𝐸)) = (𝑊‘((♯‘𝑊) − 1)))
169168adantr 483 . . . . . . 7 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → (𝑊‘((((♯‘𝑊) − 1) − 𝐸) + 𝐸)) = (𝑊‘((♯‘𝑊) − 1)))
170143, 166, 1693eqtrd 2858 . . . . . 6 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → (𝑈‘((♯‘𝑈) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
171170fveq2d 6667 . . . . 5 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → ((𝑀𝑊)‘(𝑈‘((♯‘𝑈) − 1))) = ((𝑀𝑊)‘(𝑊‘((♯‘𝑊) − 1))))
17213fveq1d 6665 . . . . . . 7 (𝜑 → (𝑈‘0) = ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘0))
173 nn0p1nn 11928 . . . . . . . . . . . 12 (𝐸 ∈ ℕ0 → (𝐸 + 1) ∈ ℕ)
17467, 173syl 17 . . . . . . . . . . 11 (𝜑 → (𝐸 + 1) ∈ ℕ)
175 lbfzo0 13069 . . . . . . . . . . 11 (0 ∈ (0..^(𝐸 + 1)) ↔ (𝐸 + 1) ∈ ℕ)
176174, 175sylibr 236 . . . . . . . . . 10 (𝜑 → 0 ∈ (0..^(𝐸 + 1)))
17757oveq2d 7164 . . . . . . . . . 10 (𝜑 → (0..^(♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩))) = (0..^(𝐸 + 1)))
178176, 177eleqtrrd 2914 . . . . . . . . 9 (𝜑 → 0 ∈ (0..^(♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩))))
179 ccatval1 13922 . . . . . . . . 9 ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ∈ Word 𝐷 ∧ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∈ Word 𝐷 ∧ 0 ∈ (0..^(♯‘((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)))) → ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘0) = (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)‘0))
18028, 30, 178, 179syl3anc 1366 . . . . . . . 8 (𝜑 → ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘0) = (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)‘0))
181 elfzonn0 13074 . . . . . . . . . . . . . 14 ((𝑊𝐽) ∈ (0..^(♯‘𝑊)) → (𝑊𝐽) ∈ ℕ0)
18250, 181syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑊𝐽) ∈ ℕ0)
183 nn0p1nn 11928 . . . . . . . . . . . . 13 ((𝑊𝐽) ∈ ℕ0 → ((𝑊𝐽) + 1) ∈ ℕ)
184182, 183syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝑊𝐽) + 1) ∈ ℕ)
1855, 184eqeltrid 2915 . . . . . . . . . . 11 (𝜑𝐸 ∈ ℕ)
186 lbfzo0 13069 . . . . . . . . . . 11 (0 ∈ (0..^𝐸) ↔ 𝐸 ∈ ℕ)
187185, 186sylibr 236 . . . . . . . . . 10 (𝜑 → 0 ∈ (0..^𝐸))
18855oveq2d 7164 . . . . . . . . . 10 (𝜑 → (0..^(♯‘(𝑊 prefix 𝐸))) = (0..^𝐸))
189187, 188eleqtrrd 2914 . . . . . . . . 9 (𝜑 → 0 ∈ (0..^(♯‘(𝑊 prefix 𝐸))))
190 ccatval1 13922 . . . . . . . . 9 (((𝑊 prefix 𝐸) ∈ Word 𝐷 ∧ ⟨“𝐼”⟩ ∈ Word 𝐷 ∧ 0 ∈ (0..^(♯‘(𝑊 prefix 𝐸)))) → (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)‘0) = ((𝑊 prefix 𝐸)‘0))
19126, 10, 189, 190syl3anc 1366 . . . . . . . 8 (𝜑 → (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)‘0) = ((𝑊 prefix 𝐸)‘0))
192 nn0p1gt0 11918 . . . . . . . . . . . . . 14 ((𝑊𝐽) ∈ ℕ0 → 0 < ((𝑊𝐽) + 1))
193182, 192syl 17 . . . . . . . . . . . . 13 (𝜑 → 0 < ((𝑊𝐽) + 1))
194193, 5breqtrrdi 5099 . . . . . . . . . . . 12 (𝜑 → 0 < 𝐸)
195194gt0ne0d 11196 . . . . . . . . . . 11 (𝜑𝐸 ≠ 0)
196 fzne1 30503 . . . . . . . . . . 11 ((𝐸 ∈ (0...(♯‘𝑊)) ∧ 𝐸 ≠ 0) → 𝐸 ∈ ((0 + 1)...(♯‘𝑊)))
19753, 195, 196syl2anc 586 . . . . . . . . . 10 (𝜑𝐸 ∈ ((0 + 1)...(♯‘𝑊)))
198 0p1e1 11751 . . . . . . . . . . 11 (0 + 1) = 1
199198oveq1i 7158 . . . . . . . . . 10 ((0 + 1)...(♯‘𝑊)) = (1...(♯‘𝑊))
200197, 199eleqtrdi 2921 . . . . . . . . 9 (𝜑𝐸 ∈ (1...(♯‘𝑊)))
201 pfxfv0 14046 . . . . . . . . 9 ((𝑊 ∈ Word 𝐷𝐸 ∈ (1...(♯‘𝑊))) → ((𝑊 prefix 𝐸)‘0) = (𝑊‘0))
20224, 200, 201syl2anc 586 . . . . . . . 8 (𝜑 → ((𝑊 prefix 𝐸)‘0) = (𝑊‘0))
203180, 191, 2023eqtrd 2858 . . . . . . 7 (𝜑 → ((((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))‘0) = (𝑊‘0))
204172, 203eqtrd 2854 . . . . . 6 (𝜑 → (𝑈‘0) = (𝑊‘0))
205204adantr 483 . . . . 5 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → (𝑈‘0) = (𝑊‘0))
206132, 171, 2053eqtr4rd 2865 . . . 4 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → (𝑈‘0) = ((𝑀𝑊)‘(𝑈‘((♯‘𝑈) − 1))))
207118, 206eqtrd 2854 . . 3 ((𝜑 ∧ (♯‘𝑊) ≠ 𝐸) → ((𝑀𝑈)‘(𝑈‘((♯‘𝑈) − 1))) = ((𝑀𝑊)‘(𝑈‘((♯‘𝑈) − 1))))
208109, 207pm2.61dane 3102 . 2 (𝜑 → ((𝑀𝑈)‘(𝑈‘((♯‘𝑈) − 1))) = ((𝑀𝑊)‘(𝑈‘((♯‘𝑈) − 1))))
209101fveq2d 6667 . 2 (𝜑 → ((𝑀𝑈)‘(𝑈‘((♯‘𝑈) − 1))) = ((𝑀𝑈)‘𝐾))
210101fveq2d 6667 . 2 (𝜑 → ((𝑀𝑊)‘(𝑈‘((♯‘𝑈) − 1))) = ((𝑀𝑊)‘𝐾))
211208, 209, 2103eqtr3d 2862 1 (𝜑 → ((𝑀𝑈)‘𝐾) = ((𝑀𝑊)‘𝐾))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 398   = wceq 1531  wcel 2108  wne 3014  {crab 3140  Vcvv 3493  cdif 3931  cun 3932  c0 4289  {csn 4559  cop 4565  cotp 4567   class class class wbr 5057  ccnv 5547  dom cdm 5548  ran crn 5549  wf 6344  1-1wf1 6345  1-1-ontowf1o 6347  cfv 6348  (class class class)co 7148  cc 10527  0cc0 10529  1c1 10530   + caddc 10532   < clt 10667  cmin 10862  cn 11630  0cn0 11889  ...cfz 12884  ..^cfzo 13025  chash 13682  Word cword 13853   ++ cconcat 13914  ⟨“cs1 13941   substr csubstr 13994   prefix cpfx 14024   splice csplice 14103  Basecbs 16475  SymGrpcsymg 18487  toCycctocyc 30741
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-ot 4568  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7573  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-oadd 8098  df-er 8281  df-map 8400  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-sup 8898  df-inf 8899  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-xnn0 11960  df-z 11974  df-uz 12236  df-rp 12382  df-fz 12885  df-fzo 13026  df-fl 13154  df-mod 13230  df-hash 13683  df-word 13854  df-concat 13915  df-s1 13942  df-substr 13995  df-pfx 14025  df-splice 14104  df-csh 14143  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-tset 16576  df-efmnd 18026  df-symg 18488  df-tocyc 30742
This theorem is referenced by:  cycpmco2  30768
  Copyright terms: Public domain W3C validator