Theorem efgredleme 19904

Description: Lemma for efgred 19909. (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 19890	. . . . . . . 8 ⊢ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊
9	8	fdmi 6710	. . . . . . . . 9 ⊢ dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}
10	9	feq2i 6690	. . . . . . . 8 ⊢ (𝑆:dom 𝑆⟶𝑊 ↔ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊)
11	8, 10	mpbir 234	. . . . . . 7 ⊢ 𝑆:dom 𝑆⟶𝑊
12	11	ffvelcdmi 7072	. . . . . 6 ⊢ (𝐶 ∈ dom 𝑆 → (𝑆‘𝐶) ∈ 𝑊)
13	1, 12	syl 18	. . . . 5 ⊢ (𝜑 → (𝑆‘𝐶) ∈ 𝑊)
14		efgredlemb.q	. . . . . . 7 ⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))))
15		elfzuz 13607	. . . . . . 7 ⊢ (𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) → 𝑄 ∈ (ℤ≥‘0))
16	14, 15	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑄 ∈ (ℤ≥‘0))
17		efgredlemd.sc	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
18	17	fveq2d 6878	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(𝑆‘𝐶)) = (♯‘(((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))))
19		fviss 6951	. . . . . . . . . . . . 13 ⊢ ( I ‘Word (𝐼 × 2o)) ⊆ Word (𝐼 × 2o)
20	2, 19	eqsstri 3977	. . . . . . . . . . . 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 19902	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝐾) ∈ 𝑊 ∧ (𝐵‘𝐿) ∈ 𝑊))
29	28	simprd 501	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵‘𝐿) ∈ 𝑊)
30	20, 29	sselid 3929	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵‘𝐿) ∈ Word (𝐼 × 2o))
31		pfxcl 14780	. . . . . . . . . . 11 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o))
32	30, 31	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o))
33	28	simpld 500	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴‘𝐾) ∈ 𝑊)
34	20, 33	sselid 3929	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴‘𝐾) ∈ Word (𝐼 × 2o))
35		swrdcl 14746	. . . . . . . . . . 11 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2o))
36	34, 35	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2o))
37		ccatlen 14673	. . . . . . . . . 10 ⊢ ((((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2o)) → (♯‘(((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))) = ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))))
38	32, 36, 37	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))) = ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))))
39		pfxlen 14786	. . . . . . . . . . . 12 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) prefix 𝑄)) = 𝑄)
40	30, 14, 39	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) prefix 𝑄)) = 𝑄)
41		2nn0 12578	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ0
42		uzaddcl 12986	. . . . . . . . . . . . . 14 ⊢ ((𝑄 ∈ (ℤ≥‘0) ∧ 2 ∈ ℕ0) → (𝑄 + 2) ∈ (ℤ≥‘0))
43	16, 41, 42	sylancl 598	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄 + 2) ∈ (ℤ≥‘0))
44		efgredlemb.p	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))))
45		elfzuz3 13608	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘𝑃))
46	44, 45	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘𝑃))
47		efgredlemd.9	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(𝑄 + 2)))
48		uztrn 12938	. . . . . . . . . . . . . 14 ⊢ (((♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘𝑃) ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘(𝑄 + 2)))
49	46, 47, 48	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘(𝑄 + 2)))
50		elfzuzb 13605	. . . . . . . . . . . . 13 ⊢ ((𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾))) ↔ ((𝑄 + 2) ∈ (ℤ≥‘0) ∧ (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘(𝑄 + 2))))
51	43, 49, 50	sylanbrc 595	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾))))
52		lencl 14631	. . . . . . . . . . . . . . 15 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → (♯‘(𝐴‘𝐾)) ∈ ℕ0)
53	34, 52	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ ℕ0)
54		nn0uz 12958	. . . . . . . . . . . . . 14 ⊢ ℕ0 = (ℤ≥‘0)
55	53, 54	eleqtrdi 2870	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘0))
56		eluzfz2 13619	. . . . . . . . . . . . 13 ⊢ ((♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘0) → (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾))))
57	55, 56	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾))))
58		swrdlen 14748	. . . . . . . . . . . 12 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾))) ∧ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((♯‘(𝐴‘𝐾)) − (𝑄 + 2)))
59	34, 51, 57, 58	syl3anc 1398	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((♯‘(𝐴‘𝐾)) − (𝑄 + 2)))
60	40, 59	oveq12d 7427	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))) = (𝑄 + ((♯‘(𝐴‘𝐾)) − (𝑄 + 2))))
61	14	elfzelzd 13612	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ ℤ)
62	61	zcnd 12759	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ ℂ)
63	53	nn0cnd 12624	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ ℂ)
64		2z 12683	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℤ
65		zaddcl 12691	. . . . . . . . . . . . 13 ⊢ ((𝑄 ∈ ℤ ∧ 2 ∈ ℤ) → (𝑄 + 2) ∈ ℤ)
66	61, 64, 65	sylancl 598	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄 + 2) ∈ ℤ)
67	66	zcnd 12759	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄 + 2) ∈ ℂ)
68	62, 63, 67	addsubassd 11646	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑄 + (♯‘(𝐴‘𝐾))) − (𝑄 + 2)) = (𝑄 + ((♯‘(𝐴‘𝐾)) − (𝑄 + 2))))
69		2cn 12373	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
70	69	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℂ)
71	62, 63, 70	pnpcand 11663	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑄 + (♯‘(𝐴‘𝐾))) − (𝑄 + 2)) = ((♯‘(𝐴‘𝐾)) − 2))
72	60, 68, 71	3eqtr2d 2801	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))) = ((♯‘(𝐴‘𝐾)) − 2))
73	18, 38, 72	3eqtrd 2799	. . . . . . . 8 ⊢ (𝜑 → (♯‘(𝑆‘𝐶)) = ((♯‘(𝐴‘𝐾)) − 2))
74	44	elfzelzd 13612	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ ℤ)
75		zsubcl 12693	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℤ ∧ 2 ∈ ℤ) → (𝑃 − 2) ∈ ℤ)
76	74, 64, 75	sylancl 598	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 − 2) ∈ ℤ)
77	64	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 2 ∈ ℤ)
78	74	zcnd 12759	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℂ)
79		npcan 11523	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑃 − 2) + 2) = 𝑃)
80	78, 69, 79	sylancl 598	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑃 − 2) + 2) = 𝑃)
81	80	fveq2d 6878	. . . . . . . . . 10 ⊢ (𝜑 → (ℤ≥‘((𝑃 − 2) + 2)) = (ℤ≥‘𝑃))
82	46, 81	eleqtrrd 2863	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘((𝑃 − 2) + 2)))
83		eluzsub 12950	. . . . . . . . 9 ⊢ (((𝑃 − 2) ∈ ℤ ∧ 2 ∈ ℤ ∧ (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘((𝑃 − 2) + 2))) → ((♯‘(𝐴‘𝐾)) − 2) ∈ (ℤ≥‘(𝑃 − 2)))
84	76, 77, 82, 83	syl3anc 1398	. . . . . . . 8 ⊢ (𝜑 → ((♯‘(𝐴‘𝐾)) − 2) ∈ (ℤ≥‘(𝑃 − 2)))
85	73, 84	eqeltrd 2860	. . . . . . 7 ⊢ (𝜑 → (♯‘(𝑆‘𝐶)) ∈ (ℤ≥‘(𝑃 − 2)))
86		eluzsub 12950	. . . . . . . 8 ⊢ ((𝑄 ∈ ℤ ∧ 2 ∈ ℤ ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) → (𝑃 − 2) ∈ (ℤ≥‘𝑄))
87	61, 77, 47, 86	syl3anc 1398	. . . . . . 7 ⊢ (𝜑 → (𝑃 − 2) ∈ (ℤ≥‘𝑄))
88		uztrn 12938	. . . . . . 7 ⊢ (((♯‘(𝑆‘𝐶)) ∈ (ℤ≥‘(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (ℤ≥‘𝑄)) → (♯‘(𝑆‘𝐶)) ∈ (ℤ≥‘𝑄))
89	85, 87, 88	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (♯‘(𝑆‘𝐶)) ∈ (ℤ≥‘𝑄))
90		elfzuzb 13605	. . . . . 6 ⊢ (𝑄 ∈ (0...(♯‘(𝑆‘𝐶))) ↔ (𝑄 ∈ (ℤ≥‘0) ∧ (♯‘(𝑆‘𝐶)) ∈ (ℤ≥‘𝑄)))
91	16, 89, 90	sylanbrc 595	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝑆‘𝐶))))
92		efgredlemb.v	. . . . 5 ⊢ (𝜑 → 𝑉 ∈ (𝐼 × 2o))
93	2, 3, 4, 5	efgtval 19884	. . . . 5 ⊢ (((𝑆‘𝐶) ∈ 𝑊 ∧ 𝑄 ∈ (0...(♯‘(𝑆‘𝐶))) ∧ 𝑉 ∈ (𝐼 × 2o)) → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = ((𝑆‘𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩))
94	13, 91, 92, 93	syl3anc 1398	. . . 4 ⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = ((𝑆‘𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩))
95		pfxcl 14780	. . . . . 6 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o))
96	34, 95	syl 18	. . . . 5 ⊢ (𝜑 → ((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o))
97		wrd0 14637	. . . . . 6 ⊢ ∅ ∈ Word (𝐼 × 2o)
98	97	a1i 11	. . . . 5 ⊢ (𝜑 → ∅ ∈ Word (𝐼 × 2o))
99	4	efgmf 19874	. . . . . . . 8 ⊢ 𝑀:(𝐼 × 2o)⟶(𝐼 × 2o)
100	99	ffvelcdmi 7072	. . . . . . 7 ⊢ (𝑉 ∈ (𝐼 × 2o) → (𝑀‘𝑉) ∈ (𝐼 × 2o))
101	92, 100	syl 18	. . . . . 6 ⊢ (𝜑 → (𝑀‘𝑉) ∈ (𝐼 × 2o))
102	92, 101	s2cld 14975	. . . . 5 ⊢ (𝜑 → ⟨“𝑉(𝑀‘𝑉)”⟩ ∈ Word (𝐼 × 2o))
103	61	zred 12758	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄 ∈ ℝ)
104		nn0addge1 12607	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄 ∈ ℝ ∧ 2 ∈ ℕ0) → 𝑄 ≤ (𝑄 + 2))
105	103, 41, 104	sylancl 598	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑄 ≤ (𝑄 + 2))
106		eluz2 12926	. . . . . . . . . . . . . . . 16 ⊢ ((𝑄 + 2) ∈ (ℤ≥‘𝑄) ↔ (𝑄 ∈ ℤ ∧ (𝑄 + 2) ∈ ℤ ∧ 𝑄 ≤ (𝑄 + 2)))
107	61, 66, 105, 106	syl3anbrc 1362	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑄 + 2) ∈ (ℤ≥‘𝑄))
108		uztrn 12938	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℤ≥‘(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (ℤ≥‘𝑄)) → 𝑃 ∈ (ℤ≥‘𝑄))
109	47, 107, 108	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘𝑄))
110		elfzuzb 13605	. . . . . . . . . . . . . 14 ⊢ (𝑄 ∈ (0...𝑃) ↔ (𝑄 ∈ (ℤ≥‘0) ∧ 𝑃 ∈ (ℤ≥‘𝑄)))
111	16, 109, 110	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∈ (0...𝑃))
112		ccatpfx 14803	. . . . . . . . . . . . 13 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾)))) → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) = ((𝐴‘𝐾) prefix 𝑃))
113	34, 111, 44, 112	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) = ((𝐴‘𝐾) prefix 𝑃))
114	113	oveq1d 7424	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) prefix 𝑃) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))))
115		pfxcl 14780	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) prefix 𝑃) ∈ Word (𝐼 × 2o))
116	34, 115	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) prefix 𝑃) ∈ Word (𝐼 × 2o))
117		efgredlemb.u	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ∈ (𝐼 × 2o))
118	99	ffvelcdmi 7072	. . . . . . . . . . . . . 14 ⊢ (𝑈 ∈ (𝐼 × 2o) → (𝑀‘𝑈) ∈ (𝐼 × 2o))
119	117, 118	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀‘𝑈) ∈ (𝐼 × 2o))
120	117, 119	s2cld 14975	. . . . . . . . . . . 12 ⊢ (𝜑 → ⟨“𝑈(𝑀‘𝑈)”⟩ ∈ Word (𝐼 × 2o))
121		swrdcl 14746	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2o))
122	34, 121	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2o))
123		ccatass 14687	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝐾) prefix 𝑃) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑈(𝑀‘𝑈)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2o)) → ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐴‘𝐾) prefix 𝑃) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))))
124	116, 120, 122, 123	syl3anc 1398	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐴‘𝐾) prefix 𝑃) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))))
125		efgredlemb.6	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈))
126	2, 3, 4, 5	efgtval 19884	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝐾) ∈ 𝑊 ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ 𝑈 ∈ (𝐼 × 2o)) → (𝑃(𝑇‘(𝐴‘𝐾))𝑈) = ((𝐴‘𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀‘𝑈)”⟩⟩))
127	33, 44, 117, 126	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃(𝑇‘(𝐴‘𝐾))𝑈) = ((𝐴‘𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀‘𝑈)”⟩⟩))
128		splval 14853	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝐾) ∈ 𝑊 ∧ (𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ ⟨“𝑈(𝑀‘𝑈)”⟩ ∈ Word (𝐼 × 2o))) → ((𝐴‘𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀‘𝑈)”⟩⟩) = ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))
129	33, 44, 44, 120, 128	syl13anc 1399	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀‘𝑈)”⟩⟩) = ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))
130	125, 127, 129	3eqtrd 2799	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘𝐴) = ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))
131		efgredlemb.7	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉))
132	2, 3, 4, 5	efgtval 19884	. . . . . . . . . . . . . 14 ⊢ (((𝐵‘𝐿) ∈ 𝑊 ∧ 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ 𝑉 ∈ (𝐼 × 2o)) → (𝑄(𝑇‘(𝐵‘𝐿))𝑉) = ((𝐵‘𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩))
133	29, 14, 92, 132	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄(𝑇‘(𝐵‘𝐿))𝑉) = ((𝐵‘𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩))
134		splval 14853	. . . . . . . . . . . . . 14 ⊢ (((𝐵‘𝐿) ∈ 𝑊 ∧ (𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ ⟨“𝑉(𝑀‘𝑉)”⟩ ∈ Word (𝐼 × 2o))) → ((𝐵‘𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
135	29, 14, 14, 102, 134	syl13anc 1399	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵‘𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
136	131, 133, 135	3eqtrd 2799	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘𝐵) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
137	24, 130, 136	3eqtr3d 2803	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
138	114, 124, 137	3eqtr2d 2801	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
139		swrdcl 14746	. . . . . . . . . . . 12 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2o))
140	34, 139	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2o))
141		ccatcl 14672	. . . . . . . . . . . 12 ⊢ ((⟨“𝑈(𝑀‘𝑈)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2o)) → (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2o))
142	120, 122, 141	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2o))
143		ccatass 14687	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2o)) → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))))
144	96, 140, 142, 143	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))))
145		swrdcl 14746	. . . . . . . . . . . 12 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o))
146	30, 145	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o))
147		ccatass 14687	. . . . . . . . . . 11 ⊢ ((((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑉(𝑀‘𝑉)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o)) → ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
148	32, 102, 146, 147	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
149	138, 144, 148	3eqtr3d 2803	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))) = (((𝐵‘𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
150		ccatcl 14672	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2o)) → (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2o))
151	140, 142, 150	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2o))
152		ccatcl 14672	. . . . . . . . . . 11 ⊢ ((⟨“𝑉(𝑀‘𝑉)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o)) → (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) ∈ Word (𝐼 × 2o))
153	102, 146, 152	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) ∈ Word (𝐼 × 2o))
154		uztrn 12938	. . . . . . . . . . . . . 14 ⊢ (((♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘𝑃) ∧ 𝑃 ∈ (ℤ≥‘𝑄)) → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘𝑄))
155	46, 109, 154	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘𝑄))
156		elfzuzb 13605	. . . . . . . . . . . . 13 ⊢ (𝑄 ∈ (0...(♯‘(𝐴‘𝐾))) ↔ (𝑄 ∈ (ℤ≥‘0) ∧ (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘𝑄)))
157	16, 155, 156	sylanbrc 595	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝐴‘𝐾))))
158		pfxlen 14786	. . . . . . . . . . . 12 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) prefix 𝑄)) = 𝑄)
159	34, 157, 158	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) prefix 𝑄)) = 𝑄)
160	159, 40	eqtr4d 2798	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) prefix 𝑄)) = (♯‘((𝐵‘𝐿) prefix 𝑄)))
161		ccatopth 14818	. . . . . . . . . 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 1408	. . . . . . . . 9 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))) = (((𝐵‘𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))) ↔ (((𝐴‘𝐾) prefix 𝑄) = ((𝐵‘𝐿) prefix 𝑄) ∧ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))))
163	149, 162	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) = ((𝐵‘𝐿) prefix 𝑄) ∧ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
164	163	simpld 500	. . . . . . 7 ⊢ (𝜑 → ((𝐴‘𝐾) prefix 𝑄) = ((𝐵‘𝐿) prefix 𝑄))
165	164	oveq1d 7424	. . . . . 6 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
166		ccatrid 14686	. . . . . . . 8 ⊢ (((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o) → (((𝐴‘𝐾) prefix 𝑄) ++ ∅) = ((𝐴‘𝐾) prefix 𝑄))
167	96, 166	syl 18	. . . . . . 7 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ∅) = ((𝐴‘𝐾) prefix 𝑄))
168	167	oveq1d 7424	. . . . . 6 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ∅) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
169	165, 168, 17	3eqtr4rd 2806	. . . . 5 ⊢ (𝜑 → (𝑆‘𝐶) = ((((𝐴‘𝐾) prefix 𝑄) ++ ∅) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
170	159	eqcomd 2766	. . . . 5 ⊢ (𝜑 → 𝑄 = (♯‘((𝐴‘𝐾) prefix 𝑄)))
171		hash0 14464	. . . . . . 7 ⊢ (♯‘∅) = 0
172	171	oveq2i 7420	. . . . . 6 ⊢ (𝑄 + (♯‘∅)) = (𝑄 + 0)
173	62	addridd 11467	. . . . . 6 ⊢ (𝜑 → (𝑄 + 0) = 𝑄)
174	172, 173	eqtr2id 2808	. . . . 5 ⊢ (𝜑 → 𝑄 = (𝑄 + (♯‘∅)))
175	96, 98, 36, 102, 169, 170, 174	splval2 14859	. . . 4 ⊢ (𝜑 → ((𝑆‘𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩) = ((((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
176		elfzuzb 13605	. . . . . . . . . . . . . 14 ⊢ (𝑄 ∈ (0...(𝑄 + 2)) ↔ (𝑄 ∈ (ℤ≥‘0) ∧ (𝑄 + 2) ∈ (ℤ≥‘𝑄)))
177	16, 107, 176	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∈ (0...(𝑄 + 2)))
178		elfzuzb 13605	. . . . . . . . . . . . . 14 ⊢ ((𝑄 + 2) ∈ (0...𝑃) ↔ ((𝑄 + 2) ∈ (ℤ≥‘0) ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))))
179	43, 47, 178	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄 + 2) ∈ (0...𝑃))
180		ccatswrd 14771	. . . . . . . . . . . . 13 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))))) → (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩))
181	34, 177, 179, 44, 180	syl13anc 1399	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩))
182	181	oveq1d 7424	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))))
183		swrdcl 14746	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2o))
184	34, 183	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2o))
185		swrdcl 14746	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2o))
186	34, 185	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2o))
187		ccatass 14687	. . . . . . . . . . . 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 1398	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))))
189	163	simprd 501	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
190	182, 188, 189	3eqtr3d 2803	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
191		ccatcl 14672	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2o)) → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2o))
192	186, 142, 191	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2o))
193		swrdlen 14748	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝑄 + 2) − 𝑄))
194	34, 177, 51, 193	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝑄 + 2) − 𝑄))
195		pncan2 11521	. . . . . . . . . . . . . 14 ⊢ ((𝑄 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑄 + 2) − 𝑄) = 2)
196	62, 69, 195	sylancl 598	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑄 + 2) − 𝑄) = 2)
197	194, 196	eqtrd 2795	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = 2)
198		s2len 14993	. . . . . . . . . . . 12 ⊢ (♯‘⟨“𝑉(𝑀‘𝑉)”⟩) = 2
199	197, 198	eqtr4di 2813	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (♯‘⟨“𝑉(𝑀‘𝑉)”⟩))
200		ccatopth 14818	. . . . . . . . . . 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 1408	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) ↔ (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀‘𝑉)”⟩ ∧ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
202	190, 201	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀‘𝑉)”⟩ ∧ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
203	202	simpld 500	. . . . . . . 8 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀‘𝑉)”⟩)
204	203	oveq2d 7425	. . . . . . 7 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩))
205		ccatpfx 14803	. . . . . . . 8 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾)))) → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝐴‘𝐾) prefix (𝑄 + 2)))
206	34, 177, 51, 205	syl3anc 1398	. . . . . . 7 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝐴‘𝐾) prefix (𝑄 + 2)))
207	204, 206	eqtr3d 2797	. . . . . 6 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) = ((𝐴‘𝐾) prefix (𝑄 + 2)))
208	207	oveq1d 7424	. . . . 5 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (((𝐴‘𝐾) prefix (𝑄 + 2)) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
209		ccatpfx 14803	. . . . . 6 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾))) ∧ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾)))) → (((𝐴‘𝐾) prefix (𝑄 + 2)) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))))
210	34, 51, 57, 209	syl3anc 1398	. . . . 5 ⊢ (𝜑 → (((𝐴‘𝐾) prefix (𝑄 + 2)) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))))
211		pfxid 14787	. . . . . 6 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))) = (𝐴‘𝐾))
212	34, 211	syl 18	. . . . 5 ⊢ (𝜑 → ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))) = (𝐴‘𝐾))
213	208, 210, 212	3eqtrd 2799	. . . 4 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (𝐴‘𝐾))
214	94, 175, 213	3eqtrd 2799	. . 3 ⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = (𝐴‘𝐾))
215	2, 3, 4, 5	efgtf 19883	. . . . . . 7 ⊢ ((𝑆‘𝐶) ∈ 𝑊 → ((𝑇‘(𝑆‘𝐶)) = (𝑎 ∈ (0...(♯‘(𝑆‘𝐶))), 𝑖 ∈ (𝐼 × 2o) ↦ ((𝑆‘𝐶) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀‘𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆‘𝐶)):((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o))⟶𝑊))
216	13, 215	syl 18	. . . . . 6 ⊢ (𝜑 → ((𝑇‘(𝑆‘𝐶)) = (𝑎 ∈ (0...(♯‘(𝑆‘𝐶))), 𝑖 ∈ (𝐼 × 2o) ↦ ((𝑆‘𝐶) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀‘𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆‘𝐶)):((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o))⟶𝑊))
217	216	simprd 501	. . . . 5 ⊢ (𝜑 → (𝑇‘(𝑆‘𝐶)):((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o))⟶𝑊)
218	217	ffnd 6699	. . . 4 ⊢ (𝜑 → (𝑇‘(𝑆‘𝐶)) Fn ((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o)))
219		fnovrn 7585	. . . 4 ⊢ (((𝑇‘(𝑆‘𝐶)) Fn ((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o)) ∧ 𝑄 ∈ (0...(♯‘(𝑆‘𝐶))) ∧ 𝑉 ∈ (𝐼 × 2o)) → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) ∈ ran (𝑇‘(𝑆‘𝐶)))
220	218, 91, 92, 219	syl3anc 1398	. . 3 ⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) ∈ ran (𝑇‘(𝑆‘𝐶)))
221	214, 220	eqeltrrd 2861	. 2 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶)))
222		uztrn 12938	. . . . . . 7 ⊢ (((𝑃 − 2) ∈ (ℤ≥‘𝑄) ∧ 𝑄 ∈ (ℤ≥‘0)) → (𝑃 − 2) ∈ (ℤ≥‘0))
223	87, 16, 222	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (𝑃 − 2) ∈ (ℤ≥‘0))
224		elfzuzb 13605	. . . . . 6 ⊢ ((𝑃 − 2) ∈ (0...(♯‘(𝑆‘𝐶))) ↔ ((𝑃 − 2) ∈ (ℤ≥‘0) ∧ (♯‘(𝑆‘𝐶)) ∈ (ℤ≥‘(𝑃 − 2))))
225	223, 85, 224	sylanbrc 595	. . . . 5 ⊢ (𝜑 → (𝑃 − 2) ∈ (0...(♯‘(𝑆‘𝐶))))
226	2, 3, 4, 5	efgtval 19884	. . . . 5 ⊢ (((𝑆‘𝐶) ∈ 𝑊 ∧ (𝑃 − 2) ∈ (0...(♯‘(𝑆‘𝐶))) ∧ 𝑈 ∈ (𝐼 × 2o)) → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = ((𝑆‘𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀‘𝑈)”⟩⟩))
227	13, 225, 117, 226	syl3anc 1398	. . . 4 ⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = ((𝑆‘𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀‘𝑈)”⟩⟩))
228		pfxcl 14780	. . . . . 6 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2o))
229	30, 228	syl 18	. . . . 5 ⊢ (𝜑 → ((𝐵‘𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2o))
230		swrdcl 14746	. . . . . 6 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o))
231	30, 230	syl 18	. . . . 5 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o))
232		ccatswrd 14771	. . . . . . . . . . 11 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ ((𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾))))) → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))
233	34, 179, 44, 57, 232	syl13anc 1399	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))
234	202	simprd 501	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))
235		elfzuzb 13605	. . . . . . . . . . . . . . . 16 ⊢ (𝑄 ∈ (0...(𝑃 − 2)) ↔ (𝑄 ∈ (ℤ≥‘0) ∧ (𝑃 − 2) ∈ (ℤ≥‘𝑄)))
236	16, 87, 235	sylanbrc 595	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑄 ∈ (0...(𝑃 − 2)))
237	2, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27, 44, 14, 117, 92, 125, 131	efgredlemg 19903	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) = (♯‘(𝐵‘𝐿)))
238	237, 46	eqeltrrd 2861	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘𝑃))
239		0le2 12400	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ≤ 2
240	239	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 ≤ 2)
241	74	zred 12758	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑃 ∈ ℝ)
242		2re 12372	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℝ
243		subge02 11787	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃 ∈ ℝ ∧ 2 ∈ ℝ) → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃))
244	241, 242, 243	sylancl 598	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃))
245	240, 244	mpbid 235	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑃 − 2) ≤ 𝑃)
246		eluz2 12926	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ (ℤ≥‘(𝑃 − 2)) ↔ ((𝑃 − 2) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑃 − 2) ≤ 𝑃))
247	76, 74, 245, 246	syl3anbrc 1362	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(𝑃 − 2)))
248		uztrn 12938	. . . . . . . . . . . . . . . . 17 ⊢ (((♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘𝑃) ∧ 𝑃 ∈ (ℤ≥‘(𝑃 − 2))) → (♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘(𝑃 − 2)))
249	238, 247, 248	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘(𝑃 − 2)))
250		elfzuzb 13605	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿))) ↔ ((𝑃 − 2) ∈ (ℤ≥‘0) ∧ (♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘(𝑃 − 2))))
251	223, 249, 250	sylanbrc 595	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿))))
252		lencl 14631	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → (♯‘(𝐵‘𝐿)) ∈ ℕ0)
253	30, 252	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ ℕ0)
254	253, 54	eleqtrdi 2870	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘0))
255		eluzfz2 13619	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘0) → (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))
256	254, 255	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))
257		ccatswrd 14771	. . . . . . . . . . . . . . 15 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿))) ∧ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))) → (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))
258	30, 236, 251, 256, 257	syl13anc 1399	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))
259	234, 258	eqtr4d 2798	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)))
260		swrdcl 14746	. . . . . . . . . . . . . . 15 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2o))
261	30, 260	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2o))
262		swrdcl 14746	. . . . . . . . . . . . . . 15 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o))
263	30, 262	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o))
264		swrdlen 14748	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (𝑃 − (𝑄 + 2)))
265	34, 179, 44, 264	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (𝑃 − (𝑄 + 2)))
266		swrdlen 14748	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝑃 − 2) − 𝑄))
267	30, 236, 251, 266	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝑃 − 2) − 𝑄))
268	78, 62, 70	sub32d 11658	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑃 − 𝑄) − 2) = ((𝑃 − 2) − 𝑄))
269	78, 62, 70	subsub4d 11657	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑃 − 𝑄) − 2) = (𝑃 − (𝑄 + 2)))
270	267, 268, 269	3eqtr2d 2801	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = (𝑃 − (𝑄 + 2)))
271	265, 270	eqtr4d 2798	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (♯‘((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)))
272		ccatopth 14818	. . . . . . . . . . . . . 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 1408	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)) ↔ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩))))
274	259, 273	mpbid 235	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)))
275	274	simpld 500	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩))
276	274	simprd 501	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩))
277		elfzuzb 13605	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 − 2) ∈ (0...𝑃) ↔ ((𝑃 − 2) ∈ (ℤ≥‘0) ∧ 𝑃 ∈ (ℤ≥‘(𝑃 − 2))))
278	223, 247, 277	sylanbrc 595	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 − 2) ∈ (0...𝑃))
279		elfzuz 13607	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) → 𝑃 ∈ (ℤ≥‘0))
280	44, 279	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘0))
281		elfzuzb 13605	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ (0...(♯‘(𝐵‘𝐿))) ↔ (𝑃 ∈ (ℤ≥‘0) ∧ (♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘𝑃)))
282	280, 238, 281	sylanbrc 595	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ (0...(♯‘(𝐵‘𝐿))))
283		ccatswrd 14771	. . . . . . . . . . . . . . 15 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ ((𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))) → (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩))
284	30, 278, 282, 256, 283	syl13anc 1399	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩))
285	276, 284	eqtr4d 2798	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
286		swrdcl 14746	. . . . . . . . . . . . . . 15 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2o))
287	30, 286	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2o))
288		s2len 14993	. . . . . . . . . . . . . . 15 ⊢ (♯‘⟨“𝑈(𝑀‘𝑈)”⟩) = 2
289		swrdlen 14748	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = (𝑃 − (𝑃 − 2)))
290	30, 278, 282, 289	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = (𝑃 − (𝑃 − 2)))
291		nncan 11544	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑃 − (𝑃 − 2)) = 2)
292	78, 69, 291	sylancl 598	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃 − (𝑃 − 2)) = 2)
293	290, 292	eqtr2d 2796	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 = (♯‘((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
294	288, 293	eqtrid 2807	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘⟨“𝑈(𝑀‘𝑈)”⟩) = (♯‘((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
295		ccatopth 14818	. . . . . . . . . . . . . 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 1408	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) ↔ (⟨“𝑈(𝑀‘𝑈)”⟩ = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) = ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))))
297	285, 296	mpbid 235	. . . . . . . . . . . 12 ⊢ (𝜑 → (⟨“𝑈(𝑀‘𝑈)”⟩ = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) = ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
298	297	simprd 501	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) = ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))
299	275, 298	oveq12d 7427	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
300	233, 299	eqtr3d 2797	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩) = (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
301	300	oveq2d 7425	. . . . . . . 8 ⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))))
302		ccatass 14687	. . . . . . . . 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 1398	. . . . . . . 8 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))))
304	301, 303	eqtr4d 2798	. . . . . . 7 ⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
305		ccatpfx 14803	. . . . . . . . 9 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿)))) → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝐵‘𝐿) prefix (𝑃 − 2)))
306	30, 236, 251, 305	syl3anc 1398	. . . . . . . 8 ⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝐵‘𝐿) prefix (𝑃 − 2)))
307	306	oveq1d 7424	. . . . . . 7 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
308	17, 304, 307	3eqtrd 2799	. . . . . 6 ⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
309		ccatrid 14686	. . . . . . . 8 ⊢ (((𝐵‘𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2o) → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) = ((𝐵‘𝐿) prefix (𝑃 − 2)))
310	229, 309	syl 18	. . . . . . 7 ⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) = ((𝐵‘𝐿) prefix (𝑃 − 2)))
311	310	oveq1d 7424	. . . . . 6 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
312	308, 311	eqtr4d 2798	. . . . 5 ⊢ (𝜑 → (𝑆‘𝐶) = ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
313		pfxlen 14786	. . . . . . 7 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) prefix (𝑃 − 2))) = (𝑃 − 2))
314	30, 251, 313	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) prefix (𝑃 − 2))) = (𝑃 − 2))
315	314	eqcomd 2766	. . . . 5 ⊢ (𝜑 → (𝑃 − 2) = (♯‘((𝐵‘𝐿) prefix (𝑃 − 2))))
316	171	oveq2i 7420	. . . . . 6 ⊢ ((𝑃 − 2) + (♯‘∅)) = ((𝑃 − 2) + 0)
317	76	zcnd 12759	. . . . . . 7 ⊢ (𝜑 → (𝑃 − 2) ∈ ℂ)
318	317	addridd 11467	. . . . . 6 ⊢ (𝜑 → ((𝑃 − 2) + 0) = (𝑃 − 2))
319	316, 318	eqtr2id 2808	. . . . 5 ⊢ (𝜑 → (𝑃 − 2) = ((𝑃 − 2) + (♯‘∅)))
320	229, 98, 231, 120, 312, 315, 319	splval2 14859	. . . 4 ⊢ (𝜑 → ((𝑆‘𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀‘𝑈)”⟩⟩) = ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
321	297	simpld 500	. . . . . . . 8 ⊢ (𝜑 → ⟨“𝑈(𝑀‘𝑈)”⟩ = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩))
322	321	oveq2d 7425	. . . . . . 7 ⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
323		ccatpfx 14803	. . . . . . . 8 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿)))) → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = ((𝐵‘𝐿) prefix 𝑃))
324	30, 278, 282, 323	syl3anc 1398	. . . . . . 7 ⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = ((𝐵‘𝐿) prefix 𝑃))
325	322, 324	eqtrd 2795	. . . . . 6 ⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) = ((𝐵‘𝐿) prefix 𝑃))
326	325	oveq1d 7424	. . . . 5 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑃) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
327		ccatpfx 14803	. . . . . 6 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿)))) → (((𝐵‘𝐿) prefix 𝑃) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))))
328	30, 282, 256, 327	syl3anc 1398	. . . . 5 ⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑃) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))))
329		pfxid 14787	. . . . . 6 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))) = (𝐵‘𝐿))
330	30, 329	syl 18	. . . . 5 ⊢ (𝜑 → ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))) = (𝐵‘𝐿))
331	326, 328, 330	3eqtrd 2799	. . . 4 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (𝐵‘𝐿))
332	227, 320, 331	3eqtrd 2799	. . 3 ⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = (𝐵‘𝐿))
333		fnovrn 7585	. . . 4 ⊢ (((𝑇‘(𝑆‘𝐶)) Fn ((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝑆‘𝐶))) ∧ 𝑈 ∈ (𝐼 × 2o)) → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) ∈ ran (𝑇‘(𝑆‘𝐶)))
334	218, 225, 117, 333	syl3anc 1398	. . 3 ⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) ∈ ran (𝑇‘(𝑆‘𝐶)))
335	332, 334	eqeltrrd 2861	. 2 ⊢ (𝜑 → (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶)))
336	221, 335	jca 521	1 ⊢ (𝜑 → ((𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶)) ∧ (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3076  {crab 3412   ∖ cdif 3896  ∅c0 4279  {csn 4584  ⟨cop 4590  ⟨cotp 4592  ∪ ciun 4951   class class class wbr 5103   ↦ cmpt 5186   I cid 5542   × cxp 5646  dom cdm 5648  ran crn 5649   Fn wfn 6523  ⟶wf 6524  ‘cfv 6528  (class class class)co 7409   ∈ cmpo 7411  1_oc1o 8448  2_oc2o 8449  ℂcc 11155  ℝcr 11156  0cc0 11157  1c1 11158   + caddc 11160   < clt 11300   ≤ cle 11301   − cmin 11498  2c2 12352  ℕ₀cn0 12561  ℤcz 12648  ℤ_≥cuz 12920  ...cfz 13594  ..^cfzo 13742  ♯chash 14427  Word cword 14611   ++ cconcat 14668   substr csubstr 14741   prefix cpfx 14773   splice csplice 14851  ⟨“cs2 14945   ~_FG cefg 19867

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7735  ax-cnex 11213  ax-resscn 11214  ax-1cn 11215  ax-icn 11216  ax-addcl 11217  ax-addrcl 11218  ax-mulcl 11219  ax-mulrcl 11220  ax-mulcom 11221  ax-addass 11222  ax-mulass 11223  ax-distr 11224  ax-i2m1 11225  ax-1ne0 11226  ax-1rid 11227  ax-rnegex 11228  ax-rrecex 11229  ax-cnre 11230  ax-pre-lttri 11231  ax-pre-lttrn 11232  ax-pre-ltadd 11233  ax-pre-mulgt0 11234

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-ot 4593  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-pred 6294  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-riota 7366  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7862  df-1st 7985  df-2nd 7986  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-1o 8455  df-2o 8456  df-er 8696  df-map 8828  df-en 8953  df-dom 8954  df-sdom 8955  df-fin 8956  df-card 9977  df-pnf 11302  df-mnf 11303  df-xr 11304  df-ltxr 11305  df-le 11306  df-sub 11500  df-neg 11501  df-nn 12291  df-2 12360  df-n0 12562  df-z 12649  df-uz 12921  df-fz 13595  df-fzo 13743  df-hash 14428  df-word 14612  df-concat 14669  df-s1 14696  df-substr 14742  df-pfx 14774  df-splice 14852  df-s2 14952

This theorem is used by:  efgredlemd  19905