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 19133

Description: Lemma for efgred 19138. (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 19119	. . . . . . . 8 ⊢ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊
9	8	fdmi 6557	. . . . . . . . 9 ⊢ dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}
10	9	feq2i 6537	. . . . . . . 8 ⊢ (𝑆:dom 𝑆⟶𝑊 ↔ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊)
11	8, 10	mpbir 234	. . . . . . 7 ⊢ 𝑆:dom 𝑆⟶𝑊
12	11	ffvelrni 6903	. . . . . 6 ⊢ (𝐶 ∈ dom 𝑆 → (𝑆‘𝐶) ∈ 𝑊)
13	1, 12	syl 17	. . . . 5 ⊢ (𝜑 → (𝑆‘𝐶) ∈ 𝑊)
14		efgredlemb.q	. . . . . . 7 ⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))))
15		elfzuz 13108	. . . . . . 7 ⊢ (𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) → 𝑄 ∈ (ℤ_≥‘0))
16	14, 15	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑄 ∈ (ℤ_≥‘0))
17		efgredlemd.sc	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
18	17	fveq2d 6721	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(𝑆‘𝐶)) = (♯‘(((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))))
19		fviss 6788	. . . . . . . . . . . . 13 ⊢ ( I ‘Word (𝐼 × 2_o)) ⊆ Word (𝐼 × 2_o)
20	2, 19	eqsstri 3935	. . . . . . . . . . . 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 19131	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝐾) ∈ 𝑊 ∧ (𝐵‘𝐿) ∈ 𝑊))
29	28	simprd 499	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵‘𝐿) ∈ 𝑊)
30	20, 29	sseldi 3899	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵‘𝐿) ∈ Word (𝐼 × 2_o))
31		pfxcl 14242	. . . . . . . . . . 11 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) → ((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2_o))
32	30, 31	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2_o))
33	28	simpld 498	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴‘𝐾) ∈ 𝑊)
34	20, 33	sseldi 3899	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴‘𝐾) ∈ Word (𝐼 × 2_o))
35		swrdcl 14210	. . . . . . . . . . 11 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2_o))
36	34, 35	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2_o))
37		ccatlen 14130	. . . . . . . . . 10 ⊢ ((((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2_o) ∧ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2_o)) → (♯‘(((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))) = ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))))
38	32, 36, 37	syl2anc 587	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))) = ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))))
39		pfxlen 14248	. . . . . . . . . . . 12 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) ∧ 𝑄 ∈ (0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) prefix 𝑄)) = 𝑄)
40	30, 14, 39	syl2anc 587	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) prefix 𝑄)) = 𝑄)
41		2nn0 12107	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ₀
42		uzaddcl 12500	. . . . . . . . . . . . . 14 ⊢ ((𝑄 ∈ (ℤ_≥‘0) ∧ 2 ∈ ℕ₀) → (𝑄 + 2) ∈ (ℤ_≥‘0))
43	16, 41, 42	sylancl 589	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄 + 2) ∈ (ℤ_≥‘0))
44		efgredlemb.p	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))))
45		elfzuz3 13109	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) → (♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘𝑃))
46	44, 45	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘𝑃))
47		efgredlemd.9	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ (ℤ_≥‘(𝑄 + 2)))
48		uztrn 12456	. . . . . . . . . . . . . 14 ⊢ (((♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘𝑃) ∧ 𝑃 ∈ (ℤ_≥‘(𝑄 + 2))) → (♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘(𝑄 + 2)))
49	46, 47, 48	syl2anc 587	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘(𝑄 + 2)))
50		elfzuzb 13106	. . . . . . . . . . . . 13 ⊢ ((𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾))) ↔ ((𝑄 + 2) ∈ (ℤ_≥‘0) ∧ (♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘(𝑄 + 2))))
51	43, 49, 50	sylanbrc 586	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾))))
52		lencl 14088	. . . . . . . . . . . . . . 15 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) → (♯‘(𝐴‘𝐾)) ∈ ℕ₀)
53	34, 52	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ ℕ₀)
54		nn0uz 12476	. . . . . . . . . . . . . 14 ⊢ ℕ₀ = (ℤ_≥‘0)
55	53, 54	eleqtrdi 2848	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘0))
56		eluzfz2 13120	. . . . . . . . . . . . 13 ⊢ ((♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘0) → (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾))))
57	55, 56	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾))))
58		swrdlen 14212	. . . . . . . . . . . 12 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾))) ∧ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((♯‘(𝐴‘𝐾)) − (𝑄 + 2)))
59	34, 51, 57, 58	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((♯‘(𝐴‘𝐾)) − (𝑄 + 2)))
60	40, 59	oveq12d 7231	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))) = (𝑄 + ((♯‘(𝐴‘𝐾)) − (𝑄 + 2))))
61	14	elfzelzd 13113	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ ℤ)
62	61	zcnd 12283	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ ℂ)
63	53	nn0cnd 12152	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ ℂ)
64		2z 12209	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℤ
65		zaddcl 12217	. . . . . . . . . . . . 13 ⊢ ((𝑄 ∈ ℤ ∧ 2 ∈ ℤ) → (𝑄 + 2) ∈ ℤ)
66	61, 64, 65	sylancl 589	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄 + 2) ∈ ℤ)
67	66	zcnd 12283	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄 + 2) ∈ ℂ)
68	62, 63, 67	addsubassd 11209	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑄 + (♯‘(𝐴‘𝐾))) − (𝑄 + 2)) = (𝑄 + ((♯‘(𝐴‘𝐾)) − (𝑄 + 2))))
69		2cn 11905	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
70	69	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℂ)
71	62, 63, 70	pnpcand 11226	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑄 + (♯‘(𝐴‘𝐾))) − (𝑄 + 2)) = ((♯‘(𝐴‘𝐾)) − 2))
72	60, 68, 71	3eqtr2d 2783	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))) = ((♯‘(𝐴‘𝐾)) − 2))
73	18, 38, 72	3eqtrd 2781	. . . . . . . 8 ⊢ (𝜑 → (♯‘(𝑆‘𝐶)) = ((♯‘(𝐴‘𝐾)) − 2))
74	44	elfzelzd 13113	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ ℤ)
75		zsubcl 12219	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℤ ∧ 2 ∈ ℤ) → (𝑃 − 2) ∈ ℤ)
76	74, 64, 75	sylancl 589	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 − 2) ∈ ℤ)
77	64	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 2 ∈ ℤ)
78	74	zcnd 12283	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℂ)
79		npcan 11087	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑃 − 2) + 2) = 𝑃)
80	78, 69, 79	sylancl 589	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑃 − 2) + 2) = 𝑃)
81	80	fveq2d 6721	. . . . . . . . . 10 ⊢ (𝜑 → (ℤ_≥‘((𝑃 − 2) + 2)) = (ℤ_≥‘𝑃))
82	46, 81	eleqtrrd 2841	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘((𝑃 − 2) + 2)))
83		eluzsub 12470	. . . . . . . . 9 ⊢ (((𝑃 − 2) ∈ ℤ ∧ 2 ∈ ℤ ∧ (♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘((𝑃 − 2) + 2))) → ((♯‘(𝐴‘𝐾)) − 2) ∈ (ℤ_≥‘(𝑃 − 2)))
84	76, 77, 82, 83	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → ((♯‘(𝐴‘𝐾)) − 2) ∈ (ℤ_≥‘(𝑃 − 2)))
85	73, 84	eqeltrd 2838	. . . . . . 7 ⊢ (𝜑 → (♯‘(𝑆‘𝐶)) ∈ (ℤ_≥‘(𝑃 − 2)))
86		eluzsub 12470	. . . . . . . 8 ⊢ ((𝑄 ∈ ℤ ∧ 2 ∈ ℤ ∧ 𝑃 ∈ (ℤ_≥‘(𝑄 + 2))) → (𝑃 − 2) ∈ (ℤ_≥‘𝑄))
87	61, 77, 47, 86	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → (𝑃 − 2) ∈ (ℤ_≥‘𝑄))
88		uztrn 12456	. . . . . . 7 ⊢ (((♯‘(𝑆‘𝐶)) ∈ (ℤ_≥‘(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (ℤ_≥‘𝑄)) → (♯‘(𝑆‘𝐶)) ∈ (ℤ_≥‘𝑄))
89	85, 87, 88	syl2anc 587	. . . . . 6 ⊢ (𝜑 → (♯‘(𝑆‘𝐶)) ∈ (ℤ_≥‘𝑄))
90		elfzuzb 13106	. . . . . 6 ⊢ (𝑄 ∈ (0...(♯‘(𝑆‘𝐶))) ↔ (𝑄 ∈ (ℤ_≥‘0) ∧ (♯‘(𝑆‘𝐶)) ∈ (ℤ_≥‘𝑄)))
91	16, 89, 90	sylanbrc 586	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝑆‘𝐶))))
92		efgredlemb.v	. . . . 5 ⊢ (𝜑 → 𝑉 ∈ (𝐼 × 2_o))
93	2, 3, 4, 5	efgtval 19113	. . . . 5 ⊢ (((𝑆‘𝐶) ∈ 𝑊 ∧ 𝑄 ∈ (0...(♯‘(𝑆‘𝐶))) ∧ 𝑉 ∈ (𝐼 × 2_o)) → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = ((𝑆‘𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩))
94	13, 91, 92, 93	syl3anc 1373	. . . 4 ⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = ((𝑆‘𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩))
95		pfxcl 14242	. . . . . 6 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) → ((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2_o))
96	34, 95	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2_o))
97		wrd0 14094	. . . . . 6 ⊢ ∅ ∈ Word (𝐼 × 2_o)
98	97	a1i 11	. . . . 5 ⊢ (𝜑 → ∅ ∈ Word (𝐼 × 2_o))
99	4	efgmf 19103	. . . . . . . 8 ⊢ 𝑀:(𝐼 × 2_o)⟶(𝐼 × 2_o)
100	99	ffvelrni 6903	. . . . . . 7 ⊢ (𝑉 ∈ (𝐼 × 2_o) → (𝑀‘𝑉) ∈ (𝐼 × 2_o))
101	92, 100	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑀‘𝑉) ∈ (𝐼 × 2_o))
102	92, 101	s2cld 14436	. . . . 5 ⊢ (𝜑 → ⟨“𝑉(𝑀‘𝑉)”⟩ ∈ Word (𝐼 × 2_o))
103	61	zred 12282	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄 ∈ ℝ)
104		nn0addge1 12136	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄 ∈ ℝ ∧ 2 ∈ ℕ₀) → 𝑄 ≤ (𝑄 + 2))
105	103, 41, 104	sylancl 589	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑄 ≤ (𝑄 + 2))
106		eluz2 12444	. . . . . . . . . . . . . . . 16 ⊢ ((𝑄 + 2) ∈ (ℤ_≥‘𝑄) ↔ (𝑄 ∈ ℤ ∧ (𝑄 + 2) ∈ ℤ ∧ 𝑄 ≤ (𝑄 + 2)))
107	61, 66, 105, 106	syl3anbrc 1345	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑄 + 2) ∈ (ℤ_≥‘𝑄))
108		uztrn 12456	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℤ_≥‘(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (ℤ_≥‘𝑄)) → 𝑃 ∈ (ℤ_≥‘𝑄))
109	47, 107, 108	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ (ℤ_≥‘𝑄))
110		elfzuzb 13106	. . . . . . . . . . . . . 14 ⊢ (𝑄 ∈ (0...𝑃) ↔ (𝑄 ∈ (ℤ_≥‘0) ∧ 𝑃 ∈ (ℤ_≥‘𝑄)))
111	16, 109, 110	sylanbrc 586	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∈ (0...𝑃))
112		ccatpfx 14266	. . . . . . . . . . . . 13 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) ∧ 𝑄 ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾)))) → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) = ((𝐴‘𝐾) prefix 𝑃))
113	34, 111, 44, 112	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) = ((𝐴‘𝐾) prefix 𝑃))
114	113	oveq1d 7228	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) prefix 𝑃) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))))
115		pfxcl 14242	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) → ((𝐴‘𝐾) prefix 𝑃) ∈ Word (𝐼 × 2_o))
116	34, 115	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) prefix 𝑃) ∈ Word (𝐼 × 2_o))
117		efgredlemb.u	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ∈ (𝐼 × 2_o))
118	99	ffvelrni 6903	. . . . . . . . . . . . . 14 ⊢ (𝑈 ∈ (𝐼 × 2_o) → (𝑀‘𝑈) ∈ (𝐼 × 2_o))
119	117, 118	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀‘𝑈) ∈ (𝐼 × 2_o))
120	117, 119	s2cld 14436	. . . . . . . . . . . 12 ⊢ (𝜑 → ⟨“𝑈(𝑀‘𝑈)”⟩ ∈ Word (𝐼 × 2_o))
121		swrdcl 14210	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) → ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2_o))
122	34, 121	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2_o))
123		ccatass 14145	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝐾) prefix 𝑃) ∈ Word (𝐼 × 2_o) ∧ ⟨“𝑈(𝑀‘𝑈)”⟩ ∈ Word (𝐼 × 2_o) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2_o)) → ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐴‘𝐾) prefix 𝑃) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))))
124	116, 120, 122, 123	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐴‘𝐾) prefix 𝑃) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))))
125		efgredlemb.6	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈))
126	2, 3, 4, 5	efgtval 19113	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝐾) ∈ 𝑊 ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ 𝑈 ∈ (𝐼 × 2_o)) → (𝑃(𝑇‘(𝐴‘𝐾))𝑈) = ((𝐴‘𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀‘𝑈)”⟩⟩))
127	33, 44, 117, 126	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃(𝑇‘(𝐴‘𝐾))𝑈) = ((𝐴‘𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀‘𝑈)”⟩⟩))
128		splval 14316	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝐾) ∈ 𝑊 ∧ (𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ ⟨“𝑈(𝑀‘𝑈)”⟩ ∈ Word (𝐼 × 2_o))) → ((𝐴‘𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀‘𝑈)”⟩⟩) = ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))
129	33, 44, 44, 120, 128	syl13anc 1374	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀‘𝑈)”⟩⟩) = ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))
130	125, 127, 129	3eqtrd 2781	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘𝐴) = ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))
131		efgredlemb.7	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉))
132	2, 3, 4, 5	efgtval 19113	. . . . . . . . . . . . . 14 ⊢ (((𝐵‘𝐿) ∈ 𝑊 ∧ 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ 𝑉 ∈ (𝐼 × 2_o)) → (𝑄(𝑇‘(𝐵‘𝐿))𝑉) = ((𝐵‘𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩))
133	29, 14, 92, 132	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄(𝑇‘(𝐵‘𝐿))𝑉) = ((𝐵‘𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩))
134		splval 14316	. . . . . . . . . . . . . 14 ⊢ (((𝐵‘𝐿) ∈ 𝑊 ∧ (𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ ⟨“𝑉(𝑀‘𝑉)”⟩ ∈ Word (𝐼 × 2_o))) → ((𝐵‘𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
135	29, 14, 14, 102, 134	syl13anc 1374	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵‘𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
136	131, 133, 135	3eqtrd 2781	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘𝐵) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
137	24, 130, 136	3eqtr3d 2785	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
138	114, 124, 137	3eqtr2d 2783	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
139		swrdcl 14210	. . . . . . . . . . . 12 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) → ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2_o))
140	34, 139	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2_o))
141		ccatcl 14129	. . . . . . . . . . . 12 ⊢ ((⟨“𝑈(𝑀‘𝑈)”⟩ ∈ Word (𝐼 × 2_o) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) ∈ Word (𝐼 × 2_o)) → (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2_o))
142	120, 122, 141	syl2anc 587	. . . . . . . . . . 11 ⊢ (𝜑 → (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2_o))
143		ccatass 14145	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2_o) ∧ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2_o) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2_o)) → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))))
144	96, 140, 142, 143	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))))
145		swrdcl 14210	. . . . . . . . . . . 12 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) → ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2_o))
146	30, 145	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2_o))
147		ccatass 14145	. . . . . . . . . . 11 ⊢ ((((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2_o) ∧ ⟨“𝑉(𝑀‘𝑉)”⟩ ∈ Word (𝐼 × 2_o) ∧ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2_o)) → ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
148	32, 102, 146, 147	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
149	138, 144, 148	3eqtr3d 2785	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))) = (((𝐵‘𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
150		ccatcl 14129	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2_o) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2_o)) → (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2_o))
151	140, 142, 150	syl2anc 587	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2_o))
152		ccatcl 14129	. . . . . . . . . . 11 ⊢ ((⟨“𝑉(𝑀‘𝑉)”⟩ ∈ Word (𝐼 × 2_o) ∧ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2_o)) → (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) ∈ Word (𝐼 × 2_o))
153	102, 146, 152	syl2anc 587	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)) ∈ Word (𝐼 × 2_o))
154		uztrn 12456	. . . . . . . . . . . . . 14 ⊢ (((♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘𝑃) ∧ 𝑃 ∈ (ℤ_≥‘𝑄)) → (♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘𝑄))
155	46, 109, 154	syl2anc 587	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘𝑄))
156		elfzuzb 13106	. . . . . . . . . . . . 13 ⊢ (𝑄 ∈ (0...(♯‘(𝐴‘𝐾))) ↔ (𝑄 ∈ (ℤ_≥‘0) ∧ (♯‘(𝐴‘𝐾)) ∈ (ℤ_≥‘𝑄)))
157	16, 155, 156	sylanbrc 586	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝐴‘𝐾))))
158		pfxlen 14248	. . . . . . . . . . . 12 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) ∧ 𝑄 ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) prefix 𝑄)) = 𝑄)
159	34, 157, 158	syl2anc 587	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) prefix 𝑄)) = 𝑄)
160	159, 40	eqtr4d 2780	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) prefix 𝑄)) = (♯‘((𝐵‘𝐿) prefix 𝑄)))
161		ccatopth 14281	. . . . . . . . . 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 ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))))
162	96, 151, 32, 153, 160, 161	syl221anc 1383	. . . . . . . . 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 498	. . . . . . 7 ⊢ (𝜑 → ((𝐴‘𝐾) prefix 𝑄) = ((𝐵‘𝐿) prefix 𝑄))
165	164	oveq1d 7228	. . . . . 6 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
166		ccatrid 14144	. . . . . . . 8 ⊢ (((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2_o) → (((𝐴‘𝐾) prefix 𝑄) ++ ∅) = ((𝐴‘𝐾) prefix 𝑄))
167	96, 166	syl 17	. . . . . . 7 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ∅) = ((𝐴‘𝐾) prefix 𝑄))
168	167	oveq1d 7228	. . . . . 6 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ∅) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
169	165, 168, 17	3eqtr4rd 2788	. . . . 5 ⊢ (𝜑 → (𝑆‘𝐶) = ((((𝐴‘𝐾) prefix 𝑄) ++ ∅) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
170	159	eqcomd 2743	. . . . 5 ⊢ (𝜑 → 𝑄 = (♯‘((𝐴‘𝐾) prefix 𝑄)))
171		hash0 13934	. . . . . . 7 ⊢ (♯‘∅) = 0
172	171	oveq2i 7224	. . . . . 6 ⊢ (𝑄 + (♯‘∅)) = (𝑄 + 0)
173	62	addid1d 11032	. . . . . 6 ⊢ (𝜑 → (𝑄 + 0) = 𝑄)
174	172, 173	eqtr2id 2791	. . . . 5 ⊢ (𝜑 → 𝑄 = (𝑄 + (♯‘∅)))
175	96, 98, 36, 102, 169, 170, 174	splval2 14322	. . . 4 ⊢ (𝜑 → ((𝑆‘𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀‘𝑉)”⟩⟩) = ((((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
176		elfzuzb 13106	. . . . . . . . . . . . . 14 ⊢ (𝑄 ∈ (0...(𝑄 + 2)) ↔ (𝑄 ∈ (ℤ_≥‘0) ∧ (𝑄 + 2) ∈ (ℤ_≥‘𝑄)))
177	16, 107, 176	sylanbrc 586	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∈ (0...(𝑄 + 2)))
178		elfzuzb 13106	. . . . . . . . . . . . . 14 ⊢ ((𝑄 + 2) ∈ (0...𝑃) ↔ ((𝑄 + 2) ∈ (ℤ_≥‘0) ∧ 𝑃 ∈ (ℤ_≥‘(𝑄 + 2))))
179	43, 47, 178	sylanbrc 586	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄 + 2) ∈ (0...𝑃))
180		ccatswrd 14233	. . . . . . . . . . . . 13 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) ∧ (𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))))) → (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩))
181	34, 177, 179, 44, 180	syl13anc 1374	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = ((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩))
182	181	oveq1d 7228	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))))
183		swrdcl 14210	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) → ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2_o))
184	34, 183	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2_o))
185		swrdcl 14210	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2_o))
186	34, 185	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2_o))
187		ccatass 14145	. . . . . . . . . . . 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 ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))))
188	184, 186, 142, 187	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))))
189	163	simprd 499	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
190	182, 188, 189	3eqtr3d 2785	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)))) = (⟨“𝑉(𝑀‘𝑉)”⟩ ++ ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩)))
191		ccatcl 14129	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2_o) ∧ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) ∈ Word (𝐼 × 2_o)) → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2_o))
192	186, 142, 191	syl2anc 587	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) ∈ Word (𝐼 × 2_o))
193		swrdlen 14212	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝑄 + 2) − 𝑄))
194	34, 177, 51, 193	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝑄 + 2) − 𝑄))
195		pncan2 11085	. . . . . . . . . . . . . 14 ⊢ ((𝑄 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑄 + 2) − 𝑄) = 2)
196	62, 69, 195	sylancl 589	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑄 + 2) − 𝑄) = 2)
197	194, 196	eqtrd 2777	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = 2)
198		s2len 14454	. . . . . . . . . . . 12 ⊢ (♯‘⟨“𝑉(𝑀‘𝑉)”⟩) = 2
199	197, 198	eqtr4di 2796	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (♯‘⟨“𝑉(𝑀‘𝑉)”⟩))
200		ccatopth 14281	. . . . . . . . . . 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 ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))))
201	184, 192, 102, 146, 199, 200	syl221anc 1383	. . . . . . . . . 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 498	. . . . . . . 8 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀‘𝑉)”⟩)
204	203	oveq2d 7229	. . . . . . 7 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩))
205		ccatpfx 14266	. . . . . . . 8 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾)))) → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝐴‘𝐾) prefix (𝑄 + 2)))
206	34, 177, 51, 205	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝐴‘𝐾) prefix (𝑄 + 2)))
207	204, 206	eqtr3d 2779	. . . . . 6 ⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) = ((𝐴‘𝐾) prefix (𝑄 + 2)))
208	207	oveq1d 7228	. . . . 5 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (((𝐴‘𝐾) prefix (𝑄 + 2)) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))
209		ccatpfx 14266	. . . . . 6 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾))) ∧ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾)))) → (((𝐴‘𝐾) prefix (𝑄 + 2)) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))))
210	34, 51, 57, 209	syl3anc 1373	. . . . 5 ⊢ (𝜑 → (((𝐴‘𝐾) prefix (𝑄 + 2)) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))))
211		pfxid 14249	. . . . . 6 ⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) → ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))) = (𝐴‘𝐾))
212	34, 211	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))) = (𝐴‘𝐾))
213	208, 210, 212	3eqtrd 2781	. . . 4 ⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀‘𝑉)”⟩) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (𝐴‘𝐾))
214	94, 175, 213	3eqtrd 2781	. . 3 ⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = (𝐴‘𝐾))
215	2, 3, 4, 5	efgtf 19112	. . . . . . 7 ⊢ ((𝑆‘𝐶) ∈ 𝑊 → ((𝑇‘(𝑆‘𝐶)) = (𝑎 ∈ (0...(♯‘(𝑆‘𝐶))), 𝑖 ∈ (𝐼 × 2_o) ↦ ((𝑆‘𝐶) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀‘𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆‘𝐶)):((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2_o))⟶𝑊))
216	13, 215	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝑇‘(𝑆‘𝐶)) = (𝑎 ∈ (0...(♯‘(𝑆‘𝐶))), 𝑖 ∈ (𝐼 × 2_o) ↦ ((𝑆‘𝐶) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀‘𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆‘𝐶)):((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2_o))⟶𝑊))
217	216	simprd 499	. . . . 5 ⊢ (𝜑 → (𝑇‘(𝑆‘𝐶)):((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2_o))⟶𝑊)
218	217	ffnd 6546	. . . 4 ⊢ (𝜑 → (𝑇‘(𝑆‘𝐶)) Fn ((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2_o)))
219		fnovrn 7383	. . . 4 ⊢ (((𝑇‘(𝑆‘𝐶)) Fn ((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2_o)) ∧ 𝑄 ∈ (0...(♯‘(𝑆‘𝐶))) ∧ 𝑉 ∈ (𝐼 × 2_o)) → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) ∈ ran (𝑇‘(𝑆‘𝐶)))
220	218, 91, 92, 219	syl3anc 1373	. . 3 ⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) ∈ ran (𝑇‘(𝑆‘𝐶)))
221	214, 220	eqeltrrd 2839	. 2 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶)))
222		uztrn 12456	. . . . . . 7 ⊢ (((𝑃 − 2) ∈ (ℤ_≥‘𝑄) ∧ 𝑄 ∈ (ℤ_≥‘0)) → (𝑃 − 2) ∈ (ℤ_≥‘0))
223	87, 16, 222	syl2anc 587	. . . . . 6 ⊢ (𝜑 → (𝑃 − 2) ∈ (ℤ_≥‘0))
224		elfzuzb 13106	. . . . . 6 ⊢ ((𝑃 − 2) ∈ (0...(♯‘(𝑆‘𝐶))) ↔ ((𝑃 − 2) ∈ (ℤ_≥‘0) ∧ (♯‘(𝑆‘𝐶)) ∈ (ℤ_≥‘(𝑃 − 2))))
225	223, 85, 224	sylanbrc 586	. . . . 5 ⊢ (𝜑 → (𝑃 − 2) ∈ (0...(♯‘(𝑆‘𝐶))))
226	2, 3, 4, 5	efgtval 19113	. . . . 5 ⊢ (((𝑆‘𝐶) ∈ 𝑊 ∧ (𝑃 − 2) ∈ (0...(♯‘(𝑆‘𝐶))) ∧ 𝑈 ∈ (𝐼 × 2_o)) → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = ((𝑆‘𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀‘𝑈)”⟩⟩))
227	13, 225, 117, 226	syl3anc 1373	. . . 4 ⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = ((𝑆‘𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀‘𝑈)”⟩⟩))
228		pfxcl 14242	. . . . . 6 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) → ((𝐵‘𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2_o))
229	30, 228	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐵‘𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2_o))
230		swrdcl 14210	. . . . . 6 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) → ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2_o))
231	30, 230	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2_o))
232		ccatswrd 14233	. . . . . . . . . . 11 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) ∧ ((𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾))))) → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))
233	34, 179, 44, 57, 232	syl13anc 1374	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩))
234	202	simprd 499	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))
235		elfzuzb 13106	. . . . . . . . . . . . . . . 16 ⊢ (𝑄 ∈ (0...(𝑃 − 2)) ↔ (𝑄 ∈ (ℤ_≥‘0) ∧ (𝑃 − 2) ∈ (ℤ_≥‘𝑄)))
236	16, 87, 235	sylanbrc 586	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑄 ∈ (0...(𝑃 − 2)))
237	2, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27, 44, 14, 117, 92, 125, 131	efgredlemg 19132	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) = (♯‘(𝐵‘𝐿)))
238	237, 46	eqeltrrd 2839	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ (ℤ_≥‘𝑃))
239		0le2 11932	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ≤ 2
240	239	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 ≤ 2)
241	74	zred 12282	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑃 ∈ ℝ)
242		2re 11904	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℝ
243		subge02 11348	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃 ∈ ℝ ∧ 2 ∈ ℝ) → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃))
244	241, 242, 243	sylancl 589	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃))
245	240, 244	mpbid 235	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑃 − 2) ≤ 𝑃)
246		eluz2 12444	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ (ℤ_≥‘(𝑃 − 2)) ↔ ((𝑃 − 2) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑃 − 2) ≤ 𝑃))
247	76, 74, 245, 246	syl3anbrc 1345	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ (ℤ_≥‘(𝑃 − 2)))
248		uztrn 12456	. . . . . . . . . . . . . . . . 17 ⊢ (((♯‘(𝐵‘𝐿)) ∈ (ℤ_≥‘𝑃) ∧ 𝑃 ∈ (ℤ_≥‘(𝑃 − 2))) → (♯‘(𝐵‘𝐿)) ∈ (ℤ_≥‘(𝑃 − 2)))
249	238, 247, 248	syl2anc 587	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ (ℤ_≥‘(𝑃 − 2)))
250		elfzuzb 13106	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿))) ↔ ((𝑃 − 2) ∈ (ℤ_≥‘0) ∧ (♯‘(𝐵‘𝐿)) ∈ (ℤ_≥‘(𝑃 − 2))))
251	223, 249, 250	sylanbrc 586	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿))))
252		lencl 14088	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) → (♯‘(𝐵‘𝐿)) ∈ ℕ₀)
253	30, 252	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ ℕ₀)
254	253, 54	eleqtrdi 2848	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ (ℤ_≥‘0))
255		eluzfz2 13120	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘(𝐵‘𝐿)) ∈ (ℤ_≥‘0) → (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))
256	254, 255	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))
257		ccatswrd 14233	. . . . . . . . . . . . . . 15 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) ∧ (𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿))) ∧ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))) → (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))
258	30, 236, 251, 256, 257	syl13anc 1374	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) substr ⟨𝑄, (♯‘(𝐵‘𝐿))⟩))
259	234, 258	eqtr4d 2780	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩))) = (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩)))
260		swrdcl 14210	. . . . . . . . . . . . . . 15 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) → ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2_o))
261	30, 260	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2_o))
262		swrdcl 14210	. . . . . . . . . . . . . . 15 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) → ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2_o))
263	30, 262	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2_o))
264		swrdlen 14212	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2_o) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (𝑃 − (𝑄 + 2)))
265	34, 179, 44, 264	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (𝑃 − (𝑄 + 2)))
266		swrdlen 14212	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝑃 − 2) − 𝑄))
267	30, 236, 251, 266	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝑃 − 2) − 𝑄))
268	78, 62, 70	sub32d 11221	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑃 − 𝑄) − 2) = ((𝑃 − 2) − 𝑄))
269	78, 62, 70	subsub4d 11220	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑃 − 𝑄) − 2) = (𝑃 − (𝑄 + 2)))
270	267, 268, 269	3eqtr2d 2783	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = (𝑃 − (𝑄 + 2)))
271	265, 270	eqtr4d 2780	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (♯‘((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)))
272		ccatopth 14281	. . . . . . . . . . . . . 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), (♯‘(𝐵‘𝐿))⟩))))
273	186, 142, 261, 263, 271, 272	syl221anc 1383	. . . . . . . . . . . . 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 498	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩))
276	274	simprd 499	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩))
277		elfzuzb 13106	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 − 2) ∈ (0...𝑃) ↔ ((𝑃 − 2) ∈ (ℤ_≥‘0) ∧ 𝑃 ∈ (ℤ_≥‘(𝑃 − 2))))
278	223, 247, 277	sylanbrc 586	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 − 2) ∈ (0...𝑃))
279		elfzuz 13108	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) → 𝑃 ∈ (ℤ_≥‘0))
280	44, 279	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ (ℤ_≥‘0))
281		elfzuzb 13106	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ (0...(♯‘(𝐵‘𝐿))) ↔ (𝑃 ∈ (ℤ_≥‘0) ∧ (♯‘(𝐵‘𝐿)) ∈ (ℤ_≥‘𝑃)))
282	280, 238, 281	sylanbrc 586	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ (0...(♯‘(𝐵‘𝐿))))
283		ccatswrd 14233	. . . . . . . . . . . . . . 15 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) ∧ ((𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))) → (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩))
284	30, 278, 282, 256, 283	syl13anc 1374	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵‘𝐿))⟩))
285	276, 284	eqtr4d 2780	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
286		swrdcl 14210	. . . . . . . . . . . . . . 15 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) → ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2_o))
287	30, 286	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2_o))
288		s2len 14454	. . . . . . . . . . . . . . 15 ⊢ (♯‘⟨“𝑈(𝑀‘𝑈)”⟩) = 2
289		swrdlen 14212	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = (𝑃 − (𝑃 − 2)))
290	30, 278, 282, 289	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = (𝑃 − (𝑃 − 2)))
291		nncan 11107	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑃 − (𝑃 − 2)) = 2)
292	78, 69, 291	sylancl 589	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃 − (𝑃 − 2)) = 2)
293	290, 292	eqtr2d 2778	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 = (♯‘((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
294	288, 293	syl5eq 2790	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘⟨“𝑈(𝑀‘𝑈)”⟩) = (♯‘((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
295		ccatopth 14281	. . . . . . . . . . . . . 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 ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))))
296	120, 122, 287, 231, 294, 295	syl221anc 1383	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((⟨“𝑈(𝑀‘𝑈)”⟩ ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) ↔ (⟨“𝑈(𝑀‘𝑈)”⟩ = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) = ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))))
297	285, 296	mpbid 235	. . . . . . . . . . . 12 ⊢ (𝜑 → (⟨“𝑈(𝑀‘𝑈)”⟩ = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) = ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
298	297	simprd 499	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩) = ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))
299	275, 298	oveq12d 7231	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴‘𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴‘𝐾) substr ⟨𝑃, (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
300	233, 299	eqtr3d 2779	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩) = (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
301	300	oveq2d 7229	. . . . . . . 8 ⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))))
302		ccatass 14145	. . . . . . . . 9 ⊢ ((((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2_o) ∧ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2_o) ∧ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩) ∈ Word (𝐼 × 2_o)) → ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))))
303	32, 261, 231, 302	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑄) ++ (((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩))))
304	301, 303	eqtr4d 2780	. . . . . . 7 ⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)) = ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
305		ccatpfx 14266	. . . . . . . . 9 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿)))) → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝐵‘𝐿) prefix (𝑃 − 2)))
306	30, 236, 251, 305	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝐵‘𝐿) prefix (𝑃 − 2)))
307	306	oveq1d 7228	. . . . . . 7 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
308	17, 304, 307	3eqtrd 2781	. . . . . 6 ⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
309		ccatrid 14144	. . . . . . . 8 ⊢ (((𝐵‘𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2_o) → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) = ((𝐵‘𝐿) prefix (𝑃 − 2)))
310	229, 309	syl 17	. . . . . . 7 ⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) = ((𝐵‘𝐿) prefix (𝑃 − 2)))
311	310	oveq1d 7228	. . . . . 6 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
312	308, 311	eqtr4d 2780	. . . . 5 ⊢ (𝜑 → (𝑆‘𝐶) = ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
313		pfxlen 14248	. . . . . . 7 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) prefix (𝑃 − 2))) = (𝑃 − 2))
314	30, 251, 313	syl2anc 587	. . . . . 6 ⊢ (𝜑 → (♯‘((𝐵‘𝐿) prefix (𝑃 − 2))) = (𝑃 − 2))
315	314	eqcomd 2743	. . . . 5 ⊢ (𝜑 → (𝑃 − 2) = (♯‘((𝐵‘𝐿) prefix (𝑃 − 2))))
316	171	oveq2i 7224	. . . . . 6 ⊢ ((𝑃 − 2) + (♯‘∅)) = ((𝑃 − 2) + 0)
317	76	zcnd 12283	. . . . . . 7 ⊢ (𝜑 → (𝑃 − 2) ∈ ℂ)
318	317	addid1d 11032	. . . . . 6 ⊢ (𝜑 → ((𝑃 − 2) + 0) = (𝑃 − 2))
319	316, 318	eqtr2id 2791	. . . . 5 ⊢ (𝜑 → (𝑃 − 2) = ((𝑃 − 2) + (♯‘∅)))
320	229, 98, 231, 120, 312, 315, 319	splval2 14322	. . . 4 ⊢ (𝜑 → ((𝑆‘𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀‘𝑈)”⟩⟩) = ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
321	297	simpld 498	. . . . . . . 8 ⊢ (𝜑 → ⟨“𝑈(𝑀‘𝑈)”⟩ = ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩))
322	321	oveq2d 7229	. . . . . . 7 ⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
323		ccatpfx 14266	. . . . . . . 8 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿)))) → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = ((𝐵‘𝐿) prefix 𝑃))
324	30, 278, 282, 323	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = ((𝐵‘𝐿) prefix 𝑃))
325	322, 324	eqtrd 2777	. . . . . 6 ⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) = ((𝐵‘𝐿) prefix 𝑃))
326	325	oveq1d 7228	. . . . 5 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (((𝐵‘𝐿) prefix 𝑃) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)))
327		ccatpfx 14266	. . . . . 6 ⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿)))) → (((𝐵‘𝐿) prefix 𝑃) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))))
328	30, 282, 256, 327	syl3anc 1373	. . . . 5 ⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑃) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))))
329		pfxid 14249	. . . . . 6 ⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2_o) → ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))) = (𝐵‘𝐿))
330	30, 329	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))) = (𝐵‘𝐿))
331	326, 328, 330	3eqtrd 2781	. . . 4 ⊢ (𝜑 → ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀‘𝑈)”⟩) ++ ((𝐵‘𝐿) substr ⟨𝑃, (♯‘(𝐵‘𝐿))⟩)) = (𝐵‘𝐿))
332	227, 320, 331	3eqtrd 2781	. . 3 ⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = (𝐵‘𝐿))
333		fnovrn 7383	. . . 4 ⊢ (((𝑇‘(𝑆‘𝐶)) Fn ((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2_o)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝑆‘𝐶))) ∧ 𝑈 ∈ (𝐼 × 2_o)) → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) ∈ ran (𝑇‘(𝑆‘𝐶)))
334	218, 225, 117, 333	syl3anc 1373	. . 3 ⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) ∈ ran (𝑇‘(𝑆‘𝐶)))
335	332, 334	eqeltrrd 2839	. 2 ⊢ (𝜑 → (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶)))
336	221, 335	jca 515	1 ⊢ (𝜑 → ((𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶)) ∧ (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1543 ∈ wcel 2110 ∀wral 3061 {crab 3065 ∖ cdif 3863 ∅c0 4237 {csn 4541 ⟨cop 4547 ⟨cotp 4549 ∪ ciun 4904 class class class wbr 5053 ↦ cmpt 5135 I cid 5454 × cxp 5549 dom cdm 5551 ran crn 5552 Fn wfn 6375 ⟶wf 6376 ‘cfv 6380 (class class class)co 7213 ∈ cmpo 7215 1_oc1o 8195 2_oc2o 8196 ℂcc 10727 ℝcr 10728 0cc0 10729 1c1 10730 + caddc 10732 < clt 10867 ≤ cle 10868 − cmin 11062 2c2 11885 ℕ₀cn0 12090 ℤcz 12176 ℤ_≥cuz 12438 ...cfz 13095 ..^cfzo 13238 ♯chash 13896 Word cword 14069 ++ cconcat 14125 substr csubstr 14205 prefix cpfx 14235 splice csplice 14314 ⟨“cs2 14406 ~_FG cefg 19096

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-rep 5179 ax-sep 5192 ax-nul 5199 ax-pow 5258 ax-pr 5322 ax-un 7523 ax-cnex 10785 ax-resscn 10786 ax-1cn 10787 ax-icn 10788 ax-addcl 10789 ax-addrcl 10790 ax-mulcl 10791 ax-mulrcl 10792 ax-mulcom 10793 ax-addass 10794 ax-mulass 10795 ax-distr 10796 ax-i2m1 10797 ax-1ne0 10798 ax-1rid 10799 ax-rnegex 10800 ax-rrecex 10801 ax-cnre 10802 ax-pre-lttri 10803 ax-pre-lttrn 10804 ax-pre-ltadd 10805 ax-pre-mulgt0 10806

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rab 3070 df-v 3410 df-sbc 3695 df-csb 3812 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-pss 3885 df-nul 4238 df-if 4440 df-pw 4515 df-sn 4542 df-pr 4544 df-tp 4546 df-op 4548 df-ot 4550 df-uni 4820 df-int 4860 df-iun 4906 df-br 5054 df-opab 5116 df-mpt 5136 df-tr 5162 df-id 5455 df-eprel 5460 df-po 5468 df-so 5469 df-fr 5509 df-we 5511 df-xp 5557 df-rel 5558 df-cnv 5559 df-co 5560 df-dm 5561 df-rn 5562 df-res 5563 df-ima 5564 df-pred 6160 df-ord 6216 df-on 6217 df-lim 6218 df-suc 6219 df-iota 6338 df-fun 6382 df-fn 6383 df-f 6384 df-f1 6385 df-fo 6386 df-f1o 6387 df-fv 6388 df-riota 7170 df-ov 7216 df-oprab 7217 df-mpo 7218 df-om 7645 df-1st 7761 df-2nd 7762 df-wrecs 8047 df-recs 8108 df-rdg 8146 df-1o 8202 df-2o 8203 df-er 8391 df-map 8510 df-en 8627 df-dom 8628 df-sdom 8629 df-fin 8630 df-card 9555 df-pnf 10869 df-mnf 10870 df-xr 10871 df-ltxr 10872 df-le 10873 df-sub 11064 df-neg 11065 df-nn 11831 df-2 11893 df-n0 12091 df-z 12177 df-uz 12439 df-fz 13096 df-fzo 13239 df-hash 13897 df-word 14070 df-concat 14126 df-s1 14153 df-substr 14206 df-pfx 14236 df-splice 14315 df-s2 14413

This theorem is referenced by: efgredlemd 19134

W3C validator