Theorem efgredleme 19349

Description: Lemma for efgred 19354. (Contributed by Mario Carneiro, 1-Oct-2015.) (Proof shortened by AV, 15-Oct-2022.)

Hypotheses

Ref	Expression
efgval.w	⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))
efgval.r	⊢ ∼ = ( ~FG ‘𝐼)
efgval2.m	⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)
efgval2.t	⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))
efgred.d	⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))
efgred.s	⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))
efgredlem.1	⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))
efgredlem.2	⊢ (𝜑 → 𝐴 ∈ dom 𝑆)
efgredlem.3	⊢ (𝜑 → 𝐵 ∈ dom 𝑆)
efgredlem.4	⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵))
efgredlem.5	⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0))
efgredlemb.k	⊢ 𝐾 = (((♯‘𝐴) − 1) − 1)
efgredlemb.l	⊢ 𝐿 = (((♯‘𝐵) − 1) − 1)
efgredlemb.p	⊢ (𝜑 → 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))))
efgredlemb.q	⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))))
efgredlemb.u	⊢ (𝜑 → 𝑈 ∈ (𝐼 × 2o))
efgredlemb.v	⊢ (𝜑 → 𝑉 ∈ (𝐼 × 2o))
efgredlemb.6	⊢ (𝜑 → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈))
efgredlemb.7	⊢ (𝜑 → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉))
efgredlemb.8	⊢ (𝜑 → ¬ (𝐴‘𝐾) = (𝐵‘𝐿))
efgredlemd.9	⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(𝑄 + 2)))
efgredlemd.c	⊢ (𝜑 → 𝐶 ∈ dom 𝑆)
efgredlemd.sc	⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))

Assertion

Ref	Expression
efgredleme	⊢ (𝜑 → ((𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶)) ∧ (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶))))

Distinct variable groups:   𝑎,𝑏,𝐴   𝑦,𝑎,𝑧,𝑏   𝐿,𝑎,𝑏   𝐾,𝑎,𝑏   𝑡,𝑛,𝑣,𝑤,𝑦,𝑧,𝑃   𝑚,𝑎,𝑛,𝑡,𝑣,𝑤,𝑥,𝑀,𝑏   𝑈,𝑛,𝑣,𝑤,𝑦,𝑧   𝑘,𝑎,𝑇,𝑏,𝑚,𝑡,𝑥   𝑛,𝑉,𝑣,𝑤,𝑦,𝑧   𝑄,𝑛,𝑡,𝑣,𝑤,𝑦,𝑧   𝑊,𝑎,𝑏   𝑘,𝑛,𝑣,𝑤,𝑦,𝑧,𝑊,𝑚,𝑡,𝑥   ∼ ,𝑎,𝑏,𝑚,𝑡,𝑥,𝑦,𝑧   𝐵,𝑎,𝑏   𝐶,𝑎,𝑏,𝑘,𝑚,𝑛,𝑡,𝑣,𝑤,𝑥,𝑦,𝑧   𝑆,𝑎,𝑏   𝐼,𝑎,𝑏,𝑚,𝑛,𝑡,𝑣,𝑤,𝑥,𝑦,𝑧   𝐷,𝑎,𝑏,𝑚,𝑡

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛,𝑎,𝑏)   𝐴(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝐵(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝐷(𝑥,𝑦,𝑧,𝑤,𝑣,𝑘,𝑛)   𝑃(𝑥,𝑘,𝑚,𝑎,𝑏)   𝑄(𝑥,𝑘,𝑚,𝑎,𝑏)   ∼ (𝑤,𝑣,𝑘,𝑛)   𝑆(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝑇(𝑦,𝑧,𝑤,𝑣,𝑛)   𝑈(𝑥,𝑡,𝑘,𝑚,𝑎,𝑏)   𝐼(𝑘)   𝐾(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝐿(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝑀(𝑦,𝑧,𝑘)   𝑉(𝑥,𝑡,𝑘,𝑚,𝑎,𝑏)

Proof of Theorem efgredleme

Dummy variable 𝑖 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		efgredlemd.c	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ dom 𝑆)
2		efgval.w	. . . . . . . . 9 ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))
3		efgval.r	. . . . . . . . 9 ⊢ ∼ = ( ~FG ‘𝐼)
4		efgval2.m	. . . . . . . . 9 ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)
5		efgval2.t	. . . . . . . . 9 ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))
6		efgred.d	. . . . . . . . 9 ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))
7		efgred.s	. . . . . . . . 9 ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))
8	2, 3, 4, 5, 6, 7	efgsf 19335	. . . . . . . 8 ⊢ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊
9	8	fdmi 6612	. . . . . . . . 9 ⊢ dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}
10	9	feq2i 6592	. . . . . . . 8 ⊢ (𝑆:dom 𝑆⟶𝑊 ↔ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊)
11	8, 10	mpbir 230	. . . . . . 7 ⊢ 𝑆:dom 𝑆⟶𝑊
12	11	ffvelrni 6960	. . . . . 6 ⊢ (𝐶 ∈ dom 𝑆 → (𝑆‘𝐶) ∈ 𝑊)
13	1, 12	syl 17	. . . . 5 ⊢ (𝜑 → (𝑆‘𝐶) ∈ 𝑊)
14		efgredlemb.q	. . . . . . 7 ⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))))
15		elfzuz 13252	. . . . . . 7 ⊢ (𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) → 𝑄 ∈ (ℤ≥‘0))
16	14, 15	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑄 ∈ (ℤ≥‘0))
17		efgredlemd.sc	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
18	17	fveq2d 6778	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(𝑆‘𝐶)) = (♯‘(((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))))
19		fviss 6845	. . . . . . . . . . . . 13 ⊢ ( I ‘Word (𝐼 × 2o)) ⊆ Word (𝐼 × 2o)
20	2, 19	eqsstri 3955	. . . . . . . . . . . 12 ⊢ 𝑊 ⊆ Word (𝐼 × 2o)
21		efgredlem.1	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))
22		efgredlem.2	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ dom 𝑆)
23		efgredlem.3	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ dom 𝑆)
24		efgredlem.4	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵))
25		efgredlem.5	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0))
26		efgredlemb.k	. . . . . . . . . . . . . 14 ⊢ 𝐾 = (((♯‘𝐴) − 1) − 1)
27		efgredlemb.l	. . . . . . . . . . . . . 14 ⊢ 𝐿 = (((♯‘𝐵) − 1) − 1)
28	2, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27	efgredlemf 19347	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝐾) ∈ 𝑊 ∧ (𝐵‘𝐿) ∈ 𝑊))
29	28	simprd 496	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵‘𝐿) ∈ 𝑊)
30	20, 29	sselid 3919	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵‘𝐿) ∈ Word (𝐼 × 2o))
31		pfxcl 14390	. . . . . . . . . . 11 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o))
32	30, 31	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o))
33	28	simpld 495	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴‘𝐾) ∈ 𝑊)
34	20, 33	sselid 3919	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴‘𝐾) ∈ Word (𝐼 × 2o))
35		swrdcl 14358	. . . . . . . . . . 11 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2o))
36	34, 35	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2o))
37		ccatlen 14278	. . . . . . . . . 10 ⊢ ((((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2o)) → (♯‘(((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))) = ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))))
38	32, 36, 37	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))) = ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))))
39		pfxlen 14396	. . . . . . . . . . . 12 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) prefix 𝑄)) = 𝑄)
40	30, 14, 39	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) prefix 𝑄)) = 𝑄)
41		2nn0 12250	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ0
42		uzaddcl 12644	. . . . . . . . . . . . . 14 ⊢ ((𝑄 ∈ (ℤ≥‘0) ∧ 2 ∈ ℕ0) → (𝑄 + 2) ∈ (ℤ≥‘0))
43	16, 41, 42	sylancl 586	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄 + 2) ∈ (ℤ≥‘0))
44		efgredlemb.p	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))))
45		elfzuz3 13253	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘𝑃))
46	44, 45	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘𝑃))
47		efgredlemd.9	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(𝑄 + 2)))
48		uztrn 12600	. . . . . . . . . . . . . 14 ⊢ (((♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘𝑃) ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘(𝑄 + 2)))
49	46, 47, 48	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘(𝑄 + 2)))
50		elfzuzb 13250	. . . . . . . . . . . . 13 ⊢ ((𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾))) ↔ ((𝑄 + 2) ∈ (ℤ≥‘0) ∧ (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘(𝑄 + 2))))
51	43, 49, 50	sylanbrc 583	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾))))
52		lencl 14236	. . . . . . . . . . . . . . 15 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → (♯‘(𝐴‘𝐾)) ∈ ℕ0)
53	34, 52	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ ℕ0)
54		nn0uz 12620	. . . . . . . . . . . . . 14 ⊢ ℕ0 = (ℤ≥‘0)
55	53, 54	eleqtrdi 2849	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘0))
56		eluzfz2 13264	. . . . . . . . . . . . 13 ⊢ ((♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘0) → (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾))))
57	55, 56	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾))))
58		swrdlen 14360	. . . . . . . . . . . 12 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾))) ∧ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((♯‘(𝐴‘𝐾)) − (𝑄 + 2)))
59	34, 51, 57, 58	syl3anc 1370	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((♯‘(𝐴‘𝐾)) − (𝑄 + 2)))
60	40, 59	oveq12d 7293	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))) = (𝑄 + ((♯‘(𝐴‘𝐾)) − (𝑄 + 2))))
61	14	elfzelzd 13257	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ ℤ)
62	61	zcnd 12427	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ ℂ)
63	53	nn0cnd 12295	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ ℂ)
64		2z 12352	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℤ
65		zaddcl 12360	. . . . . . . . . . . . 13 ⊢ ((𝑄 ∈ ℤ ∧ 2 ∈ ℤ) → (𝑄 + 2) ∈ ℤ)
66	61, 64, 65	sylancl 586	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄 + 2) ∈ ℤ)
67	66	zcnd 12427	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄 + 2) ∈ ℂ)
68	62, 63, 67	addsubassd 11352	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑄 + (♯‘(𝐴‘𝐾))) − (𝑄 + 2)) = (𝑄 + ((♯‘(𝐴‘𝐾)) − (𝑄 + 2))))
69		2cn 12048	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
70	69	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℂ)
71	62, 63, 70	pnpcand 11369	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑄 + (♯‘(𝐴‘𝐾))) − (𝑄 + 2)) = ((♯‘(𝐴‘𝐾)) − 2))
72	60, 68, 71	3eqtr2d 2784	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))) = ((♯‘(𝐴‘𝐾)) − 2))
73	18, 38, 72	3eqtrd 2782	. . . . . . . 8 ⊢ (𝜑 → (♯‘(𝑆‘𝐶)) = ((♯‘(𝐴‘𝐾)) − 2))
74	44	elfzelzd 13257	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ ℤ)
75		zsubcl 12362	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℤ ∧ 2 ∈ ℤ) → (𝑃 − 2) ∈ ℤ)
76	74, 64, 75	sylancl 586	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 − 2) ∈ ℤ)
77	64	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 2 ∈ ℤ)
78	74	zcnd 12427	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℂ)
79		npcan 11230	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑃 − 2) + 2) = 𝑃)
80	78, 69, 79	sylancl 586	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑃 − 2) + 2) = 𝑃)
81	80	fveq2d 6778	. . . . . . . . . 10 ⊢ (𝜑 → (ℤ≥‘((𝑃 − 2) + 2)) = (ℤ≥‘𝑃))
82	46, 81	eleqtrrd 2842	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘((𝑃 − 2) + 2)))
83		eluzsub 12614	. . . . . . . . 9 ⊢ (((𝑃 − 2) ∈ ℤ ∧ 2 ∈ ℤ ∧ (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘((𝑃 − 2) + 2))) → ((♯‘(𝐴‘𝐾)) − 2) ∈ (ℤ≥‘(𝑃 − 2)))
84	76, 77, 82, 83	syl3anc 1370	. . . . . . . 8 ⊢ (𝜑 → ((♯‘(𝐴‘𝐾)) − 2) ∈ (ℤ≥‘(𝑃 − 2)))
85	73, 84	eqeltrd 2839	. . . . . . 7 ⊢ (𝜑 → (♯‘(𝑆‘𝐶)) ∈ (ℤ≥‘(𝑃 − 2)))
86		eluzsub 12614	. . . . . . . 8 ⊢ ((𝑄 ∈ ℤ ∧ 2 ∈ ℤ ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) → (𝑃 − 2) ∈ (ℤ≥‘𝑄))
87	61, 77, 47, 86	syl3anc 1370	. . . . . . 7 ⊢ (𝜑 → (𝑃 − 2) ∈ (ℤ≥‘𝑄))
88		uztrn 12600	. . . . . . 7 ⊢ (((♯‘(𝑆‘𝐶)) ∈ (ℤ≥‘(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (ℤ≥‘𝑄)) → (♯‘(𝑆‘𝐶)) ∈ (ℤ≥‘𝑄))
89	85, 87, 88	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (♯‘(𝑆‘𝐶)) ∈ (ℤ≥‘𝑄))
90		elfzuzb 13250	. . . . . 6 ⊢ (𝑄 ∈ (0...(♯‘(𝑆‘𝐶))) ↔ (𝑄 ∈ (ℤ≥‘0) ∧ (♯‘(𝑆‘𝐶)) ∈ (ℤ≥‘𝑄)))
91	16, 89, 90	sylanbrc 583	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝑆‘𝐶))))
92		efgredlemb.v	. . . . 5 ⊢ (𝜑 → 𝑉 ∈ (𝐼 × 2o))
93	2, 3, 4, 5	efgtval 19329	. . . . 5 ⊢ (((𝑆‘𝐶) ∈ 𝑊 ∧ 𝑄 ∈ (0...(♯‘(𝑆‘𝐶))) ∧ 𝑉 ∈ (𝐼 × 2o)) → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = ((𝑆‘𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩))
94	13, 91, 92, 93	syl3anc 1370	. . . 4 ⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = ((𝑆‘𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩))
95		pfxcl 14390	. . . . . 6 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o))
96	34, 95	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o))
97		wrd0 14242	. . . . . 6 ⊢ ∅ ∈ Word (𝐼 × 2o)
98	97	a1i 11	. . . . 5 ⊢ (𝜑 → ∅ ∈ Word (𝐼 × 2o))
99	4	efgmf 19319	. . . . . . . 8 ⊢ 𝑀:(𝐼 × 2o)⟶(𝐼 × 2o)
100	99	ffvelrni 6960	. . . . . . 7 ⊢ (𝑉 ∈ (𝐼 × 2o) → (𝑀‘𝑉) ∈ (𝐼 × 2o))
101	92, 100	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑀‘𝑉) ∈ (𝐼 × 2o))
102	92, 101	s2cld 14584	. . . . 5 ⊢ (𝜑 → ⟨“𝑉(𝑀‘𝑉)”⟩ ∈ Word (𝐼 × 2o))
103	61	zred 12426	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄 ∈ ℝ)
104		nn0addge1 12279	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄 ∈ ℝ ∧ 2 ∈ ℕ0) → 𝑄 ≤ (𝑄 + 2))
105	103, 41, 104	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑄 ≤ (𝑄 + 2))
106		eluz2 12588	. . . . . . . . . . . . . . . 16 ⊢ ((𝑄 + 2) ∈ (ℤ≥‘𝑄) ↔ (𝑄 ∈ ℤ ∧ (𝑄 + 2) ∈ ℤ ∧ 𝑄 ≤ (𝑄 + 2)))
107	61, 66, 105, 106	syl3anbrc 1342	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑄 + 2) ∈ (ℤ≥‘𝑄))
108		uztrn 12600	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℤ≥‘(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (ℤ≥‘𝑄)) → 𝑃 ∈ (ℤ≥‘𝑄))
109	47, 107, 108	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘𝑄))
110		elfzuzb 13250	. . . . . . . . . . . . . 14 ⊢ (𝑄 ∈ (0...𝑃) ↔ (𝑄 ∈ (ℤ≥‘0) ∧ 𝑃 ∈ (ℤ≥‘𝑄)))
111	16, 109, 110	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∈ (0...𝑃))
112		ccatpfx 14414	. . . . . . . . . . . . 13 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾)))) → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) = ((𝐴‘𝐾) prefix 𝑃))
113	34, 111, 44, 112	syl3anc 1370	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) = ((𝐴‘𝐾) prefix 𝑃))
114	113	oveq1d 7290	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) prefix 𝑃) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))))
115		pfxcl 14390	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) prefix 𝑃) ∈ Word (𝐼 × 2o))
116	34, 115	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) prefix 𝑃) ∈ Word (𝐼 × 2o))
117		efgredlemb.u	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ∈ (𝐼 × 2o))
118	99	ffvelrni 6960	. . . . . . . . . . . . . 14 ⊢ (𝑈 ∈ (𝐼 × 2o) → (𝑀‘𝑈) ∈ (𝐼 × 2o))
119	117, 118	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀‘𝑈) ∈ (𝐼 × 2o))
120	117, 119	s2cld 14584	. . . . . . . . . . . 12 ⊢ (𝜑 → ⟨“𝑈(𝑀‘𝑈)”⟩ ∈ Word (𝐼 × 2o))
121		swrdcl 14358	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2o))
122	34, 121	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2o))
123		ccatass 14293	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝐾) prefix 𝑃) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑈(𝑀‘𝑈)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2o)) → ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐴‘𝐾) prefix 𝑃) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))))
124	116, 120, 122, 123	syl3anc 1370	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐴‘𝐾) prefix 𝑃) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))))
125		efgredlemb.6	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈))
126	2, 3, 4, 5	efgtval 19329	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝐾) ∈ 𝑊 ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ 𝑈 ∈ (𝐼 × 2o)) → (𝑃(𝑇‘(𝐴‘𝐾))𝑈) = ((𝐴‘𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀‘𝑈)”⟩⟩))
127	33, 44, 117, 126	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃(𝑇‘(𝐴‘𝐾))𝑈) = ((𝐴‘𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀‘𝑈)”⟩⟩))
128		splval 14464	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝐾) ∈ 𝑊 ∧ (𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ ⟨“𝑈(𝑀‘𝑈)”⟩ ∈ Word (𝐼 × 2o))) → ((𝐴‘𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀‘𝑈)”⟩⟩) = ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))
129	33, 44, 44, 120, 128	syl13anc 1371	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀‘𝑈)”⟩⟩) = ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))
130	125, 127, 129	3eqtrd 2782	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘𝐴) = ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))
131		efgredlemb.7	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉))
132	2, 3, 4, 5	efgtval 19329	. . . . . . . . . . . . . 14 ⊢ (((𝐵‘𝐿) ∈ 𝑊 ∧ 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ 𝑉 ∈ (𝐼 × 2o)) → (𝑄(𝑇‘(𝐵‘𝐿))𝑉) = ((𝐵‘𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩))
133	29, 14, 92, 132	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄(𝑇‘(𝐵‘𝐿))𝑉) = ((𝐵‘𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩))
134		splval 14464	. . . . . . . . . . . . . 14 ⊢ (((𝐵‘𝐿) ∈ 𝑊 ∧ (𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ ⟨“𝑉(𝑀‘𝑉)”⟩ ∈ Word (𝐼 × 2o))) → ((𝐵‘𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
135	29, 14, 14, 102, 134	syl13anc 1371	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵‘𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
136	131, 133, 135	3eqtrd 2782	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘𝐵) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
137	24, 130, 136	3eqtr3d 2786	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
138	114, 124, 137	3eqtr2d 2784	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
139		swrdcl 14358	. . . . . . . . . . . 12 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2o))
140	34, 139	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2o))
141		ccatcl 14277	. . . . . . . . . . . 12 ⊢ ((⟨“𝑈(𝑀‘𝑈)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2o)) → (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2o))
142	120, 122, 141	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2o))
143		ccatass 14293	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2o)) → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))))
144	96, 140, 142, 143	syl3anc 1370	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))))
145		swrdcl 14358	. . . . . . . . . . . 12 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o))
146	30, 145	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o))
147		ccatass 14293	. . . . . . . . . . 11 ⊢ ((((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑉(𝑀‘𝑉)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o)) → ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
148	32, 102, 146, 147	syl3anc 1370	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
149	138, 144, 148	3eqtr3d 2786	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))) = (((𝐵‘𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
150		ccatcl 14277	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2o)) → (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2o))
151	140, 142, 150	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2o))
152		ccatcl 14277	. . . . . . . . . . 11 ⊢ ((⟨“𝑉(𝑀‘𝑉)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o)) → (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) ∈ Word (𝐼 × 2o))
153	102, 146, 152	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) ∈ Word (𝐼 × 2o))
154		uztrn 12600	. . . . . . . . . . . . . 14 ⊢ (((♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘𝑃) ∧ 𝑃 ∈ (ℤ≥‘𝑄)) → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘𝑄))
155	46, 109, 154	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘𝑄))
156		elfzuzb 13250	. . . . . . . . . . . . 13 ⊢ (𝑄 ∈ (0...(♯‘(𝐴‘𝐾))) ↔ (𝑄 ∈ (ℤ≥‘0) ∧ (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘𝑄)))
157	16, 155, 156	sylanbrc 583	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝐴‘𝐾))))
158		pfxlen 14396	. . . . . . . . . . . 12 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) prefix 𝑄)) = 𝑄)
159	34, 157, 158	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) prefix 𝑄)) = 𝑄)
160	159, 40	eqtr4d 2781	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) prefix 𝑄)) = (♯‘((𝐵‘𝐿) prefix 𝑄)))
161		ccatopth 14429	. . . . . . . . . 10 ⊢ (((((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2o)) ∧ (((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) ∈ Word (𝐼 × 2o)) ∧ (♯‘((𝐴‘𝐾) prefix 𝑄)) = (♯‘((𝐵‘𝐿) prefix 𝑄))) → ((((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))) = (((𝐵‘𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))) ↔ (((𝐴‘𝐾) prefix 𝑄) = ((𝐵‘𝐿) prefix 𝑄) ∧ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))))
162	96, 151, 32, 153, 160, 161	syl221anc 1380	. . . . . . . . 9 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))) = (((𝐵‘𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))) ↔ (((𝐴‘𝐾) prefix 𝑄) = ((𝐵‘𝐿) prefix 𝑄) ∧ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))))
163	149, 162	mpbid 231	. . . . . . . 8 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) = ((𝐵‘𝐿) prefix 𝑄) ∧ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
164	163	simpld 495	. . . . . . 7 ⊢ (𝜑 → ((𝐴‘𝐾) prefix 𝑄) = ((𝐵‘𝐿) prefix 𝑄))
165	164	oveq1d 7290	. . . . . 6 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
166		ccatrid 14292	. . . . . . . 8 ⊢ (((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o) → (((𝐴‘𝐾) prefix 𝑄) ++ ∅) = ((𝐴‘𝐾) prefix 𝑄))
167	96, 166	syl 17	. . . . . . 7 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ∅) = ((𝐴‘𝐾) prefix 𝑄))
168	167	oveq1d 7290	. . . . . 6 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ∅) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
169	165, 168, 17	3eqtr4rd 2789	. . . . 5 ⊢ (𝜑 → (𝑆‘𝐶) = ((((𝐴‘𝐾) prefix 𝑄) ++ ∅) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
170	159	eqcomd 2744	. . . . 5 ⊢ (𝜑 → 𝑄 = (♯‘((𝐴‘𝐾) prefix 𝑄)))
171		hash0 14082	. . . . . . 7 ⊢ (♯‘∅) = 0
172	171	oveq2i 7286	. . . . . 6 ⊢ (𝑄 + (♯‘∅)) = (𝑄 + 0)
173	62	addid1d 11175	. . . . . 6 ⊢ (𝜑 → (𝑄 + 0) = 𝑄)
174	172, 173	eqtr2id 2791	. . . . 5 ⊢ (𝜑 → 𝑄 = (𝑄 + (♯‘∅)))
175	96, 98, 36, 102, 169, 170, 174	splval2 14470	. . . 4 ⊢ (𝜑 → ((𝑆‘𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩) = ((((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
176		elfzuzb 13250	. . . . . . . . . . . . . 14 ⊢ (𝑄 ∈ (0...(𝑄 + 2)) ↔ (𝑄 ∈ (ℤ≥‘0) ∧ (𝑄 + 2) ∈ (ℤ≥‘𝑄)))
177	16, 107, 176	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∈ (0...(𝑄 + 2)))
178		elfzuzb 13250	. . . . . . . . . . . . . 14 ⊢ ((𝑄 + 2) ∈ (0...𝑃) ↔ ((𝑄 + 2) ∈ (ℤ≥‘0) ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))))
179	43, 47, 178	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄 + 2) ∈ (0...𝑃))
180		ccatswrd 14381	. . . . . . . . . . . . 13 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))))) → (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩))
181	34, 177, 179, 44, 180	syl13anc 1371	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩))
182	181	oveq1d 7290	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))))
183		swrdcl 14358	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2o))
184	34, 183	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2o))
185		swrdcl 14358	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2o))
186	34, 185	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2o))
187		ccatass 14293	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2o) ∧ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2o)) → ((((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))))
188	184, 186, 142, 187	syl3anc 1370	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))))
189	163	simprd 496	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
190	182, 188, 189	3eqtr3d 2786	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
191		ccatcl 14277	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2o)) → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2o))
192	186, 142, 191	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2o))
193		swrdlen 14360	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝑄 + 2) − 𝑄))
194	34, 177, 51, 193	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝑄 + 2) − 𝑄))
195		pncan2 11228	. . . . . . . . . . . . . 14 ⊢ ((𝑄 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑄 + 2) − 𝑄) = 2)
196	62, 69, 195	sylancl 586	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑄 + 2) − 𝑄) = 2)
197	194, 196	eqtrd 2778	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = 2)
198		s2len 14602	. . . . . . . . . . . 12 ⊢ (♯‘⟨“𝑉(𝑀‘𝑉)”⟩) = 2
199	197, 198	eqtr4di 2796	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (♯‘⟨“𝑉(𝑀‘𝑉)”⟩))
200		ccatopth 14429	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2o) ∧ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2o)) ∧ (⟨“𝑉(𝑀‘𝑉)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o)) ∧ (♯‘((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (♯‘⟨“𝑉(𝑀‘𝑉)”⟩)) → ((((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) ↔ (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀‘𝑉)”⟩ ∧ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
201	184, 192, 102, 146, 199, 200	syl221anc 1380	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) ↔ (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀‘𝑉)”⟩ ∧ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
202	190, 201	mpbid 231	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀‘𝑉)”⟩ ∧ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
203	202	simpld 495	. . . . . . . 8 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀‘𝑉)”⟩)
204	203	oveq2d 7291	. . . . . . 7 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩))
205		ccatpfx 14414	. . . . . . . 8 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾)))) → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝐴‘𝐾) prefix (𝑄 + 2)))
206	34, 177, 51, 205	syl3anc 1370	. . . . . . 7 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝐴‘𝐾) prefix (𝑄 + 2)))
207	204, 206	eqtr3d 2780	. . . . . 6 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) = ((𝐴‘𝐾) prefix (𝑄 + 2)))
208	207	oveq1d 7290	. . . . 5 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (((𝐴‘𝐾) prefix (𝑄 + 2)) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
209		ccatpfx 14414	. . . . . 6 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾))) ∧ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾)))) → (((𝐴‘𝐾) prefix (𝑄 + 2)) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))))
210	34, 51, 57, 209	syl3anc 1370	. . . . 5 ⊢ (𝜑 → (((𝐴‘𝐾) prefix (𝑄 + 2)) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))))
211		pfxid 14397	. . . . . 6 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))) = (𝐴‘𝐾))
212	34, 211	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))) = (𝐴‘𝐾))
213	208, 210, 212	3eqtrd 2782	. . . 4 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (𝐴‘𝐾))
214	94, 175, 213	3eqtrd 2782	. . 3 ⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = (𝐴‘𝐾))
215	2, 3, 4, 5	efgtf 19328	. . . . . . 7 ⊢ ((𝑆‘𝐶) ∈ 𝑊 → ((𝑇‘(𝑆‘𝐶)) = (𝑎 ∈ (0...(♯‘(𝑆‘𝐶))), 𝑖 ∈ (𝐼 × 2o) ↦ ((𝑆‘𝐶) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀‘𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆‘𝐶)):((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o))⟶𝑊))
216	13, 215	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝑇‘(𝑆‘𝐶)) = (𝑎 ∈ (0...(♯‘(𝑆‘𝐶))), 𝑖 ∈ (𝐼 × 2o) ↦ ((𝑆‘𝐶) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀‘𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆‘𝐶)):((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o))⟶𝑊))
217	216	simprd 496	. . . . 5 ⊢ (𝜑 → (𝑇‘(𝑆‘𝐶)):((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o))⟶𝑊)
218	217	ffnd 6601	. . . 4 ⊢ (𝜑 → (𝑇‘(𝑆‘𝐶)) Fn ((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o)))
219		fnovrn 7447	. . . 4 ⊢ (((𝑇‘(𝑆‘𝐶)) Fn ((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o)) ∧ 𝑄 ∈ (0...(♯‘(𝑆‘𝐶))) ∧ 𝑉 ∈ (𝐼 × 2o)) → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) ∈ ran (𝑇‘(𝑆‘𝐶)))
220	218, 91, 92, 219	syl3anc 1370	. . 3 ⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) ∈ ran (𝑇‘(𝑆‘𝐶)))
221	214, 220	eqeltrrd 2840	. 2 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶)))
222		uztrn 12600	. . . . . . 7 ⊢ (((𝑃 − 2) ∈ (ℤ≥‘𝑄) ∧ 𝑄 ∈ (ℤ≥‘0)) → (𝑃 − 2) ∈ (ℤ≥‘0))
223	87, 16, 222	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝑃 − 2) ∈ (ℤ≥‘0))
224		elfzuzb 13250	. . . . . 6 ⊢ ((𝑃 − 2) ∈ (0...(♯‘(𝑆‘𝐶))) ↔ ((𝑃 − 2) ∈ (ℤ≥‘0) ∧ (♯‘(𝑆‘𝐶)) ∈ (ℤ≥‘(𝑃 − 2))))
225	223, 85, 224	sylanbrc 583	. . . . 5 ⊢ (𝜑 → (𝑃 − 2) ∈ (0...(♯‘(𝑆‘𝐶))))
226	2, 3, 4, 5	efgtval 19329	. . . . 5 ⊢ (((𝑆‘𝐶) ∈ 𝑊 ∧ (𝑃 − 2) ∈ (0...(♯‘(𝑆‘𝐶))) ∧ 𝑈 ∈ (𝐼 × 2o)) → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = ((𝑆‘𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀‘𝑈)”⟩⟩))
227	13, 225, 117, 226	syl3anc 1370	. . . 4 ⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = ((𝑆‘𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀‘𝑈)”⟩⟩))
228		pfxcl 14390	. . . . . 6 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2o))
229	30, 228	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐵‘𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2o))
230		swrdcl 14358	. . . . . 6 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o))
231	30, 230	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o))
232		ccatswrd 14381	. . . . . . . . . . 11 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ ((𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾))))) → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))
233	34, 179, 44, 57, 232	syl13anc 1371	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))
234	202	simprd 496	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))
235		elfzuzb 13250	. . . . . . . . . . . . . . . 16 ⊢ (𝑄 ∈ (0...(𝑃 − 2)) ↔ (𝑄 ∈ (ℤ≥‘0) ∧ (𝑃 − 2) ∈ (ℤ≥‘𝑄)))
236	16, 87, 235	sylanbrc 583	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑄 ∈ (0...(𝑃 − 2)))
237	2, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27, 44, 14, 117, 92, 125, 131	efgredlemg 19348	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) = (♯‘(𝐵‘𝐿)))
238	237, 46	eqeltrrd 2840	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘𝑃))
239		0le2 12075	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ≤ 2
240	239	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 ≤ 2)
241	74	zred 12426	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑃 ∈ ℝ)
242		2re 12047	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℝ
243		subge02 11491	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃 ∈ ℝ ∧ 2 ∈ ℝ) → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃))
244	241, 242, 243	sylancl 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃))
245	240, 244	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑃 − 2) ≤ 𝑃)
246		eluz2 12588	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ (ℤ≥‘(𝑃 − 2)) ↔ ((𝑃 − 2) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑃 − 2) ≤ 𝑃))
247	76, 74, 245, 246	syl3anbrc 1342	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(𝑃 − 2)))
248		uztrn 12600	. . . . . . . . . . . . . . . . 17 ⊢ (((♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘𝑃) ∧ 𝑃 ∈ (ℤ≥‘(𝑃 − 2))) → (♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘(𝑃 − 2)))
249	238, 247, 248	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘(𝑃 − 2)))
250		elfzuzb 13250	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿))) ↔ ((𝑃 − 2) ∈ (ℤ≥‘0) ∧ (♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘(𝑃 − 2))))
251	223, 249, 250	sylanbrc 583	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿))))
252		lencl 14236	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → (♯‘(𝐵‘𝐿)) ∈ ℕ0)
253	30, 252	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ ℕ0)
254	253, 54	eleqtrdi 2849	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘0))
255		eluzfz2 13264	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘0) → (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))
256	254, 255	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))
257		ccatswrd 14381	. . . . . . . . . . . . . . 15 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿))) ∧ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))) → (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))
258	30, 236, 251, 256, 257	syl13anc 1371	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))
259	234, 258	eqtr4d 2781	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)))
260		swrdcl 14358	. . . . . . . . . . . . . . 15 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2o))
261	30, 260	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2o))
262		swrdcl 14358	. . . . . . . . . . . . . . 15 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o))
263	30, 262	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o))
264		swrdlen 14360	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (𝑃 − (𝑄 + 2)))
265	34, 179, 44, 264	syl3anc 1370	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (𝑃 − (𝑄 + 2)))
266		swrdlen 14360	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝑃 − 2) − 𝑄))
267	30, 236, 251, 266	syl3anc 1370	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝑃 − 2) − 𝑄))
268	78, 62, 70	sub32d 11364	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑃 − 𝑄) − 2) = ((𝑃 − 2) − 𝑄))
269	78, 62, 70	subsub4d 11363	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑃 − 𝑄) − 2) = (𝑃 − (𝑄 + 2)))
270	267, 268, 269	3eqtr2d 2784	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = (𝑃 − (𝑄 + 2)))
271	265, 270	eqtr4d 2781	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (♯‘((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)))
272		ccatopth 14429	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2o)) ∧ (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2o) ∧ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o)) ∧ (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (♯‘((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩))) → ((((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)) ↔ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩))))
273	186, 142, 261, 263, 271, 272	syl221anc 1380	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)) ↔ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩))))
274	259, 273	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)))
275	274	simpld 495	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩))
276	274	simprd 496	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩))
277		elfzuzb 13250	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 − 2) ∈ (0...𝑃) ↔ ((𝑃 − 2) ∈ (ℤ≥‘0) ∧ 𝑃 ∈ (ℤ≥‘(𝑃 − 2))))
278	223, 247, 277	sylanbrc 583	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 − 2) ∈ (0...𝑃))
279		elfzuz 13252	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) → 𝑃 ∈ (ℤ≥‘0))
280	44, 279	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘0))
281		elfzuzb 13250	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ (0...(♯‘(𝐵‘𝐿))) ↔ (𝑃 ∈ (ℤ≥‘0) ∧ (♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘𝑃)))
282	280, 238, 281	sylanbrc 583	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ (0...(♯‘(𝐵‘𝐿))))
283		ccatswrd 14381	. . . . . . . . . . . . . . 15 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ ((𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))) → (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩))
284	30, 278, 282, 256, 283	syl13anc 1371	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩))
285	276, 284	eqtr4d 2781	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
286		swrdcl 14358	. . . . . . . . . . . . . . 15 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2o))
287	30, 286	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2o))
288		s2len 14602	. . . . . . . . . . . . . . 15 ⊢ (♯‘⟨“𝑈(𝑀‘𝑈)”⟩) = 2
289		swrdlen 14360	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = (𝑃 − (𝑃 − 2)))
290	30, 278, 282, 289	syl3anc 1370	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = (𝑃 − (𝑃 − 2)))
291		nncan 11250	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑃 − (𝑃 − 2)) = 2)
292	78, 69, 291	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃 − (𝑃 − 2)) = 2)
293	290, 292	eqtr2d 2779	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 = (♯‘((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
294	288, 293	eqtrid 2790	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘⟨“𝑈(𝑀‘𝑈)”⟩) = (♯‘((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
295		ccatopth 14429	. . . . . . . . . . . . . 14 ⊢ (((⟨“𝑈(𝑀‘𝑈)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2o)) ∧ (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o)) ∧ (♯‘⟨“𝑈(𝑀‘𝑈)”⟩) = (♯‘((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩))) → ((⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) ↔ (⟨“𝑈(𝑀‘𝑈)”⟩ = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) = ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))))
296	120, 122, 287, 231, 294, 295	syl221anc 1380	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) ↔ (⟨“𝑈(𝑀‘𝑈)”⟩ = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) = ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))))
297	285, 296	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝜑 → (⟨“𝑈(𝑀‘𝑈)”⟩ = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) = ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
298	297	simprd 496	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) = ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))
299	275, 298	oveq12d 7293	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
300	233, 299	eqtr3d 2780	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩) = (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
301	300	oveq2d 7291	. . . . . . . 8 ⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))))
302		ccatass 14293	. . . . . . . . 9 ⊢ ((((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2o) ∧ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o)) → ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))))
303	32, 261, 231, 302	syl3anc 1370	. . . . . . . 8 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))))
304	301, 303	eqtr4d 2781	. . . . . . 7 ⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
305		ccatpfx 14414	. . . . . . . . 9 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿)))) → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝐵‘𝐿) prefix (𝑃 − 2)))
306	30, 236, 251, 305	syl3anc 1370	. . . . . . . 8 ⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝐵‘𝐿) prefix (𝑃 − 2)))
307	306	oveq1d 7290	. . . . . . 7 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
308	17, 304, 307	3eqtrd 2782	. . . . . 6 ⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
309		ccatrid 14292	. . . . . . . 8 ⊢ (((𝐵‘𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2o) → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) = ((𝐵‘𝐿) prefix (𝑃 − 2)))
310	229, 309	syl 17	. . . . . . 7 ⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) = ((𝐵‘𝐿) prefix (𝑃 − 2)))
311	310	oveq1d 7290	. . . . . 6 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
312	308, 311	eqtr4d 2781	. . . . 5 ⊢ (𝜑 → (𝑆‘𝐶) = ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
313		pfxlen 14396	. . . . . . 7 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) prefix (𝑃 − 2))) = (𝑃 − 2))
314	30, 251, 313	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) prefix (𝑃 − 2))) = (𝑃 − 2))
315	314	eqcomd 2744	. . . . 5 ⊢ (𝜑 → (𝑃 − 2) = (♯‘((𝐵‘𝐿) prefix (𝑃 − 2))))
316	171	oveq2i 7286	. . . . . 6 ⊢ ((𝑃 − 2) + (♯‘∅)) = ((𝑃 − 2) + 0)
317	76	zcnd 12427	. . . . . . 7 ⊢ (𝜑 → (𝑃 − 2) ∈ ℂ)
318	317	addid1d 11175	. . . . . 6 ⊢ (𝜑 → ((𝑃 − 2) + 0) = (𝑃 − 2))
319	316, 318	eqtr2id 2791	. . . . 5 ⊢ (𝜑 → (𝑃 − 2) = ((𝑃 − 2) + (♯‘∅)))
320	229, 98, 231, 120, 312, 315, 319	splval2 14470	. . . 4 ⊢ (𝜑 → ((𝑆‘𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀‘𝑈)”⟩⟩) = ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
321	297	simpld 495	. . . . . . . 8 ⊢ (𝜑 → ⟨“𝑈(𝑀‘𝑈)”⟩ = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩))
322	321	oveq2d 7291	. . . . . . 7 ⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
323		ccatpfx 14414	. . . . . . . 8 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿)))) → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = ((𝐵‘𝐿) prefix 𝑃))
324	30, 278, 282, 323	syl3anc 1370	. . . . . . 7 ⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = ((𝐵‘𝐿) prefix 𝑃))
325	322, 324	eqtrd 2778	. . . . . 6 ⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) = ((𝐵‘𝐿) prefix 𝑃))
326	325	oveq1d 7290	. . . . 5 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑃) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
327		ccatpfx 14414	. . . . . 6 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿)))) → (((𝐵‘𝐿) prefix 𝑃) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))))
328	30, 282, 256, 327	syl3anc 1370	. . . . 5 ⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑃) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))))
329		pfxid 14397	. . . . . 6 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))) = (𝐵‘𝐿))
330	30, 329	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))) = (𝐵‘𝐿))
331	326, 328, 330	3eqtrd 2782	. . . 4 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (𝐵‘𝐿))
332	227, 320, 331	3eqtrd 2782	. . 3 ⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = (𝐵‘𝐿))
333		fnovrn 7447	. . . 4 ⊢ (((𝑇‘(𝑆‘𝐶)) Fn ((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝑆‘𝐶))) ∧ 𝑈 ∈ (𝐼 × 2o)) → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) ∈ ran (𝑇‘(𝑆‘𝐶)))
334	218, 225, 117, 333	syl3anc 1370	. . 3 ⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) ∈ ran (𝑇‘(𝑆‘𝐶)))
335	332, 334	eqeltrrd 2840	. 2 ⊢ (𝜑 → (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶)))
336	221, 335	jca 512	1 ⊢ (𝜑 → ((𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶)) ∧ (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ∀wral 3064  {crab 3068   ∖ cdif 3884  ∅c0 4256  {csn 4561  ⟨cop 4567  ⟨cotp 4569  ∪ ciun 4924   class class class wbr 5074   ↦ cmpt 5157   I cid 5488   × cxp 5587  dom cdm 5589  ran crn 5590   Fn wfn 6428  ⟶wf 6429  ‘cfv 6433  (class class class)co 7275   ∈ cmpo 7277  1_oc1o 8290  2_oc2o 8291  ℂcc 10869  ℝcr 10870  0cc0 10871  1c1 10872   + caddc 10874   < clt 11009   ≤ cle 11010   − cmin 11205  2c2 12028  ℕ₀cn0 12233  ℤcz 12319  ℤ_≥cuz 12582  ...cfz 13239  ..^cfzo 13382  ♯chash 14044  Word cword 14217   ++ cconcat 14273   substr csubstr 14353   prefix cpfx 14383   splice csplice 14462  ⟨“cs2 14554   ~_FG cefg 19312

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-ot 4570  df-uni 4840  df-int 4880  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-2o 8298  df-er 8498  df-map 8617  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-card 9697  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-nn 11974  df-2 12036  df-n0 12234  df-z 12320  df-uz 12583  df-fz 13240  df-fzo 13383  df-hash 14045  df-word 14218  df-concat 14274  df-s1 14301  df-substr 14354  df-pfx 14384  df-splice 14463  df-s2 14561

This theorem is referenced by:  efgredlemd  19350