Theorem efgcpbllemb 19696

Description: Lemma for efgrelex 19692. Show that 𝐿 is an equivalence relation containing all direct extensions of a word, so is closed under ∼. (Contributed by Mario Carneiro, 1-Oct-2015.)

Hypotheses

Ref	Expression
efgval.w	⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))
efgval.r	⊢ ∼ = ( ~FG ‘𝐼)
efgval2.m	⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)
efgval2.t	⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))
efgred.d	⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))
efgred.s	⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))
efgcpbllem.1	⊢ 𝐿 = {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑊 ∧ ((𝐴 ++ 𝑖) ++ 𝐵) ∼ ((𝐴 ++ 𝑗) ++ 𝐵))}

Assertion

Ref	Expression
efgcpbllemb	⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ∼ ⊆ 𝐿)

Distinct variable groups:   𝑖,𝑗,𝐴   𝑦,𝑧   𝑡,𝑛,𝑣,𝑤,𝑦,𝑧   𝑖,𝑚,𝑛,𝑡,𝑣,𝑤,𝑥,𝑀,𝑗   𝑖,𝑘,𝑇,𝑗,𝑚,𝑡,𝑥   𝑦,𝑖,𝑧,𝑊,𝑗   𝑘,𝑛,𝑣,𝑤,𝑦,𝑧,𝑊,𝑚,𝑡,𝑥   ∼ ,𝑖,𝑗,𝑚,𝑡,𝑥,𝑦,𝑧   𝐵,𝑖,𝑗   𝑆,𝑖,𝑗   𝑖,𝐼,𝑗,𝑚,𝑛,𝑡,𝑣,𝑤,𝑥,𝑦,𝑧   𝐷,𝑖,𝑗,𝑚,𝑡

Allowed substitution hints:   𝐴(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝐵(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝐷(𝑥,𝑦,𝑧,𝑤,𝑣,𝑘,𝑛)   ∼ (𝑤,𝑣,𝑘,𝑛)   𝑆(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝑇(𝑦,𝑧,𝑤,𝑣,𝑛)   𝐼(𝑘)   𝐿(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑖,𝑗,𝑘,𝑚,𝑛)   𝑀(𝑦,𝑧,𝑘)

Proof of Theorem efgcpbllemb

Dummy variables 𝑎 𝑏 𝑐 𝑓 𝑔 ℎ 𝑟 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		efgval.w	. . 3 ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))
2		efgval.r	. . 3 ⊢ ∼ = ( ~FG ‘𝐼)
3		efgval2.m	. . 3 ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)
4		efgval2.t	. . 3 ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))
5	1, 2, 3, 4	efgval2 19665	. 2 ⊢ ∼ = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)}
6		efgcpbllem.1	. . . . . . 7 ⊢ 𝐿 = {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑊 ∧ ((𝐴 ++ 𝑖) ++ 𝐵) ∼ ((𝐴 ++ 𝑗) ++ 𝐵))}
7	6	relopabiv 5777	. . . . . 6 ⊢ Rel 𝐿
8	7	a1i 11	. . . . 5 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → Rel 𝐿)
9		efgred.d	. . . . . . . . 9 ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))
10		efgred.s	. . . . . . . . 9 ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))
11	1, 2, 3, 4, 9, 10, 6	efgcpbllema 19695	. . . . . . . 8 ⊢ (𝑓𝐿𝑔 ↔ (𝑓 ∈ 𝑊 ∧ 𝑔 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵)))
12	11	simp2bi 1147	. . . . . . 7 ⊢ (𝑓𝐿𝑔 → 𝑔 ∈ 𝑊)
13	12	adantl 481	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → 𝑔 ∈ 𝑊)
14	11	simp1bi 1146	. . . . . . 7 ⊢ (𝑓𝐿𝑔 → 𝑓 ∈ 𝑊)
15	14	adantl 481	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → 𝑓 ∈ 𝑊)
16	1, 2	efger 19659	. . . . . . . 8 ⊢ ∼ Er 𝑊
17	16	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → ∼ Er 𝑊)
18	11	simp3bi 1148	. . . . . . . 8 ⊢ (𝑓𝐿𝑔 → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵))
19	18	adantl 481	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵))
20	17, 19	ersym 8658	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))
21	1, 2, 3, 4, 9, 10, 6	efgcpbllema 19695	. . . . . 6 ⊢ (𝑔𝐿𝑓 ↔ (𝑔 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
22	13, 15, 20, 21	syl3anbrc 1345	. . . . 5 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → 𝑔𝐿𝑓)
23	14	ad2antrl 729	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → 𝑓 ∈ 𝑊)
24	1, 2, 3, 4, 9, 10, 6	efgcpbllema 19695	. . . . . . . 8 ⊢ (𝑔𝐿ℎ ↔ (𝑔 ∈ 𝑊 ∧ ℎ ∈ 𝑊 ∧ ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵)))
25	24	simp2bi 1147	. . . . . . 7 ⊢ (𝑔𝐿ℎ → ℎ ∈ 𝑊)
26	25	ad2antll 730	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ℎ ∈ 𝑊)
27	16	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ∼ Er 𝑊)
28	18	ad2antrl 729	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵))
29	24	simp3bi 1148	. . . . . . . 8 ⊢ (𝑔𝐿ℎ → ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵))
30	29	ad2antll 730	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵))
31	27, 28, 30	ertrd 8662	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵))
32	1, 2, 3, 4, 9, 10, 6	efgcpbllema 19695	. . . . . 6 ⊢ (𝑓𝐿ℎ ↔ (𝑓 ∈ 𝑊 ∧ ℎ ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵)))
33	23, 26, 31, 32	syl3anbrc 1345	. . . . 5 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → 𝑓𝐿ℎ)
34	16	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ∼ Er 𝑊)
35		fviss 6919	. . . . . . . . . . . . . 14 ⊢ ( I ‘Word (𝐼 × 2o)) ⊆ Word (𝐼 × 2o)
36	1, 35	eqsstri 3982	. . . . . . . . . . . . 13 ⊢ 𝑊 ⊆ Word (𝐼 × 2o)
37		simpll 767	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐴 ∈ 𝑊)
38	36, 37	sselid 3933	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐴 ∈ Word (𝐼 × 2o))
39		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝑓 ∈ 𝑊)
40	36, 39	sselid 3933	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝑓 ∈ Word (𝐼 × 2o))
41		ccatcl 14509	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ 𝑓 ∈ Word (𝐼 × 2o)) → (𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o))
42	38, 40, 41	syl2anc 585	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o))
43		simplr 769	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐵 ∈ 𝑊)
44	36, 43	sselid 3933	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐵 ∈ Word (𝐼 × 2o))
45		ccatcl 14509	. . . . . . . . . . 11 ⊢ (((𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ Word (𝐼 × 2o))
46	42, 44, 45	syl2anc 585	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ Word (𝐼 × 2o))
47	1	efgrcl 19656	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o)))
48	47	simprd 495	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑊 → 𝑊 = Word (𝐼 × 2o))
49	48	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝑊 = Word (𝐼 × 2o))
50	46, 49	eleqtrrd 2840	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊)
51	34, 50	erref 8666	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))
52	51	ex 412	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝑓 ∈ 𝑊 → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
53	52	pm4.71d 561	. . . . . 6 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝑓 ∈ 𝑊 ↔ (𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))))
54	1, 2, 3, 4, 9, 10, 6	efgcpbllema 19695	. . . . . . 7 ⊢ (𝑓𝐿𝑓 ↔ (𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
55		df-3an 1089	. . . . . . 7 ⊢ ((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)) ↔ ((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊) ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
56		anidm 564	. . . . . . . 8 ⊢ ((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊) ↔ 𝑓 ∈ 𝑊)
57	56	anbi1i 625	. . . . . . 7 ⊢ (((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊) ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)) ↔ (𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
58	54, 55, 57	3bitri 297	. . . . . 6 ⊢ (𝑓𝐿𝑓 ↔ (𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
59	53, 58	bitr4di 289	. . . . 5 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝑓 ∈ 𝑊 ↔ 𝑓𝐿𝑓))
60	8, 22, 33, 59	iserd 8672	. . . 4 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐿 Er 𝑊)
61	1, 2, 3, 4	efgtf 19663	. . . . . . . . . 10 ⊢ (𝑓 ∈ 𝑊 → ((𝑇‘𝑓) = (𝑎 ∈ (0...(♯‘𝑓)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑓 splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀‘𝑏)”⟩⟩)) ∧ (𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊))
62	61	simprd 495	. . . . . . . . 9 ⊢ (𝑓 ∈ 𝑊 → (𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊)
63	62	adantl 481	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊)
64		ffn 6670	. . . . . . . 8 ⊢ ((𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊 → (𝑇‘𝑓) Fn ((0...(♯‘𝑓)) × (𝐼 × 2o)))
65		ovelrn 7544	. . . . . . . 8 ⊢ ((𝑇‘𝑓) Fn ((0...(♯‘𝑓)) × (𝐼 × 2o)) → (𝑎 ∈ ran (𝑇‘𝑓) ↔ ∃𝑐 ∈ (0...(♯‘𝑓))∃𝑢 ∈ (𝐼 × 2o)𝑎 = (𝑐(𝑇‘𝑓)𝑢)))
66	63, 64, 65	3syl 18	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝑎 ∈ ran (𝑇‘𝑓) ↔ ∃𝑐 ∈ (0...(♯‘𝑓))∃𝑢 ∈ (𝐼 × 2o)𝑎 = (𝑐(𝑇‘𝑓)𝑢)))
67		simplr 769	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑓 ∈ 𝑊)
68	62	ad2antlr 728	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊)
69		simprl 771	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑐 ∈ (0...(♯‘𝑓)))
70		simprr 773	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑢 ∈ (𝐼 × 2o))
71	68, 69, 70	fovcdmd 7540	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐(𝑇‘𝑓)𝑢) ∈ 𝑊)
72	50	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊)
73	37	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝐴 ∈ 𝑊)
74	36, 73	sselid 3933	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝐴 ∈ Word (𝐼 × 2o))
75	40	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑓 ∈ Word (𝐼 × 2o))
76		pfxcl 14613	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ Word (𝐼 × 2o) → (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o))
77	75, 76	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o))
78		ccatcl 14509	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o)) → (𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o))
79	74, 77, 78	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o))
80	3	efgmf 19654	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑀:(𝐼 × 2o)⟶(𝐼 × 2o)
81	80	ffvelcdmi 7037	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ (𝐼 × 2o) → (𝑀‘𝑢) ∈ (𝐼 × 2o))
82	81	ad2antll 730	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑀‘𝑢) ∈ (𝐼 × 2o))
83	70, 82	s2cld 14806	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ⟨“𝑢(𝑀‘𝑢)”⟩ ∈ Word (𝐼 × 2o))
84		ccatcl 14509	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑢(𝑀‘𝑢)”⟩ ∈ Word (𝐼 × 2o)) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o))
85	79, 83, 84	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o))
86		swrdcl 14581	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ Word (𝐼 × 2o) → (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o))
87	75, 86	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o))
88	44	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝐵 ∈ Word (𝐼 × 2o))
89		ccatass 14524	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o) ∧ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
90	85, 87, 88, 89	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
91		ccatcl 14509	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑢(𝑀‘𝑢)”⟩ ∈ Word (𝐼 × 2o)) → ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o))
92	77, 83, 91	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o))
93		ccatass 14524	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o) ∧ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o)) → ((𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
94	74, 92, 87, 93	syl3anc 1374	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
95		ccatass 14524	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑢(𝑀‘𝑢)”⟩ ∈ Word (𝐼 × 2o)) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩)))
96	74, 77, 83, 95	syl3anc 1374	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩)))
97	96	oveq1d 7383	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = ((𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
98	1, 2, 3, 4	efgtval 19664	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ 𝑊 ∧ 𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o)) → (𝑐(𝑇‘𝑓)𝑢) = (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀‘𝑢)”⟩⟩))
99	67, 69, 70, 98	syl3anc 1374	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐(𝑇‘𝑓)𝑢) = (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀‘𝑢)”⟩⟩))
100		splval 14686	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ 𝑊 ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑐 ∈ (0...(♯‘𝑓)) ∧ ⟨“𝑢(𝑀‘𝑢)”⟩ ∈ Word (𝐼 × 2o))) → (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀‘𝑢)”⟩⟩) = (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
101	67, 69, 69, 83, 100	syl13anc 1375	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀‘𝑢)”⟩⟩) = (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
102	99, 101	eqtrd 2772	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐(𝑇‘𝑓)𝑢) = (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
103	102	oveq2d 7384	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) = (𝐴 ++ (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
104	94, 97, 103	3eqtr4rd 2783	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
105	104	oveq1d 7383	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) = ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵))
106		lencl 14468	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ Word (𝐼 × 2o) → (♯‘𝐴) ∈ ℕ0)
107	74, 106	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐴) ∈ ℕ0)
108		nn0uz 12801	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ0 = (ℤ≥‘0)
109	107, 108	eleqtrdi 2847	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐴) ∈ (ℤ≥‘0))
110		elfznn0 13548	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ (0...(♯‘𝑓)) → 𝑐 ∈ ℕ0)
111	110	ad2antrl 729	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑐 ∈ ℕ0)
112		uzaddcl 12829	. . . . . . . . . . . . . . . . 17 ⊢ (((♯‘𝐴) ∈ (ℤ≥‘0) ∧ 𝑐 ∈ ℕ0) → ((♯‘𝐴) + 𝑐) ∈ (ℤ≥‘0))
113	109, 111, 112	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) ∈ (ℤ≥‘0))
114	42	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o))
115		ccatlen 14510	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → (♯‘((𝐴 ++ 𝑓) ++ 𝐵)) = ((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵)))
116	114, 88, 115	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘((𝐴 ++ 𝑓) ++ 𝐵)) = ((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵)))
117		ccatlen 14510	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ 𝑓 ∈ Word (𝐼 × 2o)) → (♯‘(𝐴 ++ 𝑓)) = ((♯‘𝐴) + (♯‘𝑓)))
118	74, 75, 117	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘(𝐴 ++ 𝑓)) = ((♯‘𝐴) + (♯‘𝑓)))
119		elfzuz3 13449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 ∈ (0...(♯‘𝑓)) → (♯‘𝑓) ∈ (ℤ≥‘𝑐))
120	119	ad2antrl 729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ (ℤ≥‘𝑐))
121	107	nn0zd 12525	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐴) ∈ ℤ)
122		eluzadd 12792	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((♯‘𝑓) ∈ (ℤ≥‘𝑐) ∧ (♯‘𝐴) ∈ ℤ) → ((♯‘𝑓) + (♯‘𝐴)) ∈ (ℤ≥‘(𝑐 + (♯‘𝐴))))
123	120, 121, 122	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝑓) + (♯‘𝐴)) ∈ (ℤ≥‘(𝑐 + (♯‘𝐴))))
124		lencl 14468	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∈ Word (𝐼 × 2o) → (♯‘𝑓) ∈ ℕ0)
125	75, 124	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ ℕ0)
126	125	nn0cnd 12476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ ℂ)
127	107	nn0cnd 12476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐴) ∈ ℂ)
128	126, 127	addcomd 11347	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝑓) + (♯‘𝐴)) = ((♯‘𝐴) + (♯‘𝑓)))
129	111	nn0cnd 12476	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑐 ∈ ℂ)
130	129, 127	addcomd 11347	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐 + (♯‘𝐴)) = ((♯‘𝐴) + 𝑐))
131	130	fveq2d 6846	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (ℤ≥‘(𝑐 + (♯‘𝐴))) = (ℤ≥‘((♯‘𝐴) + 𝑐)))
132	123, 128, 131	3eltr3d 2851	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + (♯‘𝑓)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)))
133	118, 132	eqeltrd 2837	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘(𝐴 ++ 𝑓)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)))
134		lencl 14468	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ Word (𝐼 × 2o) → (♯‘𝐵) ∈ ℕ0)
135	88, 134	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐵) ∈ ℕ0)
136		uzaddcl 12829	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘(𝐴 ++ 𝑓)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)) ∧ (♯‘𝐵) ∈ ℕ0) → ((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)))
137	133, 135, 136	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)))
138	116, 137	eqeltrd 2837	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘((𝐴 ++ 𝑓) ++ 𝐵)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)))
139		elfzuzb 13446	. . . . . . . . . . . . . . . 16 ⊢ (((♯‘𝐴) + 𝑐) ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) ↔ (((♯‘𝐴) + 𝑐) ∈ (ℤ≥‘0) ∧ (♯‘((𝐴 ++ 𝑓) ++ 𝐵)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐))))
140	113, 138, 139	sylanbrc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))))
141	1, 2, 3, 4	efgtval 19664	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 ∧ ((♯‘𝐴) + 𝑐) ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) ∧ 𝑢 ∈ (𝐼 × 2o)) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨((♯‘𝐴) + 𝑐), ((♯‘𝐴) + 𝑐), ⟨“𝑢(𝑀‘𝑢)”⟩⟩))
142	72, 140, 70, 141	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨((♯‘𝐴) + 𝑐), ((♯‘𝐴) + 𝑐), ⟨“𝑢(𝑀‘𝑢)”⟩⟩))
143		wrd0 14474	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ Word (𝐼 × 2o)
144	143	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ∅ ∈ Word (𝐼 × 2o))
145		ccatcl 14509	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵) ∈ Word (𝐼 × 2o))
146	87, 88, 145	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵) ∈ Word (𝐼 × 2o))
147		ccatrid 14523	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) = (𝐴 ++ (𝑓 prefix 𝑐)))
148	79, 147	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) = (𝐴 ++ (𝑓 prefix 𝑐)))
149	148	oveq1d 7383	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)) = ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
150		ccatass 14524	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o) ∧ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
151	79, 87, 88, 150	syl3anc 1374	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
152		ccatass 14524	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o) ∧ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o)) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
153	74, 77, 87, 152	syl3anc 1374	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
154	125, 108	eleqtrdi 2847	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ (ℤ≥‘0))
155		eluzfz2 13460	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝑓) ∈ (ℤ≥‘0) → (♯‘𝑓) ∈ (0...(♯‘𝑓)))
156	154, 155	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ (0...(♯‘𝑓)))
157		ccatpfx 14636	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 ∈ Word (𝐼 × 2o) ∧ 𝑐 ∈ (0...(♯‘𝑓)) ∧ (♯‘𝑓) ∈ (0...(♯‘𝑓))) → ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝑓 prefix (♯‘𝑓)))
158	75, 69, 156, 157	syl3anc 1374	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝑓 prefix (♯‘𝑓)))
159		pfxid 14620	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ Word (𝐼 × 2o) → (𝑓 prefix (♯‘𝑓)) = 𝑓)
160	75, 159	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑓 prefix (♯‘𝑓)) = 𝑓)
161	158, 160	eqtrd 2772	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = 𝑓)
162	161	oveq2d 7384	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))) = (𝐴 ++ 𝑓))
163	153, 162	eqtrd 2772	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ 𝑓))
164	163	oveq1d 7383	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = ((𝐴 ++ 𝑓) ++ 𝐵))
165	149, 151, 164	3eqtr2rd 2779	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ 𝑓) ++ 𝐵) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
166		ccatlen 14510	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o)) → (♯‘(𝐴 ++ (𝑓 prefix 𝑐))) = ((♯‘𝐴) + (♯‘(𝑓 prefix 𝑐))))
167	74, 77, 166	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘(𝐴 ++ (𝑓 prefix 𝑐))) = ((♯‘𝐴) + (♯‘(𝑓 prefix 𝑐))))
168		pfxlen 14619	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ Word (𝐼 × 2o) ∧ 𝑐 ∈ (0...(♯‘𝑓))) → (♯‘(𝑓 prefix 𝑐)) = 𝑐)
169	75, 69, 168	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘(𝑓 prefix 𝑐)) = 𝑐)
170	169	oveq2d 7384	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + (♯‘(𝑓 prefix 𝑐))) = ((♯‘𝐴) + 𝑐))
171	167, 170	eqtr2d 2773	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) = (♯‘(𝐴 ++ (𝑓 prefix 𝑐))))
172		hash0 14302	. . . . . . . . . . . . . . . . 17 ⊢ (♯‘∅) = 0
173	172	oveq2i 7379	. . . . . . . . . . . . . . . 16 ⊢ (((♯‘𝐴) + 𝑐) + (♯‘∅)) = (((♯‘𝐴) + 𝑐) + 0)
174	107, 111	nn0addcld 12478	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) ∈ ℕ0)
175	174	nn0cnd 12476	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) ∈ ℂ)
176	175	addridd 11345	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((♯‘𝐴) + 𝑐) + 0) = ((♯‘𝐴) + 𝑐))
177	173, 176	eqtr2id 2785	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) = (((♯‘𝐴) + 𝑐) + (♯‘∅)))
178	79, 144, 146, 83, 165, 171, 177	splval2 14692	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨((♯‘𝐴) + 𝑐), ((♯‘𝐴) + 𝑐), ⟨“𝑢(𝑀‘𝑢)”⟩⟩) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
179	142, 178	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
180	90, 105, 179	3eqtr4d 2782	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) = (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢))
181	1, 2, 3, 4	efgtf 19663	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 → ((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) = (𝑎 ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))), 𝑏 ∈ (𝐼 × 2o) ↦ (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀‘𝑏)”⟩⟩)) ∧ (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o))⟶𝑊))
182	181	simprd 495	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o))⟶𝑊)
183		ffn 6670	. . . . . . . . . . . . . 14 ⊢ ((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o))⟶𝑊 → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o)))
184	72, 182, 183	3syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o)))
185		fnovrn 7543	. . . . . . . . . . . . 13 ⊢ (((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o)) ∧ ((♯‘𝐴) + 𝑐) ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) ∧ 𝑢 ∈ (𝐼 × 2o)) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)))
186	184, 140, 70, 185	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)))
187	180, 186	eqeltrd 2837	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)))
188	1, 2, 3, 4	efgi2 19666	. . . . . . . . . . 11 ⊢ ((((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 ∧ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵))
189	72, 187, 188	syl2anc 585	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵))
190	1, 2, 3, 4, 9, 10, 6	efgcpbllema 19695	. . . . . . . . . 10 ⊢ (𝑓𝐿(𝑐(𝑇‘𝑓)𝑢) ↔ (𝑓 ∈ 𝑊 ∧ (𝑐(𝑇‘𝑓)𝑢) ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵)))
191	67, 71, 189, 190	syl3anbrc 1345	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑓𝐿(𝑐(𝑇‘𝑓)𝑢))
192		vex 3446	. . . . . . . . . . 11 ⊢ 𝑎 ∈ V
193		vex 3446	. . . . . . . . . . 11 ⊢ 𝑓 ∈ V
194	192, 193	elec 8692	. . . . . . . . . 10 ⊢ (𝑎 ∈ [𝑓]𝐿 ↔ 𝑓𝐿𝑎)
195		breq2 5104	. . . . . . . . . 10 ⊢ (𝑎 = (𝑐(𝑇‘𝑓)𝑢) → (𝑓𝐿𝑎 ↔ 𝑓𝐿(𝑐(𝑇‘𝑓)𝑢)))
196	194, 195	bitrid 283	. . . . . . . . 9 ⊢ (𝑎 = (𝑐(𝑇‘𝑓)𝑢) → (𝑎 ∈ [𝑓]𝐿 ↔ 𝑓𝐿(𝑐(𝑇‘𝑓)𝑢)))
197	191, 196	syl5ibrcom 247	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑎 = (𝑐(𝑇‘𝑓)𝑢) → 𝑎 ∈ [𝑓]𝐿))
198	197	rexlimdvva 3195	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (∃𝑐 ∈ (0...(♯‘𝑓))∃𝑢 ∈ (𝐼 × 2o)𝑎 = (𝑐(𝑇‘𝑓)𝑢) → 𝑎 ∈ [𝑓]𝐿))
199	66, 198	sylbid 240	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝑎 ∈ ran (𝑇‘𝑓) → 𝑎 ∈ [𝑓]𝐿))
200	199	ssrdv 3941	. . . . 5 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)
201	200	ralrimiva 3130	. . . 4 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)
202	1	fvexi 6856	. . . . . 6 ⊢ 𝑊 ∈ V
203		erex 8670	. . . . . 6 ⊢ (𝐿 Er 𝑊 → (𝑊 ∈ V → 𝐿 ∈ V))
204	60, 202, 203	mpisyl 21	. . . . 5 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐿 ∈ V)
205		ereq1 8653	. . . . . . 7 ⊢ (𝑟 = 𝐿 → (𝑟 Er 𝑊 ↔ 𝐿 Er 𝑊))
206		eceq2 8687	. . . . . . . . 9 ⊢ (𝑟 = 𝐿 → [𝑓]𝑟 = [𝑓]𝐿)
207	206	sseq2d 3968	. . . . . . . 8 ⊢ (𝑟 = 𝐿 → (ran (𝑇‘𝑓) ⊆ [𝑓]𝑟 ↔ ran (𝑇‘𝑓) ⊆ [𝑓]𝐿))
208	207	ralbidv 3161	. . . . . . 7 ⊢ (𝑟 = 𝐿 → (∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟 ↔ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿))
209	205, 208	anbi12d 633	. . . . . 6 ⊢ (𝑟 = 𝐿 → ((𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟) ↔ (𝐿 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)))
210	209	elabg 3633	. . . . 5 ⊢ (𝐿 ∈ V → (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ↔ (𝐿 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)))
211	204, 210	syl 17	. . . 4 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ↔ (𝐿 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)))
212	60, 201, 211	mpbir2and 714	. . 3 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)})
213		intss1 4920	. . 3 ⊢ (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} → ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ⊆ 𝐿)
214	212, 213	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ⊆ 𝐿)
215	5, 214	eqsstrid 3974	1 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ∼ ⊆ 𝐿)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  {cab 2715  ∀wral 3052  ∃wrex 3062  {crab 3401  Vcvv 3442   ∖ cdif 3900   ⊆ wss 3903  ∅c0 4287  {csn 4582  {cpr 4584  ⟨cop 4588  ⟨cotp 4590  ∩ cint 4904  ∪ ciun 4948   class class class wbr 5100  {copab 5162   ↦ cmpt 5181   I cid 5526   × cxp 5630  ran crn 5633  Rel wrel 5637   Fn wfn 6495  ⟶wf 6496  ‘cfv 6500  (class class class)co 7368   ∈ cmpo 7370  1_oc1o 8400  2_oc2o 8401   Er wer 8642  [cec 8643  0cc0 11038  1c1 11039   + caddc 11041   − cmin 11376  ℕ₀cn0 12413  ℤcz 12500  ℤ_≥cuz 12763  ...cfz 13435  ..^cfzo 13582  ♯chash 14265  Word cword 14448   ++ cconcat 14505   substr csubstr 14576   prefix cpfx 14606   splice csplice 14684  ⟨“cs2 14776   ~_FG cefg 19647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-ot 4591  df-uni 4866  df-int 4905  df-iun 4950  df-iin 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-om 7819  df-1st 7943  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-1o 8407  df-2o 8408  df-er 8645  df-ec 8647  df-map 8777  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-card 9863  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-nn 12158  df-n0 12414  df-z 12501  df-uz 12764  df-fz 13436  df-fzo 13583  df-hash 14266  df-word 14449  df-concat 14506  df-s1 14532  df-substr 14577  df-pfx 14607  df-splice 14685  df-s2 14783  df-efg 19650

This theorem is referenced by:  efgcpbl  19697