efgredleme - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > efgredleme		Structured version Visualization version GIF version

Theorem efgredleme 18640

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

**Hypotheses**
Ref	Expression
efgval.w	⊢ 𝑊 = ( I ‘Word (𝐼 × 2_o))
efgval.r	⊢ ∼ = ( ~_FG ‘𝐼)
efgval2.m	⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2_o ↦ ⟨𝑦, (1_o ∖ 𝑧)⟩)
efgval2.t	⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2_o) ↦ (𝑣 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	⊢ (𝜑 → 𝑈 ∈ (𝐼 × 2_o))
efgredlemb.v	⊢ (𝜑 → 𝑉 ∈ (𝐼 × 2_o))
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 (𝐼 × 2_o))
3		efgval.r	. . . . . . . . 9 ⊢ ∼ = ( ~_FG ‘𝐼)
4		efgval2.m	. . . . . . . . 9 ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2_o ↦ ⟨𝑦, (1_o ∖ 𝑧)⟩)
5		efgval2.t	. . . . . . . . 9 ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2_o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))
6		efgred.d	. . . . . . . . 9 ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))
7		efgred.s	. . . . . . . . 9 ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))
8	2, 3, 4, 5, 6, 7	efgsf 18625	. . . . . . . 8 ⊢ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊
9	8	fdmi 6359	. . . . . . . . 9 ⊢ dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}
10	9	feq2i 6341	. . . . . . . 8 ⊢ (𝑆:dom 𝑆⟶𝑊 ↔ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊)
11	8, 10	mpbir 223	. . . . . . 7 ⊢ 𝑆:dom 𝑆⟶𝑊
12	11	ffvelrni 6681	. . . . . 6 ⊢ (𝐶 ∈ dom 𝑆 → (𝑆‘𝐶) ∈ 𝑊)
13	1, 12	syl 17	. . . . 5 ⊢ (𝜑 → (𝑆‘𝐶) ∈ 𝑊)
14		efgredlemb.q	. . . . . . 7 ⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))))
15		elfzuz 12726	. . . . . . 7 ⊢ (𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) → 𝑄 ∈ (ℤ_≥‘0))
16	14, 15	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑄 ∈ (ℤ_≥‘0))
17		efgredlemd.sc	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
18	17	fveq2d 6508	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(𝑆‘𝐶)) = (♯‘(((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))))
19		fviss 6575	. . . . . . . . . . . . 13 ⊢ ( I ‘Word (𝐼 × 2_o)) ⊆ Word (𝐼 × 2_o)
20	2, 19	eqsstri 3893	. . . . . . . . . . . 12 ⊢ 𝑊 ⊆ Word (𝐼 × 2_o)
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 18638	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝐾) ∈ 𝑊 ∧ (𝐵‘𝐿) ∈ 𝑊))
29	28	simprd 488	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵‘𝐿) ∈ 𝑊)
30	20, 29	sseldi 3858	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵‘𝐿) ∈ Word (𝐼 × 2_o))
31		pfxcl 13865	. . . . . . . . . . 11 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) → ((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2_o))
32	30, 31	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2_o))
33	28	simpld 487	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴‘𝐾) ∈ 𝑊)
34	20, 33	sseldi 3858	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴‘𝐾) ∈ Word (𝐼 × 2_o))
35		swrdcl 13814	. . . . . . . . . . 11 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2_o))
36	34, 35	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2_o))
37		ccatlen 13744	. . . . . . . . . 10 ⊢ ((((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2_o) ∧ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2_o)) → (♯‘(((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))) = ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))))
38	32, 36, 37	syl2anc 576	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))) = ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))))
39		pfxlen 13871	. . . . . . . . . . . 12 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) ∧ 𝑄 ∈ (0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) prefix 𝑄)) = 𝑄)
40	30, 14, 39	syl2anc 576	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) prefix 𝑄)) = 𝑄)
41		2nn0 11732	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ₀
42		uzaddcl 12124	. . . . . . . . . . . . . 14 ⊢ ((𝑄 ∈ (ℤ_≥‘0) ∧ 2 ∈ ℕ₀) → (𝑄 + 2) ∈ (ℤ_≥‘0))
43	16, 41, 42	sylancl 578	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄 + 2) ∈ (ℤ_≥‘0))
44		efgredlemb.p	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))))
45		elfzuz3 12727	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) → (♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘𝑃))
46	44, 45	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘𝑃))
47		efgredlemd.9	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ (ℤ_≥‘(𝑄 + 2)))
48		uztrn 12081	. . . . . . . . . . . . . 14 ⊢ (((♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘𝑃) ∧ 𝑃 ∈ (ℤ_≥‘(𝑄 + 2))) → (♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘(𝑄 + 2)))
49	46, 47, 48	syl2anc 576	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘(𝑄 + 2)))
50		elfzuzb 12724	. . . . . . . . . . . . 13 ⊢ ((𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾))) ↔ ((𝑄 + 2) ∈ (ℤ_≥‘0) ∧ (♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘(𝑄 + 2))))
51	43, 49, 50	sylanbrc 575	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾))))
52		lencl 13700	. . . . . . . . . . . . . . 15 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) → (♯‘(𝐴‘𝐾)) ∈ ℕ₀)
53	34, 52	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ ℕ₀)
54		nn0uz 12100	. . . . . . . . . . . . . 14 ⊢ ℕ₀ = (ℤ_≥‘0)
55	53, 54	syl6eleq 2878	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘0))
56		eluzfz2 12737	. . . . . . . . . . . . 13 ⊢ ((♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘0) → (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾))))
57	55, 56	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾))))
58		swrdlen 13818	. . . . . . . . . . . 12 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾))) ∧ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((♯‘(𝐴‘𝐾)) − (𝑄 + 2)))
59	34, 51, 57, 58	syl3anc 1352	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((♯‘(𝐴‘𝐾)) − (𝑄 + 2)))
60	40, 59	oveq12d 7000	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))) = (𝑄 + ((♯‘(𝐴‘𝐾)) − (𝑄 + 2))))
61		elfzelz 12730	. . . . . . . . . . . . 13 ⊢ (𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) → 𝑄 ∈ ℤ)
62	14, 61	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ ℤ)
63	62	zcnd 11907	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ ℂ)
64	53	nn0cnd 11775	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ ℂ)
65		2z 11833	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℤ
66		zaddcl 11841	. . . . . . . . . . . . 13 ⊢ ((𝑄 ∈ ℤ ∧ 2 ∈ ℤ) → (𝑄 + 2) ∈ ℤ)
67	62, 65, 66	sylancl 578	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄 + 2) ∈ ℤ)
68	67	zcnd 11907	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄 + 2) ∈ ℂ)
69	63, 64, 68	addsubassd 10824	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑄 + (♯‘(𝐴‘𝐾))) − (𝑄 + 2)) = (𝑄 + ((♯‘(𝐴‘𝐾)) − (𝑄 + 2))))
70		2cn 11521	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
71	70	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℂ)
72	63, 64, 71	pnpcand 10841	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑄 + (♯‘(𝐴‘𝐾))) − (𝑄 + 2)) = ((♯‘(𝐴‘𝐾)) − 2))
73	60, 69, 72	3eqtr2d 2822	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))) = ((♯‘(𝐴‘𝐾)) − 2))
74	18, 38, 73	3eqtrd 2820	. . . . . . . 8 ⊢ (𝜑 → (♯‘(𝑆‘𝐶)) = ((♯‘(𝐴‘𝐾)) − 2))
75		elfzelz 12730	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) → 𝑃 ∈ ℤ)
76	44, 75	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ ℤ)
77		zsubcl 11843	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℤ ∧ 2 ∈ ℤ) → (𝑃 − 2) ∈ ℤ)
78	76, 65, 77	sylancl 578	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 − 2) ∈ ℤ)
79	65	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 2 ∈ ℤ)
80	76	zcnd 11907	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℂ)
81		npcan 10702	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑃 − 2) + 2) = 𝑃)
82	80, 70, 81	sylancl 578	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑃 − 2) + 2) = 𝑃)
83	82	fveq2d 6508	. . . . . . . . . 10 ⊢ (𝜑 → (ℤ_≥‘((𝑃 − 2) + 2)) = (ℤ_≥‘𝑃))
84	46, 83	eleqtrrd 2871	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘((𝑃 − 2) + 2)))
85		eluzsub 12094	. . . . . . . . 9 ⊢ (((𝑃 − 2) ∈ ℤ ∧ 2 ∈ ℤ ∧ (♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘((𝑃 − 2) + 2))) → ((♯‘(𝐴‘𝐾)) − 2) ∈ (ℤ_≥‘(𝑃 − 2)))
86	78, 79, 84, 85	syl3anc 1352	. . . . . . . 8 ⊢ (𝜑 → ((♯‘(𝐴‘𝐾)) − 2) ∈ (ℤ_≥‘(𝑃 − 2)))
87	74, 86	eqeltrd 2868	. . . . . . 7 ⊢ (𝜑 → (♯‘(𝑆‘𝐶)) ∈ (ℤ_≥‘(𝑃 − 2)))
88		eluzsub 12094	. . . . . . . 8 ⊢ ((𝑄 ∈ ℤ ∧ 2 ∈ ℤ ∧ 𝑃 ∈ (ℤ_≥‘(𝑄 + 2))) → (𝑃 − 2) ∈ (ℤ_≥‘𝑄))
89	62, 79, 47, 88	syl3anc 1352	. . . . . . 7 ⊢ (𝜑 → (𝑃 − 2) ∈ (ℤ_≥‘𝑄))
90		uztrn 12081	. . . . . . 7 ⊢ (((♯‘(𝑆‘𝐶)) ∈ (ℤ_≥‘(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (ℤ_≥‘𝑄)) → (♯‘(𝑆‘𝐶)) ∈ (ℤ_≥‘𝑄))
91	87, 89, 90	syl2anc 576	. . . . . 6 ⊢ (𝜑 → (♯‘(𝑆‘𝐶)) ∈ (ℤ_≥‘𝑄))
92		elfzuzb 12724	. . . . . 6 ⊢ (𝑄 ∈ (0...(♯‘(𝑆‘𝐶))) ↔ (𝑄 ∈ (ℤ_≥‘0) ∧ (♯‘(𝑆‘𝐶)) ∈ (ℤ_≥‘𝑄)))
93	16, 91, 92	sylanbrc 575	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝑆‘𝐶))))
94		efgredlemb.v	. . . . 5 ⊢ (𝜑 → 𝑉 ∈ (𝐼 × 2_o))
95	2, 3, 4, 5	efgtval 18619	. . . . 5 ⊢ (((𝑆‘𝐶) ∈ 𝑊 ∧ 𝑄 ∈ (0...(♯‘(𝑆‘𝐶))) ∧ 𝑉 ∈ (𝐼 × 2_o)) → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = ((𝑆‘𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩))
96	13, 93, 94, 95	syl3anc 1352	. . . 4 ⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = ((𝑆‘𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩))
97		pfxcl 13865	. . . . . 6 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) → ((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2_o))
98	34, 97	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2_o))
99		wrd0 13706	. . . . . 6 ⊢ ∅ ∈ Word (𝐼 × 2_o)
100	99	a1i 11	. . . . 5 ⊢ (𝜑 → ∅ ∈ Word (𝐼 × 2_o))
101	4	efgmf 18609	. . . . . . . 8 ⊢ 𝑀:(𝐼 × 2_o)⟶(𝐼 × 2_o)
102	101	ffvelrni 6681	. . . . . . 7 ⊢ (𝑉 ∈ (𝐼 × 2_o) → (𝑀‘𝑉) ∈ (𝐼 × 2_o))
103	94, 102	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑀‘𝑉) ∈ (𝐼 × 2_o))
104	94, 103	s2cld 14101	. . . . 5 ⊢ (𝜑 → ⟨“𝑉(𝑀‘𝑉)”⟩ ∈ Word (𝐼 × 2_o))
105	62	zred 11906	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄 ∈ ℝ)
106		nn0addge1 11761	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄 ∈ ℝ ∧ 2 ∈ ℕ₀) → 𝑄 ≤ (𝑄 + 2))
107	105, 41, 106	sylancl 578	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑄 ≤ (𝑄 + 2))
108		eluz2 12070	. . . . . . . . . . . . . . . 16 ⊢ ((𝑄 + 2) ∈ (ℤ_≥‘𝑄) ↔ (𝑄 ∈ ℤ ∧ (𝑄 + 2) ∈ ℤ ∧ 𝑄 ≤ (𝑄 + 2)))
109	62, 67, 107, 108	syl3anbrc 1324	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑄 + 2) ∈ (ℤ_≥‘𝑄))
110		uztrn 12081	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℤ_≥‘(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (ℤ_≥‘𝑄)) → 𝑃 ∈ (ℤ_≥‘𝑄))
111	47, 109, 110	syl2anc 576	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ (ℤ_≥‘𝑄))
112		elfzuzb 12724	. . . . . . . . . . . . . 14 ⊢ (𝑄 ∈ (0...𝑃) ↔ (𝑄 ∈ (ℤ_≥‘0) ∧ 𝑃 ∈ (ℤ_≥‘𝑄)))
113	16, 111, 112	sylanbrc 575	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∈ (0...𝑃))
114		ccatpfx 13889	. . . . . . . . . . . . 13 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) ∧ 𝑄 ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾)))) → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) = ((𝐴‘𝐾) prefix 𝑃))
115	34, 113, 44, 114	syl3anc 1352	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) = ((𝐴‘𝐾) prefix 𝑃))
116	115	oveq1d 6997	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) prefix 𝑃) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))))
117		pfxcl 13865	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) → ((𝐴‘𝐾) prefix 𝑃) ∈ Word (𝐼 × 2_o))
118	34, 117	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) prefix 𝑃) ∈ Word (𝐼 × 2_o))
119		efgredlemb.u	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ∈ (𝐼 × 2_o))
120	101	ffvelrni 6681	. . . . . . . . . . . . . 14 ⊢ (𝑈 ∈ (𝐼 × 2_o) → (𝑀‘𝑈) ∈ (𝐼 × 2_o))
121	119, 120	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀‘𝑈) ∈ (𝐼 × 2_o))
122	119, 121	s2cld 14101	. . . . . . . . . . . 12 ⊢ (𝜑 → ⟨“𝑈(𝑀‘𝑈)”⟩ ∈ Word (𝐼 × 2_o))
123		swrdcl 13814	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) → ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2_o))
124	34, 123	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2_o))
125		ccatass 13757	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝐾) prefix 𝑃) ∈ Word (𝐼 × 2_o) ∧ ⟨“𝑈(𝑀‘𝑈)”⟩ ∈ Word (𝐼 × 2_o) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2_o)) → ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐴‘𝐾) prefix 𝑃) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))))
126	118, 122, 124, 125	syl3anc 1352	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐴‘𝐾) prefix 𝑃) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))))
127		efgredlemb.6	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈))
128	2, 3, 4, 5	efgtval 18619	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝐾) ∈ 𝑊 ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ 𝑈 ∈ (𝐼 × 2_o)) → (𝑃(𝑇‘(𝐴‘𝐾))𝑈) = ((𝐴‘𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀‘𝑈)”⟩⟩))
129	33, 44, 119, 128	syl3anc 1352	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃(𝑇‘(𝐴‘𝐾))𝑈) = ((𝐴‘𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀‘𝑈)”⟩⟩))
130		splval 13969	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝐾) ∈ 𝑊 ∧ (𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ ⟨“𝑈(𝑀‘𝑈)”⟩ ∈ Word (𝐼 × 2_o))) → ((𝐴‘𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀‘𝑈)”⟩⟩) = ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))
131	33, 44, 44, 122, 130	syl13anc 1353	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀‘𝑈)”⟩⟩) = ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))
132	127, 129, 131	3eqtrd 2820	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘𝐴) = ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))
133		efgredlemb.7	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉))
134	2, 3, 4, 5	efgtval 18619	. . . . . . . . . . . . . 14 ⊢ (((𝐵‘𝐿) ∈ 𝑊 ∧ 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ 𝑉 ∈ (𝐼 × 2_o)) → (𝑄(𝑇‘(𝐵‘𝐿))𝑉) = ((𝐵‘𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩))
135	29, 14, 94, 134	syl3anc 1352	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄(𝑇‘(𝐵‘𝐿))𝑉) = ((𝐵‘𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩))
136		splval 13969	. . . . . . . . . . . . . 14 ⊢ (((𝐵‘𝐿) ∈ 𝑊 ∧ (𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ ⟨“𝑉(𝑀‘𝑉)”⟩ ∈ Word (𝐼 × 2_o))) → ((𝐵‘𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
137	29, 14, 14, 104, 136	syl13anc 1353	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵‘𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
138	133, 135, 137	3eqtrd 2820	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘𝐵) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
139	24, 132, 138	3eqtr3d 2824	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
140	116, 126, 139	3eqtr2d 2822	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
141		swrdcl 13814	. . . . . . . . . . . 12 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) → ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2_o))
142	34, 141	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2_o))
143		ccatcl 13743	. . . . . . . . . . . 12 ⊢ ((⟨“𝑈(𝑀‘𝑈)”⟩ ∈ Word (𝐼 × 2_o) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2_o)) → (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2_o))
144	122, 124, 143	syl2anc 576	. . . . . . . . . . 11 ⊢ (𝜑 → (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2_o))
145		ccatass 13757	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2_o) ∧ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2_o) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2_o)) → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))))
146	98, 142, 144, 145	syl3anc 1352	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))))
147		swrdcl 13814	. . . . . . . . . . . 12 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) → ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2_o))
148	30, 147	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2_o))
149		ccatass 13757	. . . . . . . . . . 11 ⊢ ((((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2_o) ∧ ⟨“𝑉(𝑀‘𝑉)”⟩ ∈ Word (𝐼 × 2_o) ∧ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2_o)) → ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
150	32, 104, 148, 149	syl3anc 1352	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
151	140, 146, 150	3eqtr3d 2824	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))) = (((𝐵‘𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
152		ccatcl 13743	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2_o) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2_o)) → (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2_o))
153	142, 144, 152	syl2anc 576	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2_o))
154		ccatcl 13743	. . . . . . . . . . 11 ⊢ ((⟨“𝑉(𝑀‘𝑉)”⟩ ∈ Word (𝐼 × 2_o) ∧ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2_o)) → (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) ∈ Word (𝐼 × 2_o))
155	104, 148, 154	syl2anc 576	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) ∈ Word (𝐼 × 2_o))
156		uztrn 12081	. . . . . . . . . . . . . 14 ⊢ (((♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘𝑃) ∧ 𝑃 ∈ (ℤ_≥‘𝑄)) → (♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘𝑄))
157	46, 111, 156	syl2anc 576	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘𝑄))
158		elfzuzb 12724	. . . . . . . . . . . . 13 ⊢ (𝑄 ∈ (0...(♯‘(𝐴‘𝐾))) ↔ (𝑄 ∈ (ℤ_≥‘0) ∧ (♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘𝑄)))
159	16, 157, 158	sylanbrc 575	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝐴‘𝐾))))
160		pfxlen 13871	. . . . . . . . . . . 12 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) ∧ 𝑄 ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) prefix 𝑄)) = 𝑄)
161	34, 159, 160	syl2anc 576	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) prefix 𝑄)) = 𝑄)
162	161, 40	eqtr4d 2819	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) prefix 𝑄)) = (♯‘((𝐵‘𝐿) prefix 𝑄)))
163		ccatopth 13913	. . . . . . . . . 10 ⊢ (((((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2_o) ∧ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2_o)) ∧ (((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2_o) ∧ (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) ∈ Word (𝐼 × 2_o)) ∧ (♯‘((𝐴‘𝐾) prefix 𝑄)) = (♯‘((𝐵‘𝐿) prefix 𝑄))) → ((((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))) = (((𝐵‘𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))) ↔ (((𝐴‘𝐾) prefix 𝑄) = ((𝐵‘𝐿) prefix 𝑄) ∧ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))))
164	98, 153, 32, 155, 162, 163	syl221anc 1362	. . . . . . . . 9 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))) = (((𝐵‘𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))) ↔ (((𝐴‘𝐾) prefix 𝑄) = ((𝐵‘𝐿) prefix 𝑄) ∧ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))))
165	151, 164	mpbid 224	. . . . . . . 8 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) = ((𝐵‘𝐿) prefix 𝑄) ∧ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
166	165	simpld 487	. . . . . . 7 ⊢ (𝜑 → ((𝐴‘𝐾) prefix 𝑄) = ((𝐵‘𝐿) prefix 𝑄))
167	166	oveq1d 6997	. . . . . 6 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
168		ccatrid 13756	. . . . . . . 8 ⊢ (((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2_o) → (((𝐴‘𝐾) prefix 𝑄) ++ ∅) = ((𝐴‘𝐾) prefix 𝑄))
169	98, 168	syl 17	. . . . . . 7 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ∅) = ((𝐴‘𝐾) prefix 𝑄))
170	169	oveq1d 6997	. . . . . 6 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ∅) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
171	167, 170, 17	3eqtr4rd 2827	. . . . 5 ⊢ (𝜑 → (𝑆‘𝐶) = ((((𝐴‘𝐾) prefix 𝑄) ++ ∅) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
172	161	eqcomd 2786	. . . . 5 ⊢ (𝜑 → 𝑄 = (♯‘((𝐴‘𝐾) prefix 𝑄)))
173		hash0 13549	. . . . . . 7 ⊢ (♯‘∅) = 0
174	173	oveq2i 6993	. . . . . 6 ⊢ (𝑄 + (♯‘∅)) = (𝑄 + 0)
175	63	addid1d 10646	. . . . . 6 ⊢ (𝜑 → (𝑄 + 0) = 𝑄)
176	174, 175	syl5req 2829	. . . . 5 ⊢ (𝜑 → 𝑄 = (𝑄 + (♯‘∅)))
177	98, 100, 36, 104, 171, 172, 176	splval2 13981	. . . 4 ⊢ (𝜑 → ((𝑆‘𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩) = ((((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
178		elfzuzb 12724	. . . . . . . . . . . . . 14 ⊢ (𝑄 ∈ (0...(𝑄 + 2)) ↔ (𝑄 ∈ (ℤ_≥‘0) ∧ (𝑄 + 2) ∈ (ℤ_≥‘𝑄)))
179	16, 109, 178	sylanbrc 575	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∈ (0...(𝑄 + 2)))
180		elfzuzb 12724	. . . . . . . . . . . . . 14 ⊢ ((𝑄 + 2) ∈ (0...𝑃) ↔ ((𝑄 + 2) ∈ (ℤ_≥‘0) ∧ 𝑃 ∈ (ℤ_≥‘(𝑄 + 2))))
181	43, 47, 180	sylanbrc 575	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄 + 2) ∈ (0...𝑃))
182		ccatswrd 13855	. . . . . . . . . . . . 13 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) ∧ (𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))))) → (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩))
183	34, 179, 181, 44, 182	syl13anc 1353	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩))
184	183	oveq1d 6997	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))))
185		swrdcl 13814	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) → ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2_o))
186	34, 185	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2_o))
187		swrdcl 13814	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2_o))
188	34, 187	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2_o))
189		ccatass 13757	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2_o) ∧ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2_o) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2_o)) → ((((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))))
190	186, 188, 144, 189	syl3anc 1352	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))))
191	165	simprd 488	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
192	184, 190, 191	3eqtr3d 2824	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
193		ccatcl 13743	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2_o) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2_o)) → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2_o))
194	188, 144, 193	syl2anc 576	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2_o))
195		swrdlen 13818	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝑄 + 2) − 𝑄))
196	34, 179, 51, 195	syl3anc 1352	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝑄 + 2) − 𝑄))
197		pncan2 10699	. . . . . . . . . . . . . 14 ⊢ ((𝑄 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑄 + 2) − 𝑄) = 2)
198	63, 70, 197	sylancl 578	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑄 + 2) − 𝑄) = 2)
199	196, 198	eqtrd 2816	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = 2)
200		s2len 14119	. . . . . . . . . . . 12 ⊢ (♯‘⟨“𝑉(𝑀‘𝑉)”⟩) = 2
201	199, 200	syl6eqr 2834	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (♯‘⟨“𝑉(𝑀‘𝑉)”⟩))
202		ccatopth 13913	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2_o) ∧ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2_o)) ∧ (⟨“𝑉(𝑀‘𝑉)”⟩ ∈ Word (𝐼 × 2_o) ∧ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2_o)) ∧ (♯‘((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (♯‘⟨“𝑉(𝑀‘𝑉)”⟩)) → ((((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) ↔ (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀‘𝑉)”⟩ ∧ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
203	186, 194, 104, 148, 201, 202	syl221anc 1362	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) ↔ (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀‘𝑉)”⟩ ∧ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
204	192, 203	mpbid 224	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀‘𝑉)”⟩ ∧ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
205	204	simpld 487	. . . . . . . 8 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀‘𝑉)”⟩)
206	205	oveq2d 6998	. . . . . . 7 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩))
207		ccatpfx 13889	. . . . . . . 8 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾)))) → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝐴‘𝐾) prefix (𝑄 + 2)))
208	34, 179, 51, 207	syl3anc 1352	. . . . . . 7 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝐴‘𝐾) prefix (𝑄 + 2)))
209	206, 208	eqtr3d 2818	. . . . . 6 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) = ((𝐴‘𝐾) prefix (𝑄 + 2)))
210	209	oveq1d 6997	. . . . 5 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (((𝐴‘𝐾) prefix (𝑄 + 2)) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
211		ccatpfx 13889	. . . . . 6 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾))) ∧ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾)))) → (((𝐴‘𝐾) prefix (𝑄 + 2)) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))))
212	34, 51, 57, 211	syl3anc 1352	. . . . 5 ⊢ (𝜑 → (((𝐴‘𝐾) prefix (𝑄 + 2)) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))))
213		pfxid 13872	. . . . . 6 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) → ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))) = (𝐴‘𝐾))
214	34, 213	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))) = (𝐴‘𝐾))
215	210, 212, 214	3eqtrd 2820	. . . 4 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (𝐴‘𝐾))
216	96, 177, 215	3eqtrd 2820	. . 3 ⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = (𝐴‘𝐾))
217	2, 3, 4, 5	efgtf 18618	. . . . . . 7 ⊢ ((𝑆‘𝐶) ∈ 𝑊 → ((𝑇‘(𝑆‘𝐶)) = (𝑎 ∈ (0...(♯‘(𝑆‘𝐶))), 𝑖 ∈ (𝐼 × 2_o) ↦ ((𝑆‘𝐶) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀‘𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆‘𝐶)):((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2_o))⟶𝑊))
218	13, 217	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝑇‘(𝑆‘𝐶)) = (𝑎 ∈ (0...(♯‘(𝑆‘𝐶))), 𝑖 ∈ (𝐼 × 2_o) ↦ ((𝑆‘𝐶) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀‘𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆‘𝐶)):((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2_o))⟶𝑊))
219	218	simprd 488	. . . . 5 ⊢ (𝜑 → (𝑇‘(𝑆‘𝐶)):((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2_o))⟶𝑊)
220	219	ffnd 6350	. . . 4 ⊢ (𝜑 → (𝑇‘(𝑆‘𝐶)) Fn ((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2_o)))
221		fnovrn 7145	. . . 4 ⊢ (((𝑇‘(𝑆‘𝐶)) Fn ((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2_o)) ∧ 𝑄 ∈ (0...(♯‘(𝑆‘𝐶))) ∧ 𝑉 ∈ (𝐼 × 2_o)) → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) ∈ ran (𝑇‘(𝑆‘𝐶)))
222	220, 93, 94, 221	syl3anc 1352	. . 3 ⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) ∈ ran (𝑇‘(𝑆‘𝐶)))
223	216, 222	eqeltrrd 2869	. 2 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶)))
224		uztrn 12081	. . . . . . 7 ⊢ (((𝑃 − 2) ∈ (ℤ_≥‘𝑄) ∧ 𝑄 ∈ (ℤ_≥‘0)) → (𝑃 − 2) ∈ (ℤ_≥‘0))
225	89, 16, 224	syl2anc 576	. . . . . 6 ⊢ (𝜑 → (𝑃 − 2) ∈ (ℤ_≥‘0))
226		elfzuzb 12724	. . . . . 6 ⊢ ((𝑃 − 2) ∈ (0...(♯‘(𝑆‘𝐶))) ↔ ((𝑃 − 2) ∈ (ℤ_≥‘0) ∧ (♯‘(𝑆‘𝐶)) ∈ (ℤ_≥‘(𝑃 − 2))))
227	225, 87, 226	sylanbrc 575	. . . . 5 ⊢ (𝜑 → (𝑃 − 2) ∈ (0...(♯‘(𝑆‘𝐶))))
228	2, 3, 4, 5	efgtval 18619	. . . . 5 ⊢ (((𝑆‘𝐶) ∈ 𝑊 ∧ (𝑃 − 2) ∈ (0...(♯‘(𝑆‘𝐶))) ∧ 𝑈 ∈ (𝐼 × 2_o)) → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = ((𝑆‘𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀‘𝑈)”⟩⟩))
229	13, 227, 119, 228	syl3anc 1352	. . . 4 ⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = ((𝑆‘𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀‘𝑈)”⟩⟩))
230		pfxcl 13865	. . . . . 6 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) → ((𝐵‘𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2_o))
231	30, 230	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐵‘𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2_o))
232		swrdcl 13814	. . . . . 6 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) → ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2_o))
233	30, 232	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2_o))
234		ccatswrd 13855	. . . . . . . . . . 11 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) ∧ ((𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾))))) → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))
235	34, 181, 44, 57, 234	syl13anc 1353	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))
236	204	simprd 488	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))
237		elfzuzb 12724	. . . . . . . . . . . . . . . 16 ⊢ (𝑄 ∈ (0...(𝑃 − 2)) ↔ (𝑄 ∈ (ℤ_≥‘0) ∧ (𝑃 − 2) ∈ (ℤ_≥‘𝑄)))
238	16, 89, 237	sylanbrc 575	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑄 ∈ (0...(𝑃 − 2)))
239	2, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27, 44, 14, 119, 94, 127, 133	efgredlemg 18639	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) = (♯‘(𝐵‘𝐿)))
240	239, 46	eqeltrrd 2869	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ (ℤ_≥‘𝑃))
241		0le2 11555	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ≤ 2
242	241	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 ≤ 2)
243	76	zred 11906	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑃 ∈ ℝ)
244		2re 11520	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℝ
245		subge02 10963	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃 ∈ ℝ ∧ 2 ∈ ℝ) → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃))
246	243, 244, 245	sylancl 578	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃))
247	242, 246	mpbid 224	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑃 − 2) ≤ 𝑃)
248		eluz2 12070	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ (ℤ_≥‘(𝑃 − 2)) ↔ ((𝑃 − 2) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑃 − 2) ≤ 𝑃))
249	78, 76, 247, 248	syl3anbrc 1324	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ (ℤ_≥‘(𝑃 − 2)))
250		uztrn 12081	. . . . . . . . . . . . . . . . 17 ⊢ (((♯‘(𝐵‘𝐿)) ∈ (ℤ_≥‘𝑃) ∧ 𝑃 ∈ (ℤ_≥‘(𝑃 − 2))) → (♯‘(𝐵‘𝐿)) ∈ (ℤ_≥‘(𝑃 − 2)))
251	240, 249, 250	syl2anc 576	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ (ℤ_≥‘(𝑃 − 2)))
252		elfzuzb 12724	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿))) ↔ ((𝑃 − 2) ∈ (ℤ_≥‘0) ∧ (♯‘(𝐵‘𝐿)) ∈ (ℤ_≥‘(𝑃 − 2))))
253	225, 251, 252	sylanbrc 575	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿))))
254		lencl 13700	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) → (♯‘(𝐵‘𝐿)) ∈ ℕ₀)
255	30, 254	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ ℕ₀)
256	255, 54	syl6eleq 2878	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ (ℤ_≥‘0))
257		eluzfz2 12737	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘(𝐵‘𝐿)) ∈ (ℤ_≥‘0) → (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))
258	256, 257	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))
259		ccatswrd 13855	. . . . . . . . . . . . . . 15 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) ∧ (𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿))) ∧ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))) → (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))
260	30, 238, 253, 258, 259	syl13anc 1353	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))
261	236, 260	eqtr4d 2819	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)))
262		swrdcl 13814	. . . . . . . . . . . . . . 15 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) → ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2_o))
263	30, 262	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2_o))
264		swrdcl 13814	. . . . . . . . . . . . . . 15 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) → ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2_o))
265	30, 264	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2_o))
266		swrdlen 13818	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (𝑃 − (𝑄 + 2)))
267	34, 181, 44, 266	syl3anc 1352	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (𝑃 − (𝑄 + 2)))
268		swrdlen 13818	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝑃 − 2) − 𝑄))
269	30, 238, 253, 268	syl3anc 1352	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝑃 − 2) − 𝑄))
270	80, 63, 71	sub32d 10836	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑃 − 𝑄) − 2) = ((𝑃 − 2) − 𝑄))
271	80, 63, 71	subsub4d 10835	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑃 − 𝑄) − 2) = (𝑃 − (𝑄 + 2)))
272	269, 270, 271	3eqtr2d 2822	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = (𝑃 − (𝑄 + 2)))
273	267, 272	eqtr4d 2819	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (♯‘((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)))
274		ccatopth 13913	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2_o) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2_o)) ∧ (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2_o) ∧ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2_o)) ∧ (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (♯‘((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩))) → ((((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)) ↔ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩))))
275	188, 144, 263, 265, 273, 274	syl221anc 1362	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)) ↔ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩))))
276	261, 275	mpbid 224	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)))
277	276	simpld 487	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩))
278	276	simprd 488	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩))
279		elfzuzb 12724	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 − 2) ∈ (0...𝑃) ↔ ((𝑃 − 2) ∈ (ℤ_≥‘0) ∧ 𝑃 ∈ (ℤ_≥‘(𝑃 − 2))))
280	225, 249, 279	sylanbrc 575	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 − 2) ∈ (0...𝑃))
281		elfzuz 12726	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) → 𝑃 ∈ (ℤ_≥‘0))
282	44, 281	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ (ℤ_≥‘0))
283		elfzuzb 12724	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ (0...(♯‘(𝐵‘𝐿))) ↔ (𝑃 ∈ (ℤ_≥‘0) ∧ (♯‘(𝐵‘𝐿)) ∈ (ℤ_≥‘𝑃)))
284	282, 240, 283	sylanbrc 575	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ (0...(♯‘(𝐵‘𝐿))))
285		ccatswrd 13855	. . . . . . . . . . . . . . 15 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) ∧ ((𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))) → (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩))
286	30, 280, 284, 258, 285	syl13anc 1353	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩))
287	278, 286	eqtr4d 2819	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
288		swrdcl 13814	. . . . . . . . . . . . . . 15 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) → ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2_o))
289	30, 288	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2_o))
290		s2len 14119	. . . . . . . . . . . . . . 15 ⊢ (♯‘⟨“𝑈(𝑀‘𝑈)”⟩) = 2
291		swrdlen 13818	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = (𝑃 − (𝑃 − 2)))
292	30, 280, 284, 291	syl3anc 1352	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = (𝑃 − (𝑃 − 2)))
293		nncan 10722	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑃 − (𝑃 − 2)) = 2)
294	80, 70, 293	sylancl 578	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃 − (𝑃 − 2)) = 2)
295	292, 294	eqtr2d 2817	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 = (♯‘((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
296	290, 295	syl5eq 2828	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘⟨“𝑈(𝑀‘𝑈)”⟩) = (♯‘((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
297		ccatopth 13913	. . . . . . . . . . . . . 14 ⊢ (((⟨“𝑈(𝑀‘𝑈)”⟩ ∈ Word (𝐼 × 2_o) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2_o)) ∧ (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2_o) ∧ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2_o)) ∧ (♯‘⟨“𝑈(𝑀‘𝑈)”⟩) = (♯‘((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩))) → ((⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) ↔ (⟨“𝑈(𝑀‘𝑈)”⟩ = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) = ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))))
298	122, 124, 289, 233, 296, 297	syl221anc 1362	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) ↔ (⟨“𝑈(𝑀‘𝑈)”⟩ = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) = ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))))
299	287, 298	mpbid 224	. . . . . . . . . . . 12 ⊢ (𝜑 → (⟨“𝑈(𝑀‘𝑈)”⟩ = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) = ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
300	299	simprd 488	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) = ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))
301	277, 300	oveq12d 7000	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
302	235, 301	eqtr3d 2818	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩) = (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
303	302	oveq2d 6998	. . . . . . . 8 ⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))))
304		ccatass 13757	. . . . . . . . 9 ⊢ ((((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2_o) ∧ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2_o) ∧ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2_o)) → ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))))
305	32, 263, 233, 304	syl3anc 1352	. . . . . . . 8 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))))
306	303, 305	eqtr4d 2819	. . . . . . 7 ⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
307		ccatpfx 13889	. . . . . . . . 9 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿)))) → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝐵‘𝐿) prefix (𝑃 − 2)))
308	30, 238, 253, 307	syl3anc 1352	. . . . . . . 8 ⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝐵‘𝐿) prefix (𝑃 − 2)))
309	308	oveq1d 6997	. . . . . . 7 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
310	17, 306, 309	3eqtrd 2820	. . . . . 6 ⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
311		ccatrid 13756	. . . . . . . 8 ⊢ (((𝐵‘𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2_o) → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) = ((𝐵‘𝐿) prefix (𝑃 − 2)))
312	231, 311	syl 17	. . . . . . 7 ⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) = ((𝐵‘𝐿) prefix (𝑃 − 2)))
313	312	oveq1d 6997	. . . . . 6 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
314	310, 313	eqtr4d 2819	. . . . 5 ⊢ (𝜑 → (𝑆‘𝐶) = ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
315		pfxlen 13871	. . . . . . 7 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) prefix (𝑃 − 2))) = (𝑃 − 2))
316	30, 253, 315	syl2anc 576	. . . . . 6 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) prefix (𝑃 − 2))) = (𝑃 − 2))
317	316	eqcomd 2786	. . . . 5 ⊢ (𝜑 → (𝑃 − 2) = (♯‘((𝐵‘𝐿) prefix (𝑃 − 2))))
318	173	oveq2i 6993	. . . . . 6 ⊢ ((𝑃 − 2) + (♯‘∅)) = ((𝑃 − 2) + 0)
319	78	zcnd 11907	. . . . . . 7 ⊢ (𝜑 → (𝑃 − 2) ∈ ℂ)
320	319	addid1d 10646	. . . . . 6 ⊢ (𝜑 → ((𝑃 − 2) + 0) = (𝑃 − 2))
321	318, 320	syl5req 2829	. . . . 5 ⊢ (𝜑 → (𝑃 − 2) = ((𝑃 − 2) + (♯‘∅)))
322	231, 100, 233, 122, 314, 317, 321	splval2 13981	. . . 4 ⊢ (𝜑 → ((𝑆‘𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀‘𝑈)”⟩⟩) = ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
323	299	simpld 487	. . . . . . . 8 ⊢ (𝜑 → ⟨“𝑈(𝑀‘𝑈)”⟩ = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩))
324	323	oveq2d 6998	. . . . . . 7 ⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
325		ccatpfx 13889	. . . . . . . 8 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿)))) → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = ((𝐵‘𝐿) prefix 𝑃))
326	30, 280, 284, 325	syl3anc 1352	. . . . . . 7 ⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = ((𝐵‘𝐿) prefix 𝑃))
327	324, 326	eqtrd 2816	. . . . . 6 ⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) = ((𝐵‘𝐿) prefix 𝑃))
328	327	oveq1d 6997	. . . . 5 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑃) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
329		ccatpfx 13889	. . . . . 6 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿)))) → (((𝐵‘𝐿) prefix 𝑃) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))))
330	30, 284, 258, 329	syl3anc 1352	. . . . 5 ⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑃) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))))
331		pfxid 13872	. . . . . 6 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) → ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))) = (𝐵‘𝐿))
332	30, 331	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))) = (𝐵‘𝐿))
333	328, 330, 332	3eqtrd 2820	. . . 4 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (𝐵‘𝐿))
334	229, 322, 333	3eqtrd 2820	. . 3 ⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = (𝐵‘𝐿))
335		fnovrn 7145	. . . 4 ⊢ (((𝑇‘(𝑆‘𝐶)) Fn ((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2_o)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝑆‘𝐶))) ∧ 𝑈 ∈ (𝐼 × 2_o)) → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) ∈ ran (𝑇‘(𝑆‘𝐶)))
336	220, 227, 119, 335	syl3anc 1352	. . 3 ⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) ∈ ran (𝑇‘(𝑆‘𝐶)))
337	334, 336	eqeltrrd 2869	. 2 ⊢ (𝜑 → (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶)))
338	223, 337	jca 504	1 ⊢ (𝜑 → ((𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶)) ∧ (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 387 = wceq 1508 ∈ wcel 2051 ∀wral 3090 {crab 3094 ∖ cdif 3828 ∅c0 4181 {csn 4444 ⟨cop 4450 ⟨cotp 4452 ∪ ciun 4797 class class class wbr 4934 ↦ cmpt 5013 I cid 5315 × cxp 5409 dom cdm 5411 ran crn 5412 Fn wfn 6188 ⟶wf 6189 ‘cfv 6193 (class class class)co 6982 ∈ cmpo 6984 1_oc1o 7904 2_oc2o 7905 ℂcc 10339 ℝcr 10340 0cc0 10341 1c1 10342 + caddc 10344 < clt 10480 ≤ cle 10481 − cmin 10676 2c2 11501 ℕ₀cn0 11713 ℤcz 11799 ℤ_≥cuz 12064 ...cfz 12714 ..^cfzo 12855 ♯chash 13511 Word cword 13678 ++ cconcat 13739 substr csubstr 13809 prefix cpfx 13858 splice csplice 13964 ⟨“cs2 14071 ~_FG cefg 18602

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2752 ax-rep 5053 ax-sep 5064 ax-nul 5071 ax-pow 5123 ax-pr 5190 ax-un 7285 ax-cnex 10397 ax-resscn 10398 ax-1cn 10399 ax-icn 10400 ax-addcl 10401 ax-addrcl 10402 ax-mulcl 10403 ax-mulrcl 10404 ax-mulcom 10405 ax-addass 10406 ax-mulass 10407 ax-distr 10408 ax-i2m1 10409 ax-1ne0 10410 ax-1rid 10411 ax-rnegex 10412 ax-rrecex 10413 ax-cnre 10414 ax-pre-lttri 10415 ax-pre-lttrn 10416 ax-pre-ltadd 10417 ax-pre-mulgt0 10418

This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3or 1070 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2551 df-eu 2589 df-clab 2761 df-cleq 2773 df-clel 2848 df-nfc 2920 df-ne 2970 df-nel 3076 df-ral 3095 df-rex 3096 df-reu 3097 df-rab 3099 df-v 3419 df-sbc 3684 df-csb 3789 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-pss 3847 df-nul 4182 df-if 4354 df-pw 4427 df-sn 4445 df-pr 4447 df-tp 4449 df-op 4451 df-ot 4453 df-uni 4718 df-int 4755 df-iun 4799 df-br 4935 df-opab 4997 df-mpt 5014 df-tr 5036 df-id 5316 df-eprel 5321 df-po 5330 df-so 5331 df-fr 5370 df-we 5372 df-xp 5417 df-rel 5418 df-cnv 5419 df-co 5420 df-dm 5421 df-rn 5422 df-res 5423 df-ima 5424 df-pred 5991 df-ord 6037 df-on 6038 df-lim 6039 df-suc 6040 df-iota 6157 df-fun 6195 df-fn 6196 df-f 6197 df-f1 6198 df-fo 6199 df-f1o 6200 df-fv 6201 df-riota 6943 df-ov 6985 df-oprab 6986 df-mpo 6987 df-om 7403 df-1st 7507 df-2nd 7508 df-wrecs 7756 df-recs 7818 df-rdg 7856 df-1o 7911 df-2o 7912 df-oadd 7915 df-er 8095 df-map 8214 df-en 8313 df-dom 8314 df-sdom 8315 df-fin 8316 df-card 9168 df-pnf 10482 df-mnf 10483 df-xr 10484 df-ltxr 10485 df-le 10486 df-sub 10678 df-neg 10679 df-nn 11446 df-2 11509 df-n0 11714 df-z 11800 df-uz 12065 df-fz 12715 df-fzo 12856 df-hash 13512 df-word 13679 df-concat 13740 df-s1 13765 df-substr 13810 df-pfx 13859 df-splice 13966 df-s2 14078

This theorem is referenced by: efgredlemd 18641

W3C validator