Theorem efgredleme 19813

Description: Lemma for efgred 19818. (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 19799	. . . . . . . 8 ⊢ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊
9	8	fdmi 6718	. . . . . . . . 9 ⊢ dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}
10	9	feq2i 6698	. . . . . . . 8 ⊢ (𝑆:dom 𝑆⟶𝑊 ↔ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊)
11	8, 10	mpbir 234	. . . . . . 7 ⊢ 𝑆:dom 𝑆⟶𝑊
12	11	ffvelcdmi 7079	. . . . . 6 ⊢ (𝐶 ∈ dom 𝑆 → (𝑆‘𝐶) ∈ 𝑊)
13	1, 12	syl 18	. . . . 5 ⊢ (𝜑 → (𝑆‘𝐶) ∈ 𝑊)
14		efgredlemb.q	. . . . . . 7 ⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))))
15		elfzuz 13548	. . . . . . 7 ⊢ (𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) → 𝑄 ∈ (ℤ≥‘0))
16	14, 15	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑄 ∈ (ℤ≥‘0))
17		efgredlemd.sc	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
18	17	fveq2d 6886	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(𝑆‘𝐶)) = (♯‘(((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))))
19		fviss 6959	. . . . . . . . . . . . 13 ⊢ ( I ‘Word (𝐼 × 2o)) ⊆ Word (𝐼 × 2o)
20	2, 19	eqsstri 3989	. . . . . . . . . . . 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 19811	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝐾) ∈ 𝑊 ∧ (𝐵‘𝐿) ∈ 𝑊))
29	28	simprd 500	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵‘𝐿) ∈ 𝑊)
30	20, 29	sselid 3941	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵‘𝐿) ∈ Word (𝐼 × 2o))
31		pfxcl 14715	. . . . . . . . . . 11 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o))
32	30, 31	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o))
33	28	simpld 499	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴‘𝐾) ∈ 𝑊)
34	20, 33	sselid 3941	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴‘𝐾) ∈ Word (𝐼 × 2o))
35		swrdcl 14683	. . . . . . . . . . 11 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2o))
36	34, 35	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2o))
37		ccatlen 14612	. . . . . . . . . 10 ⊢ ((((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2o)) → (♯‘(((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))) = ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))))
38	32, 36, 37	syl2anc 595	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))) = ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))))
39		pfxlen 14721	. . . . . . . . . . . 12 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) prefix 𝑄)) = 𝑄)
40	30, 14, 39	syl2anc 595	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) prefix 𝑄)) = 𝑄)
41		2nn0 12521	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ0
42		uzaddcl 12928	. . . . . . . . . . . . . 14 ⊢ ((𝑄 ∈ (ℤ≥‘0) ∧ 2 ∈ ℕ0) → (𝑄 + 2) ∈ (ℤ≥‘0))
43	16, 41, 42	sylancl 597	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄 + 2) ∈ (ℤ≥‘0))
44		efgredlemb.p	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))))
45		elfzuz3 13549	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘𝑃))
46	44, 45	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘𝑃))
47		efgredlemd.9	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(𝑄 + 2)))
48		uztrn 12880	. . . . . . . . . . . . . 14 ⊢ (((♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘𝑃) ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘(𝑄 + 2)))
49	46, 47, 48	syl2anc 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘(𝑄 + 2)))
50		elfzuzb 13546	. . . . . . . . . . . . 13 ⊢ ((𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾))) ↔ ((𝑄 + 2) ∈ (ℤ≥‘0) ∧ (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘(𝑄 + 2))))
51	43, 49, 50	sylanbrc 594	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾))))
52		lencl 14570	. . . . . . . . . . . . . . 15 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → (♯‘(𝐴‘𝐾)) ∈ ℕ0)
53	34, 52	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ ℕ0)
54		nn0uz 12900	. . . . . . . . . . . . . 14 ⊢ ℕ0 = (ℤ≥‘0)
55	53, 54	eleqtrdi 2879	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘0))
56		eluzfz2 13560	. . . . . . . . . . . . 13 ⊢ ((♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘0) → (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾))))
57	55, 56	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾))))
58		swrdlen 14685	. . . . . . . . . . . 12 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾))) ∧ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((♯‘(𝐴‘𝐾)) − (𝑄 + 2)))
59	34, 51, 57, 58	syl3anc 1396	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((♯‘(𝐴‘𝐾)) − (𝑄 + 2)))
60	40, 59	oveq12d 7429	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))) = (𝑄 + ((♯‘(𝐴‘𝐾)) − (𝑄 + 2))))
61	14	elfzelzd 13553	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ ℤ)
62	61	zcnd 12701	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ ℂ)
63	53	nn0cnd 12567	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ ℂ)
64		2z 12626	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℤ
65		zaddcl 12634	. . . . . . . . . . . . 13 ⊢ ((𝑄 ∈ ℤ ∧ 2 ∈ ℤ) → (𝑄 + 2) ∈ ℤ)
66	61, 64, 65	sylancl 597	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄 + 2) ∈ ℤ)
67	66	zcnd 12701	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄 + 2) ∈ ℂ)
68	62, 63, 67	addsubassd 11589	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑄 + (♯‘(𝐴‘𝐾))) − (𝑄 + 2)) = (𝑄 + ((♯‘(𝐴‘𝐾)) − (𝑄 + 2))))
69		2cn 12316	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
70	69	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℂ)
71	62, 63, 70	pnpcand 11606	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑄 + (♯‘(𝐴‘𝐾))) − (𝑄 + 2)) = ((♯‘(𝐴‘𝐾)) − 2))
72	60, 68, 71	3eqtr2d 2810	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))) = ((♯‘(𝐴‘𝐾)) − 2))
73	18, 38, 72	3eqtrd 2808	. . . . . . . 8 ⊢ (𝜑 → (♯‘(𝑆‘𝐶)) = ((♯‘(𝐴‘𝐾)) − 2))
74	44	elfzelzd 13553	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ ℤ)
75		zsubcl 12636	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℤ ∧ 2 ∈ ℤ) → (𝑃 − 2) ∈ ℤ)
76	74, 64, 75	sylancl 597	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 − 2) ∈ ℤ)
77	64	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 2 ∈ ℤ)
78	74	zcnd 12701	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℂ)
79		npcan 11466	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑃 − 2) + 2) = 𝑃)
80	78, 69, 79	sylancl 597	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑃 − 2) + 2) = 𝑃)
81	80	fveq2d 6886	. . . . . . . . . 10 ⊢ (𝜑 → (ℤ≥‘((𝑃 − 2) + 2)) = (ℤ≥‘𝑃))
82	46, 81	eleqtrrd 2872	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘((𝑃 − 2) + 2)))
83		eluzsub 12892	. . . . . . . . 9 ⊢ (((𝑃 − 2) ∈ ℤ ∧ 2 ∈ ℤ ∧ (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘((𝑃 − 2) + 2))) → ((♯‘(𝐴‘𝐾)) − 2) ∈ (ℤ≥‘(𝑃 − 2)))
84	76, 77, 82, 83	syl3anc 1396	. . . . . . . 8 ⊢ (𝜑 → ((♯‘(𝐴‘𝐾)) − 2) ∈ (ℤ≥‘(𝑃 − 2)))
85	73, 84	eqeltrd 2869	. . . . . . 7 ⊢ (𝜑 → (♯‘(𝑆‘𝐶)) ∈ (ℤ≥‘(𝑃 − 2)))
86		eluzsub 12892	. . . . . . . 8 ⊢ ((𝑄 ∈ ℤ ∧ 2 ∈ ℤ ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) → (𝑃 − 2) ∈ (ℤ≥‘𝑄))
87	61, 77, 47, 86	syl3anc 1396	. . . . . . 7 ⊢ (𝜑 → (𝑃 − 2) ∈ (ℤ≥‘𝑄))
88		uztrn 12880	. . . . . . 7 ⊢ (((♯‘(𝑆‘𝐶)) ∈ (ℤ≥‘(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (ℤ≥‘𝑄)) → (♯‘(𝑆‘𝐶)) ∈ (ℤ≥‘𝑄))
89	85, 87, 88	syl2anc 595	. . . . . 6 ⊢ (𝜑 → (♯‘(𝑆‘𝐶)) ∈ (ℤ≥‘𝑄))
90		elfzuzb 13546	. . . . . 6 ⊢ (𝑄 ∈ (0...(♯‘(𝑆‘𝐶))) ↔ (𝑄 ∈ (ℤ≥‘0) ∧ (♯‘(𝑆‘𝐶)) ∈ (ℤ≥‘𝑄)))
91	16, 89, 90	sylanbrc 594	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝑆‘𝐶))))
92		efgredlemb.v	. . . . 5 ⊢ (𝜑 → 𝑉 ∈ (𝐼 × 2o))
93	2, 3, 4, 5	efgtval 19793	. . . . 5 ⊢ (((𝑆‘𝐶) ∈ 𝑊 ∧ 𝑄 ∈ (0...(♯‘(𝑆‘𝐶))) ∧ 𝑉 ∈ (𝐼 × 2o)) → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = ((𝑆‘𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩))
94	13, 91, 92, 93	syl3anc 1396	. . . 4 ⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = ((𝑆‘𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩))
95		pfxcl 14715	. . . . . 6 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o))
96	34, 95	syl 18	. . . . 5 ⊢ (𝜑 → ((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o))
97		wrd0 14576	. . . . . 6 ⊢ ∅ ∈ Word (𝐼 × 2o)
98	97	a1i 11	. . . . 5 ⊢ (𝜑 → ∅ ∈ Word (𝐼 × 2o))
99	4	efgmf 19783	. . . . . . . 8 ⊢ 𝑀:(𝐼 × 2o)⟶(𝐼 × 2o)
100	99	ffvelcdmi 7079	. . . . . . 7 ⊢ (𝑉 ∈ (𝐼 × 2o) → (𝑀‘𝑉) ∈ (𝐼 × 2o))
101	92, 100	syl 18	. . . . . 6 ⊢ (𝜑 → (𝑀‘𝑉) ∈ (𝐼 × 2o))
102	92, 101	s2cld 14908	. . . . 5 ⊢ (𝜑 → ⟨“𝑉(𝑀‘𝑉)”⟩ ∈ Word (𝐼 × 2o))
103	61	zred 12700	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄 ∈ ℝ)
104		nn0addge1 12550	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄 ∈ ℝ ∧ 2 ∈ ℕ0) → 𝑄 ≤ (𝑄 + 2))
105	103, 41, 104	sylancl 597	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑄 ≤ (𝑄 + 2))
106		eluz2 12868	. . . . . . . . . . . . . . . 16 ⊢ ((𝑄 + 2) ∈ (ℤ≥‘𝑄) ↔ (𝑄 ∈ ℤ ∧ (𝑄 + 2) ∈ ℤ ∧ 𝑄 ≤ (𝑄 + 2)))
107	61, 66, 105, 106	syl3anbrc 1360	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑄 + 2) ∈ (ℤ≥‘𝑄))
108		uztrn 12880	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℤ≥‘(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (ℤ≥‘𝑄)) → 𝑃 ∈ (ℤ≥‘𝑄))
109	47, 107, 108	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘𝑄))
110		elfzuzb 13546	. . . . . . . . . . . . . 14 ⊢ (𝑄 ∈ (0...𝑃) ↔ (𝑄 ∈ (ℤ≥‘0) ∧ 𝑃 ∈ (ℤ≥‘𝑄)))
111	16, 109, 110	sylanbrc 594	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∈ (0...𝑃))
112		ccatpfx 14738	. . . . . . . . . . . . 13 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾)))) → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) = ((𝐴‘𝐾) prefix 𝑃))
113	34, 111, 44, 112	syl3anc 1396	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) = ((𝐴‘𝐾) prefix 𝑃))
114	113	oveq1d 7426	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) prefix 𝑃) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))))
115		pfxcl 14715	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) prefix 𝑃) ∈ Word (𝐼 × 2o))
116	34, 115	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) prefix 𝑃) ∈ Word (𝐼 × 2o))
117		efgredlemb.u	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ∈ (𝐼 × 2o))
118	99	ffvelcdmi 7079	. . . . . . . . . . . . . 14 ⊢ (𝑈 ∈ (𝐼 × 2o) → (𝑀‘𝑈) ∈ (𝐼 × 2o))
119	117, 118	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀‘𝑈) ∈ (𝐼 × 2o))
120	117, 119	s2cld 14908	. . . . . . . . . . . 12 ⊢ (𝜑 → ⟨“𝑈(𝑀‘𝑈)”⟩ ∈ Word (𝐼 × 2o))
121		swrdcl 14683	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2o))
122	34, 121	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2o))
123		ccatass 14626	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝐾) prefix 𝑃) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑈(𝑀‘𝑈)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2o)) → ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐴‘𝐾) prefix 𝑃) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))))
124	116, 120, 122, 123	syl3anc 1396	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐴‘𝐾) prefix 𝑃) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))))
125		efgredlemb.6	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈))
126	2, 3, 4, 5	efgtval 19793	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝐾) ∈ 𝑊 ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ 𝑈 ∈ (𝐼 × 2o)) → (𝑃(𝑇‘(𝐴‘𝐾))𝑈) = ((𝐴‘𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀‘𝑈)”⟩⟩))
127	33, 44, 117, 126	syl3anc 1396	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃(𝑇‘(𝐴‘𝐾))𝑈) = ((𝐴‘𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀‘𝑈)”⟩⟩))
128		splval 14788	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝐾) ∈ 𝑊 ∧ (𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ ⟨“𝑈(𝑀‘𝑈)”⟩ ∈ Word (𝐼 × 2o))) → ((𝐴‘𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀‘𝑈)”⟩⟩) = ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))
129	33, 44, 44, 120, 128	syl13anc 1397	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀‘𝑈)”⟩⟩) = ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))
130	125, 127, 129	3eqtrd 2808	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘𝐴) = ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))
131		efgredlemb.7	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉))
132	2, 3, 4, 5	efgtval 19793	. . . . . . . . . . . . . 14 ⊢ (((𝐵‘𝐿) ∈ 𝑊 ∧ 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ 𝑉 ∈ (𝐼 × 2o)) → (𝑄(𝑇‘(𝐵‘𝐿))𝑉) = ((𝐵‘𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩))
133	29, 14, 92, 132	syl3anc 1396	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄(𝑇‘(𝐵‘𝐿))𝑉) = ((𝐵‘𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩))
134		splval 14788	. . . . . . . . . . . . . 14 ⊢ (((𝐵‘𝐿) ∈ 𝑊 ∧ (𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ ⟨“𝑉(𝑀‘𝑉)”⟩ ∈ Word (𝐼 × 2o))) → ((𝐵‘𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
135	29, 14, 14, 102, 134	syl13anc 1397	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵‘𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
136	131, 133, 135	3eqtrd 2808	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘𝐵) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
137	24, 130, 136	3eqtr3d 2812	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
138	114, 124, 137	3eqtr2d 2810	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
139		swrdcl 14683	. . . . . . . . . . . 12 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2o))
140	34, 139	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2o))
141		ccatcl 14611	. . . . . . . . . . . 12 ⊢ ((⟨“𝑈(𝑀‘𝑈)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2o)) → (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2o))
142	120, 122, 141	syl2anc 595	. . . . . . . . . . 11 ⊢ (𝜑 → (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2o))
143		ccatass 14626	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2o)) → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))))
144	96, 140, 142, 143	syl3anc 1396	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))))
145		swrdcl 14683	. . . . . . . . . . . 12 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o))
146	30, 145	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o))
147		ccatass 14626	. . . . . . . . . . 11 ⊢ ((((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑉(𝑀‘𝑉)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o)) → ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
148	32, 102, 146, 147	syl3anc 1396	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
149	138, 144, 148	3eqtr3d 2812	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))) = (((𝐵‘𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
150		ccatcl 14611	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2o)) → (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2o))
151	140, 142, 150	syl2anc 595	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2o))
152		ccatcl 14611	. . . . . . . . . . 11 ⊢ ((⟨“𝑉(𝑀‘𝑉)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o)) → (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) ∈ Word (𝐼 × 2o))
153	102, 146, 152	syl2anc 595	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) ∈ Word (𝐼 × 2o))
154		uztrn 12880	. . . . . . . . . . . . . 14 ⊢ (((♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘𝑃) ∧ 𝑃 ∈ (ℤ≥‘𝑄)) → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘𝑄))
155	46, 109, 154	syl2anc 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘𝑄))
156		elfzuzb 13546	. . . . . . . . . . . . 13 ⊢ (𝑄 ∈ (0...(♯‘(𝐴‘𝐾))) ↔ (𝑄 ∈ (ℤ≥‘0) ∧ (♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘𝑄)))
157	16, 155, 156	sylanbrc 594	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝐴‘𝐾))))
158		pfxlen 14721	. . . . . . . . . . . 12 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) prefix 𝑄)) = 𝑄)
159	34, 157, 158	syl2anc 595	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) prefix 𝑄)) = 𝑄)
160	159, 40	eqtr4d 2807	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) prefix 𝑄)) = (♯‘((𝐵‘𝐿) prefix 𝑄)))
161		ccatopth 14753	. . . . . . . . . 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 1406	. . . . . . . . 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 499	. . . . . . 7 ⊢ (𝜑 → ((𝐴‘𝐾) prefix 𝑄) = ((𝐵‘𝐿) prefix 𝑄))
165	164	oveq1d 7426	. . . . . 6 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
166		ccatrid 14625	. . . . . . . 8 ⊢ (((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o) → (((𝐴‘𝐾) prefix 𝑄) ++ ∅) = ((𝐴‘𝐾) prefix 𝑄))
167	96, 166	syl 18	. . . . . . 7 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ∅) = ((𝐴‘𝐾) prefix 𝑄))
168	167	oveq1d 7426	. . . . . 6 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ∅) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
169	165, 168, 17	3eqtr4rd 2815	. . . . 5 ⊢ (𝜑 → (𝑆‘𝐶) = ((((𝐴‘𝐾) prefix 𝑄) ++ ∅) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
170	159	eqcomd 2775	. . . . 5 ⊢ (𝜑 → 𝑄 = (♯‘((𝐴‘𝐾) prefix 𝑄)))
171		hash0 14403	. . . . . . 7 ⊢ (♯‘∅) = 0
172	171	oveq2i 7422	. . . . . 6 ⊢ (𝑄 + (♯‘∅)) = (𝑄 + 0)
173	62	addridd 11410	. . . . . 6 ⊢ (𝜑 → (𝑄 + 0) = 𝑄)
174	172, 173	eqtr2id 2817	. . . . 5 ⊢ (𝜑 → 𝑄 = (𝑄 + (♯‘∅)))
175	96, 98, 36, 102, 169, 170, 174	splval2 14794	. . . 4 ⊢ (𝜑 → ((𝑆‘𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩) = ((((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
176		elfzuzb 13546	. . . . . . . . . . . . . 14 ⊢ (𝑄 ∈ (0...(𝑄 + 2)) ↔ (𝑄 ∈ (ℤ≥‘0) ∧ (𝑄 + 2) ∈ (ℤ≥‘𝑄)))
177	16, 107, 176	sylanbrc 594	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∈ (0...(𝑄 + 2)))
178		elfzuzb 13546	. . . . . . . . . . . . . 14 ⊢ ((𝑄 + 2) ∈ (0...𝑃) ↔ ((𝑄 + 2) ∈ (ℤ≥‘0) ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))))
179	43, 47, 178	sylanbrc 594	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄 + 2) ∈ (0...𝑃))
180		ccatswrd 14706	. . . . . . . . . . . . 13 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))))) → (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩))
181	34, 177, 179, 44, 180	syl13anc 1397	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩))
182	181	oveq1d 7426	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))))
183		swrdcl 14683	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2o))
184	34, 183	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2o))
185		swrdcl 14683	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2o))
186	34, 185	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2o))
187		ccatass 14626	. . . . . . . . . . . 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 1396	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))))
189	163	simprd 500	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
190	182, 188, 189	3eqtr3d 2812	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
191		ccatcl 14611	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2o)) → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2o))
192	186, 142, 191	syl2anc 595	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2o))
193		swrdlen 14685	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝑄 + 2) − 𝑄))
194	34, 177, 51, 193	syl3anc 1396	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝑄 + 2) − 𝑄))
195		pncan2 11464	. . . . . . . . . . . . . 14 ⊢ ((𝑄 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑄 + 2) − 𝑄) = 2)
196	62, 69, 195	sylancl 597	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑄 + 2) − 𝑄) = 2)
197	194, 196	eqtrd 2804	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = 2)
198		s2len 14926	. . . . . . . . . . . 12 ⊢ (♯‘⟨“𝑉(𝑀‘𝑉)”⟩) = 2
199	197, 198	eqtr4di 2822	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (♯‘⟨“𝑉(𝑀‘𝑉)”⟩))
200		ccatopth 14753	. . . . . . . . . . 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 1406	. . . . . . . . . 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 499	. . . . . . . 8 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀‘𝑉)”⟩)
204	203	oveq2d 7427	. . . . . . 7 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩))
205		ccatpfx 14738	. . . . . . . 8 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾)))) → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝐴‘𝐾) prefix (𝑄 + 2)))
206	34, 177, 51, 205	syl3anc 1396	. . . . . . 7 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝐴‘𝐾) prefix (𝑄 + 2)))
207	204, 206	eqtr3d 2806	. . . . . 6 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) = ((𝐴‘𝐾) prefix (𝑄 + 2)))
208	207	oveq1d 7426	. . . . 5 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (((𝐴‘𝐾) prefix (𝑄 + 2)) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
209		ccatpfx 14738	. . . . . 6 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾))) ∧ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾)))) → (((𝐴‘𝐾) prefix (𝑄 + 2)) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))))
210	34, 51, 57, 209	syl3anc 1396	. . . . 5 ⊢ (𝜑 → (((𝐴‘𝐾) prefix (𝑄 + 2)) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))))
211		pfxid 14722	. . . . . 6 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))) = (𝐴‘𝐾))
212	34, 211	syl 18	. . . . 5 ⊢ (𝜑 → ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))) = (𝐴‘𝐾))
213	208, 210, 212	3eqtrd 2808	. . . 4 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (𝐴‘𝐾))
214	94, 175, 213	3eqtrd 2808	. . 3 ⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = (𝐴‘𝐾))
215	2, 3, 4, 5	efgtf 19792	. . . . . . 7 ⊢ ((𝑆‘𝐶) ∈ 𝑊 → ((𝑇‘(𝑆‘𝐶)) = (𝑎 ∈ (0...(♯‘(𝑆‘𝐶))), 𝑖 ∈ (𝐼 × 2o) ↦ ((𝑆‘𝐶) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀‘𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆‘𝐶)):((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o))⟶𝑊))
216	13, 215	syl 18	. . . . . 6 ⊢ (𝜑 → ((𝑇‘(𝑆‘𝐶)) = (𝑎 ∈ (0...(♯‘(𝑆‘𝐶))), 𝑖 ∈ (𝐼 × 2o) ↦ ((𝑆‘𝐶) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀‘𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆‘𝐶)):((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o))⟶𝑊))
217	216	simprd 500	. . . . 5 ⊢ (𝜑 → (𝑇‘(𝑆‘𝐶)):((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o))⟶𝑊)
218	217	ffnd 6707	. . . 4 ⊢ (𝜑 → (𝑇‘(𝑆‘𝐶)) Fn ((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o)))
219		fnovrn 7586	. . . 4 ⊢ (((𝑇‘(𝑆‘𝐶)) Fn ((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o)) ∧ 𝑄 ∈ (0...(♯‘(𝑆‘𝐶))) ∧ 𝑉 ∈ (𝐼 × 2o)) → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) ∈ ran (𝑇‘(𝑆‘𝐶)))
220	218, 91, 92, 219	syl3anc 1396	. . 3 ⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) ∈ ran (𝑇‘(𝑆‘𝐶)))
221	214, 220	eqeltrrd 2870	. 2 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶)))
222		uztrn 12880	. . . . . . 7 ⊢ (((𝑃 − 2) ∈ (ℤ≥‘𝑄) ∧ 𝑄 ∈ (ℤ≥‘0)) → (𝑃 − 2) ∈ (ℤ≥‘0))
223	87, 16, 222	syl2anc 595	. . . . . 6 ⊢ (𝜑 → (𝑃 − 2) ∈ (ℤ≥‘0))
224		elfzuzb 13546	. . . . . 6 ⊢ ((𝑃 − 2) ∈ (0...(♯‘(𝑆‘𝐶))) ↔ ((𝑃 − 2) ∈ (ℤ≥‘0) ∧ (♯‘(𝑆‘𝐶)) ∈ (ℤ≥‘(𝑃 − 2))))
225	223, 85, 224	sylanbrc 594	. . . . 5 ⊢ (𝜑 → (𝑃 − 2) ∈ (0...(♯‘(𝑆‘𝐶))))
226	2, 3, 4, 5	efgtval 19793	. . . . 5 ⊢ (((𝑆‘𝐶) ∈ 𝑊 ∧ (𝑃 − 2) ∈ (0...(♯‘(𝑆‘𝐶))) ∧ 𝑈 ∈ (𝐼 × 2o)) → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = ((𝑆‘𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀‘𝑈)”⟩⟩))
227	13, 225, 117, 226	syl3anc 1396	. . . 4 ⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = ((𝑆‘𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀‘𝑈)”⟩⟩))
228		pfxcl 14715	. . . . . 6 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2o))
229	30, 228	syl 18	. . . . 5 ⊢ (𝜑 → ((𝐵‘𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2o))
230		swrdcl 14683	. . . . . 6 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o))
231	30, 230	syl 18	. . . . 5 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o))
232		ccatswrd 14706	. . . . . . . . . . 11 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ ((𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾))))) → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))
233	34, 179, 44, 57, 232	syl13anc 1397	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))
234	202	simprd 500	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))
235		elfzuzb 13546	. . . . . . . . . . . . . . . 16 ⊢ (𝑄 ∈ (0...(𝑃 − 2)) ↔ (𝑄 ∈ (ℤ≥‘0) ∧ (𝑃 − 2) ∈ (ℤ≥‘𝑄)))
236	16, 87, 235	sylanbrc 594	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑄 ∈ (0...(𝑃 − 2)))
237	2, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27, 44, 14, 117, 92, 125, 131	efgredlemg 19812	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) = (♯‘(𝐵‘𝐿)))
238	237, 46	eqeltrrd 2870	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘𝑃))
239		0le2 12343	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ≤ 2
240	239	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 ≤ 2)
241	74	zred 12700	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑃 ∈ ℝ)
242		2re 12315	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℝ
243		subge02 11730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃 ∈ ℝ ∧ 2 ∈ ℝ) → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃))
244	241, 242, 243	sylancl 597	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃))
245	240, 244	mpbid 235	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑃 − 2) ≤ 𝑃)
246		eluz2 12868	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ (ℤ≥‘(𝑃 − 2)) ↔ ((𝑃 − 2) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑃 − 2) ≤ 𝑃))
247	76, 74, 245, 246	syl3anbrc 1360	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(𝑃 − 2)))
248		uztrn 12880	. . . . . . . . . . . . . . . . 17 ⊢ (((♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘𝑃) ∧ 𝑃 ∈ (ℤ≥‘(𝑃 − 2))) → (♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘(𝑃 − 2)))
249	238, 247, 248	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘(𝑃 − 2)))
250		elfzuzb 13546	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿))) ↔ ((𝑃 − 2) ∈ (ℤ≥‘0) ∧ (♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘(𝑃 − 2))))
251	223, 249, 250	sylanbrc 594	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿))))
252		lencl 14570	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → (♯‘(𝐵‘𝐿)) ∈ ℕ0)
253	30, 252	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ ℕ0)
254	253, 54	eleqtrdi 2879	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘0))
255		eluzfz2 13560	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘0) → (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))
256	254, 255	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))
257		ccatswrd 14706	. . . . . . . . . . . . . . 15 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿))) ∧ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))) → (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))
258	30, 236, 251, 256, 257	syl13anc 1397	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))
259	234, 258	eqtr4d 2807	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)))
260		swrdcl 14683	. . . . . . . . . . . . . . 15 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2o))
261	30, 260	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2o))
262		swrdcl 14683	. . . . . . . . . . . . . . 15 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o))
263	30, 262	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2o))
264		swrdlen 14685	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (𝑃 − (𝑄 + 2)))
265	34, 179, 44, 264	syl3anc 1396	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (𝑃 − (𝑄 + 2)))
266		swrdlen 14685	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝑃 − 2) − 𝑄))
267	30, 236, 251, 266	syl3anc 1396	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝑃 − 2) − 𝑄))
268	78, 62, 70	sub32d 11601	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑃 − 𝑄) − 2) = ((𝑃 − 2) − 𝑄))
269	78, 62, 70	subsub4d 11600	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑃 − 𝑄) − 2) = (𝑃 − (𝑄 + 2)))
270	267, 268, 269	3eqtr2d 2810	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = (𝑃 − (𝑄 + 2)))
271	265, 270	eqtr4d 2807	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (♯‘((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)))
272		ccatopth 14753	. . . . . . . . . . . . . 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 1406	. . . . . . . . . . . . 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 499	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩))
276	274	simprd 500	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩))
277		elfzuzb 13546	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 − 2) ∈ (0...𝑃) ↔ ((𝑃 − 2) ∈ (ℤ≥‘0) ∧ 𝑃 ∈ (ℤ≥‘(𝑃 − 2))))
278	223, 247, 277	sylanbrc 594	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 − 2) ∈ (0...𝑃))
279		elfzuz 13548	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) → 𝑃 ∈ (ℤ≥‘0))
280	44, 279	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘0))
281		elfzuzb 13546	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ (0...(♯‘(𝐵‘𝐿))) ↔ (𝑃 ∈ (ℤ≥‘0) ∧ (♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘𝑃)))
282	280, 238, 281	sylanbrc 594	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ (0...(♯‘(𝐵‘𝐿))))
283		ccatswrd 14706	. . . . . . . . . . . . . . 15 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ ((𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))) → (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩))
284	30, 278, 282, 256, 283	syl13anc 1397	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩))
285	276, 284	eqtr4d 2807	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
286		swrdcl 14683	. . . . . . . . . . . . . . 15 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2o))
287	30, 286	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2o))
288		s2len 14926	. . . . . . . . . . . . . . 15 ⊢ (♯‘⟨“𝑈(𝑀‘𝑈)”⟩) = 2
289		swrdlen 14685	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = (𝑃 − (𝑃 − 2)))
290	30, 278, 282, 289	syl3anc 1396	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = (𝑃 − (𝑃 − 2)))
291		nncan 11487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑃 − (𝑃 − 2)) = 2)
292	78, 69, 291	sylancl 597	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃 − (𝑃 − 2)) = 2)
293	290, 292	eqtr2d 2805	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 = (♯‘((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
294	288, 293	eqtrid 2816	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘⟨“𝑈(𝑀‘𝑈)”⟩) = (♯‘((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
295		ccatopth 14753	. . . . . . . . . . . . . 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 1406	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) ↔ (⟨“𝑈(𝑀‘𝑈)”⟩ = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) = ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))))
297	285, 296	mpbid 235	. . . . . . . . . . . 12 ⊢ (𝜑 → (⟨“𝑈(𝑀‘𝑈)”⟩ = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) = ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
298	297	simprd 500	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) = ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))
299	275, 298	oveq12d 7429	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
300	233, 299	eqtr3d 2806	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩) = (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
301	300	oveq2d 7427	. . . . . . . 8 ⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))))
302		ccatass 14626	. . . . . . . . 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 1396	. . . . . . . 8 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))))
304	301, 303	eqtr4d 2807	. . . . . . 7 ⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
305		ccatpfx 14738	. . . . . . . . 9 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿)))) → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝐵‘𝐿) prefix (𝑃 − 2)))
306	30, 236, 251, 305	syl3anc 1396	. . . . . . . 8 ⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝐵‘𝐿) prefix (𝑃 − 2)))
307	306	oveq1d 7426	. . . . . . 7 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
308	17, 304, 307	3eqtrd 2808	. . . . . 6 ⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
309		ccatrid 14625	. . . . . . . 8 ⊢ (((𝐵‘𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2o) → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) = ((𝐵‘𝐿) prefix (𝑃 − 2)))
310	229, 309	syl 18	. . . . . . 7 ⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) = ((𝐵‘𝐿) prefix (𝑃 − 2)))
311	310	oveq1d 7426	. . . . . 6 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
312	308, 311	eqtr4d 2807	. . . . 5 ⊢ (𝜑 → (𝑆‘𝐶) = ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
313		pfxlen 14721	. . . . . . 7 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) prefix (𝑃 − 2))) = (𝑃 − 2))
314	30, 251, 313	syl2anc 595	. . . . . 6 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) prefix (𝑃 − 2))) = (𝑃 − 2))
315	314	eqcomd 2775	. . . . 5 ⊢ (𝜑 → (𝑃 − 2) = (♯‘((𝐵‘𝐿) prefix (𝑃 − 2))))
316	171	oveq2i 7422	. . . . . 6 ⊢ ((𝑃 − 2) + (♯‘∅)) = ((𝑃 − 2) + 0)
317	76	zcnd 12701	. . . . . . 7 ⊢ (𝜑 → (𝑃 − 2) ∈ ℂ)
318	317	addridd 11410	. . . . . 6 ⊢ (𝜑 → ((𝑃 − 2) + 0) = (𝑃 − 2))
319	316, 318	eqtr2id 2817	. . . . 5 ⊢ (𝜑 → (𝑃 − 2) = ((𝑃 − 2) + (♯‘∅)))
320	229, 98, 231, 120, 312, 315, 319	splval2 14794	. . . 4 ⊢ (𝜑 → ((𝑆‘𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀‘𝑈)”⟩⟩) = ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
321	297	simpld 499	. . . . . . . 8 ⊢ (𝜑 → ⟨“𝑈(𝑀‘𝑈)”⟩ = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩))
322	321	oveq2d 7427	. . . . . . 7 ⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
323		ccatpfx 14738	. . . . . . . 8 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿)))) → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = ((𝐵‘𝐿) prefix 𝑃))
324	30, 278, 282, 323	syl3anc 1396	. . . . . . 7 ⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = ((𝐵‘𝐿) prefix 𝑃))
325	322, 324	eqtrd 2804	. . . . . 6 ⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) = ((𝐵‘𝐿) prefix 𝑃))
326	325	oveq1d 7426	. . . . 5 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑃) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
327		ccatpfx 14738	. . . . . 6 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿)))) → (((𝐵‘𝐿) prefix 𝑃) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))))
328	30, 282, 256, 327	syl3anc 1396	. . . . 5 ⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑃) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))))
329		pfxid 14722	. . . . . 6 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))) = (𝐵‘𝐿))
330	30, 329	syl 18	. . . . 5 ⊢ (𝜑 → ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))) = (𝐵‘𝐿))
331	326, 328, 330	3eqtrd 2808	. . . 4 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (𝐵‘𝐿))
332	227, 320, 331	3eqtrd 2808	. . 3 ⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = (𝐵‘𝐿))
333		fnovrn 7586	. . . 4 ⊢ (((𝑇‘(𝑆‘𝐶)) Fn ((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝑆‘𝐶))) ∧ 𝑈 ∈ (𝐼 × 2o)) → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) ∈ ran (𝑇‘(𝑆‘𝐶)))
334	218, 225, 117, 333	syl3anc 1396	. . 3 ⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) ∈ ran (𝑇‘(𝑆‘𝐶)))
335	332, 334	eqeltrrd 2870	. 2 ⊢ (𝜑 → (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶)))
336	221, 335	jca 520	1 ⊢ (𝜑 → ((𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶)) ∧ (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∀wral 3085  {crab 3422   ∖ cdif 3908  ∅c0 4292  {csn 4592  ⟨cop 4598  ⟨cotp 4600  ∪ ciun 4958   class class class wbr 5111   ↦ cmpt 5194   I cid 5556   × cxp 5660  dom cdm 5662  ran crn 5663   Fn wfn 6532  ⟶wf 6533  ‘cfv 6537  (class class class)co 7411   ∈ cmpo 7413  1_oc1o 8446  2_oc2o 8447  ℂcc 11098  ℝcr 11099  0cc0 11100  1c1 11101   + caddc 11103   < clt 11243   ≤ cle 11244   − cmin 11441  2c2 12295  ℕ₀cn0 12504  ℤcz 12591  ℤ_≥cuz 12862  ...cfz 13535  ..^cfzo 13682  ♯chash 14366  Word cword 14550   ++ cconcat 14607   substr csubstr 14678   prefix cpfx 14708   splice csplice 14786  ⟨“cs2 14878   ~_FG cefg 19776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-cnex 11156  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-addrcl 11161  ax-mulcl 11162  ax-mulrcl 11163  ax-mulcom 11164  ax-addass 11165  ax-mulass 11166  ax-distr 11167  ax-i2m1 11168  ax-1ne0 11169  ax-1rid 11170  ax-rnegex 11171  ax-rrecex 11172  ax-cnre 11173  ax-pre-lttri 11174  ax-pre-lttrn 11175  ax-pre-ltadd 11176  ax-pre-mulgt0 11177

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3376  df-rab 3423  df-v 3463  df-sbc 3752  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-ot 4601  df-uni 4875  df-int 4915  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7863  df-1st 7986  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-1o 8453  df-2o 8454  df-er 8694  df-map 8826  df-en 8944  df-dom 8945  df-sdom 8946  df-fin 8947  df-card 9925  df-pnf 11245  df-mnf 11246  df-xr 11247  df-ltxr 11248  df-le 11249  df-sub 11443  df-neg 11444  df-nn 12234  df-2 12303  df-n0 12505  df-z 12592  df-uz 12863  df-fz 13536  df-fzo 13683  df-hash 14367  df-word 14551  df-concat 14608  df-s1 14634  df-substr 14679  df-pfx 14709  df-splice 14787  df-s2 14885

This theorem is referenced by:  efgredlemd  19814