Theorem efgcpbllemb 19617

Description: Lemma for efgrelex 19613. 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 19586	. 2 ⊢ ∼ = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)}
6		efgcpbllem.1	. . . . . . 7 ⊢ 𝐿 = {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑊 ∧ ((𝐴 ++ 𝑖) ++ 𝐵) ∼ ((𝐴 ++ 𝑗) ++ 𝐵))}
7	6	relopabiv 5818	. . . . . 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 19616	. . . . . . . 8 ⊢ (𝑓𝐿𝑔 ↔ (𝑓 ∈ 𝑊 ∧ 𝑔 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵)))
12	11	simp2bi 1146	. . . . . . 7 ⊢ (𝑓𝐿𝑔 → 𝑔 ∈ 𝑊)
13	12	adantl 482	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → 𝑔 ∈ 𝑊)
14	11	simp1bi 1145	. . . . . . 7 ⊢ (𝑓𝐿𝑔 → 𝑓 ∈ 𝑊)
15	14	adantl 482	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → 𝑓 ∈ 𝑊)
16	1, 2	efger 19580	. . . . . . . 8 ⊢ ∼ Er 𝑊
17	16	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → ∼ Er 𝑊)
18	11	simp3bi 1147	. . . . . . . 8 ⊢ (𝑓𝐿𝑔 → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵))
19	18	adantl 482	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵))
20	17, 19	ersym 8711	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))
21	1, 2, 3, 4, 9, 10, 6	efgcpbllema 19616	. . . . . 6 ⊢ (𝑔𝐿𝑓 ↔ (𝑔 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
22	13, 15, 20, 21	syl3anbrc 1343	. . . . 5 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → 𝑔𝐿𝑓)
23	14	ad2antrl 726	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → 𝑓 ∈ 𝑊)
24	1, 2, 3, 4, 9, 10, 6	efgcpbllema 19616	. . . . . . . 8 ⊢ (𝑔𝐿ℎ ↔ (𝑔 ∈ 𝑊 ∧ ℎ ∈ 𝑊 ∧ ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵)))
25	24	simp2bi 1146	. . . . . . 7 ⊢ (𝑔𝐿ℎ → ℎ ∈ 𝑊)
26	25	ad2antll 727	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ℎ ∈ 𝑊)
27	16	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ∼ Er 𝑊)
28	18	ad2antrl 726	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵))
29	24	simp3bi 1147	. . . . . . . 8 ⊢ (𝑔𝐿ℎ → ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵))
30	29	ad2antll 727	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵))
31	27, 28, 30	ertrd 8715	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵))
32	1, 2, 3, 4, 9, 10, 6	efgcpbllema 19616	. . . . . 6 ⊢ (𝑓𝐿ℎ ↔ (𝑓 ∈ 𝑊 ∧ ℎ ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵)))
33	23, 26, 31, 32	syl3anbrc 1343	. . . . 5 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → 𝑓𝐿ℎ)
34	16	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ∼ Er 𝑊)
35		fviss 6965	. . . . . . . . . . . . . 14 ⊢ ( I ‘Word (𝐼 × 2o)) ⊆ Word (𝐼 × 2o)
36	1, 35	eqsstri 4015	. . . . . . . . . . . . 13 ⊢ 𝑊 ⊆ Word (𝐼 × 2o)
37		simpll 765	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐴 ∈ 𝑊)
38	36, 37	sselid 3979	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐴 ∈ Word (𝐼 × 2o))
39		simpr 485	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝑓 ∈ 𝑊)
40	36, 39	sselid 3979	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝑓 ∈ Word (𝐼 × 2o))
41		ccatcl 14520	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ 𝑓 ∈ Word (𝐼 × 2o)) → (𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o))
42	38, 40, 41	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o))
43		simplr 767	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐵 ∈ 𝑊)
44	36, 43	sselid 3979	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐵 ∈ Word (𝐼 × 2o))
45		ccatcl 14520	. . . . . . . . . . 11 ⊢ (((𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ Word (𝐼 × 2o))
46	42, 44, 45	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ Word (𝐼 × 2o))
47	1	efgrcl 19577	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o)))
48	47	simprd 496	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑊 → 𝑊 = Word (𝐼 × 2o))
49	48	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝑊 = Word (𝐼 × 2o))
50	46, 49	eleqtrrd 2836	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊)
51	34, 50	erref 8719	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))
52	51	ex 413	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝑓 ∈ 𝑊 → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
53	52	pm4.71d 562	. . . . . 6 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝑓 ∈ 𝑊 ↔ (𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))))
54	1, 2, 3, 4, 9, 10, 6	efgcpbllema 19616	. . . . . . 7 ⊢ (𝑓𝐿𝑓 ↔ (𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
55		df-3an 1089	. . . . . . 7 ⊢ ((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)) ↔ ((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊) ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
56		anidm 565	. . . . . . . 8 ⊢ ((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊) ↔ 𝑓 ∈ 𝑊)
57	56	anbi1i 624	. . . . . . 7 ⊢ (((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊) ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)) ↔ (𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
58	54, 55, 57	3bitri 296	. . . . . 6 ⊢ (𝑓𝐿𝑓 ↔ (𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
59	53, 58	bitr4di 288	. . . . 5 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝑓 ∈ 𝑊 ↔ 𝑓𝐿𝑓))
60	8, 22, 33, 59	iserd 8725	. . . 4 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐿 Er 𝑊)
61	1, 2, 3, 4	efgtf 19584	. . . . . . . . . 10 ⊢ (𝑓 ∈ 𝑊 → ((𝑇‘𝑓) = (𝑎 ∈ (0...(♯‘𝑓)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑓 splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀‘𝑏)”⟩⟩)) ∧ (𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊))
62	61	simprd 496	. . . . . . . . 9 ⊢ (𝑓 ∈ 𝑊 → (𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊)
63	62	adantl 482	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊)
64		ffn 6714	. . . . . . . 8 ⊢ ((𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊 → (𝑇‘𝑓) Fn ((0...(♯‘𝑓)) × (𝐼 × 2o)))
65		ovelrn 7579	. . . . . . . 8 ⊢ ((𝑇‘𝑓) Fn ((0...(♯‘𝑓)) × (𝐼 × 2o)) → (𝑎 ∈ ran (𝑇‘𝑓) ↔ ∃𝑐 ∈ (0...(♯‘𝑓))∃𝑢 ∈ (𝐼 × 2o)𝑎 = (𝑐(𝑇‘𝑓)𝑢)))
66	63, 64, 65	3syl 18	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝑎 ∈ ran (𝑇‘𝑓) ↔ ∃𝑐 ∈ (0...(♯‘𝑓))∃𝑢 ∈ (𝐼 × 2o)𝑎 = (𝑐(𝑇‘𝑓)𝑢)))
67		simplr 767	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑓 ∈ 𝑊)
68	62	ad2antlr 725	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊)
69		simprl 769	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑐 ∈ (0...(♯‘𝑓)))
70		simprr 771	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑢 ∈ (𝐼 × 2o))
71	68, 69, 70	fovcdmd 7575	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐(𝑇‘𝑓)𝑢) ∈ 𝑊)
72	50	adantr 481	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊)
73	37	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝐴 ∈ 𝑊)
74	36, 73	sselid 3979	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝐴 ∈ Word (𝐼 × 2o))
75	40	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑓 ∈ Word (𝐼 × 2o))
76		pfxcl 14623	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ Word (𝐼 × 2o) → (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o))
77	75, 76	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o))
78		ccatcl 14520	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o)) → (𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o))
79	74, 77, 78	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o))
80	3	efgmf 19575	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑀:(𝐼 × 2o)⟶(𝐼 × 2o)
81	80	ffvelcdmi 7082	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ (𝐼 × 2o) → (𝑀‘𝑢) ∈ (𝐼 × 2o))
82	81	ad2antll 727	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑀‘𝑢) ∈ (𝐼 × 2o))
83	70, 82	s2cld 14818	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ⟨“𝑢(𝑀‘𝑢)”⟩ ∈ Word (𝐼 × 2o))
84		ccatcl 14520	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑢(𝑀‘𝑢)”⟩ ∈ Word (𝐼 × 2o)) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o))
85	79, 83, 84	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o))
86		swrdcl 14591	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ Word (𝐼 × 2o) → (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o))
87	75, 86	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o))
88	44	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝐵 ∈ Word (𝐼 × 2o))
89		ccatass 14534	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o) ∧ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
90	85, 87, 88, 89	syl3anc 1371	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
91		ccatcl 14520	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑢(𝑀‘𝑢)”⟩ ∈ Word (𝐼 × 2o)) → ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o))
92	77, 83, 91	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o))
93		ccatass 14534	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o) ∧ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o)) → ((𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
94	74, 92, 87, 93	syl3anc 1371	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
95		ccatass 14534	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑢(𝑀‘𝑢)”⟩ ∈ Word (𝐼 × 2o)) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩)))
96	74, 77, 83, 95	syl3anc 1371	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩)))
97	96	oveq1d 7420	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = ((𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
98	1, 2, 3, 4	efgtval 19585	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ 𝑊 ∧ 𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o)) → (𝑐(𝑇‘𝑓)𝑢) = (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀‘𝑢)”⟩⟩))
99	67, 69, 70, 98	syl3anc 1371	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐(𝑇‘𝑓)𝑢) = (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀‘𝑢)”⟩⟩))
100		splval 14697	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ 𝑊 ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑐 ∈ (0...(♯‘𝑓)) ∧ ⟨“𝑢(𝑀‘𝑢)”⟩ ∈ Word (𝐼 × 2o))) → (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀‘𝑢)”⟩⟩) = (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
101	67, 69, 69, 83, 100	syl13anc 1372	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀‘𝑢)”⟩⟩) = (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
102	99, 101	eqtrd 2772	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐(𝑇‘𝑓)𝑢) = (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
103	102	oveq2d 7421	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) = (𝐴 ++ (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
104	94, 97, 103	3eqtr4rd 2783	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
105	104	oveq1d 7420	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) = ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵))
106		lencl 14479	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ Word (𝐼 × 2o) → (♯‘𝐴) ∈ ℕ0)
107	74, 106	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐴) ∈ ℕ0)
108		nn0uz 12860	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ0 = (ℤ≥‘0)
109	107, 108	eleqtrdi 2843	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐴) ∈ (ℤ≥‘0))
110		elfznn0 13590	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ (0...(♯‘𝑓)) → 𝑐 ∈ ℕ0)
111	110	ad2antrl 726	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑐 ∈ ℕ0)
112		uzaddcl 12884	. . . . . . . . . . . . . . . . 17 ⊢ (((♯‘𝐴) ∈ (ℤ≥‘0) ∧ 𝑐 ∈ ℕ0) → ((♯‘𝐴) + 𝑐) ∈ (ℤ≥‘0))
113	109, 111, 112	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) ∈ (ℤ≥‘0))
114	42	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o))
115		ccatlen 14521	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → (♯‘((𝐴 ++ 𝑓) ++ 𝐵)) = ((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵)))
116	114, 88, 115	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘((𝐴 ++ 𝑓) ++ 𝐵)) = ((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵)))
117		ccatlen 14521	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ 𝑓 ∈ Word (𝐼 × 2o)) → (♯‘(𝐴 ++ 𝑓)) = ((♯‘𝐴) + (♯‘𝑓)))
118	74, 75, 117	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘(𝐴 ++ 𝑓)) = ((♯‘𝐴) + (♯‘𝑓)))
119		elfzuz3 13494	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 ∈ (0...(♯‘𝑓)) → (♯‘𝑓) ∈ (ℤ≥‘𝑐))
120	119	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ (ℤ≥‘𝑐))
121	107	nn0zd 12580	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐴) ∈ ℤ)
122		eluzadd 12847	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((♯‘𝑓) ∈ (ℤ≥‘𝑐) ∧ (♯‘𝐴) ∈ ℤ) → ((♯‘𝑓) + (♯‘𝐴)) ∈ (ℤ≥‘(𝑐 + (♯‘𝐴))))
123	120, 121, 122	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝑓) + (♯‘𝐴)) ∈ (ℤ≥‘(𝑐 + (♯‘𝐴))))
124		lencl 14479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∈ Word (𝐼 × 2o) → (♯‘𝑓) ∈ ℕ0)
125	75, 124	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ ℕ0)
126	125	nn0cnd 12530	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ ℂ)
127	107	nn0cnd 12530	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐴) ∈ ℂ)
128	126, 127	addcomd 11412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝑓) + (♯‘𝐴)) = ((♯‘𝐴) + (♯‘𝑓)))
129	111	nn0cnd 12530	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑐 ∈ ℂ)
130	129, 127	addcomd 11412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐 + (♯‘𝐴)) = ((♯‘𝐴) + 𝑐))
131	130	fveq2d 6892	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (ℤ≥‘(𝑐 + (♯‘𝐴))) = (ℤ≥‘((♯‘𝐴) + 𝑐)))
132	123, 128, 131	3eltr3d 2847	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + (♯‘𝑓)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)))
133	118, 132	eqeltrd 2833	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘(𝐴 ++ 𝑓)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)))
134		lencl 14479	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ Word (𝐼 × 2o) → (♯‘𝐵) ∈ ℕ0)
135	88, 134	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐵) ∈ ℕ0)
136		uzaddcl 12884	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘(𝐴 ++ 𝑓)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)) ∧ (♯‘𝐵) ∈ ℕ0) → ((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)))
137	133, 135, 136	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)))
138	116, 137	eqeltrd 2833	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘((𝐴 ++ 𝑓) ++ 𝐵)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)))
139		elfzuzb 13491	. . . . . . . . . . . . . . . 16 ⊢ (((♯‘𝐴) + 𝑐) ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) ↔ (((♯‘𝐴) + 𝑐) ∈ (ℤ≥‘0) ∧ (♯‘((𝐴 ++ 𝑓) ++ 𝐵)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐))))
140	113, 138, 139	sylanbrc 583	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))))
141	1, 2, 3, 4	efgtval 19585	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 ∧ ((♯‘𝐴) + 𝑐) ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) ∧ 𝑢 ∈ (𝐼 × 2o)) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨((♯‘𝐴) + 𝑐), ((♯‘𝐴) + 𝑐), ⟨“𝑢(𝑀‘𝑢)”⟩⟩))
142	72, 140, 70, 141	syl3anc 1371	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨((♯‘𝐴) + 𝑐), ((♯‘𝐴) + 𝑐), ⟨“𝑢(𝑀‘𝑢)”⟩⟩))
143		wrd0 14485	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ Word (𝐼 × 2o)
144	143	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ∅ ∈ Word (𝐼 × 2o))
145		ccatcl 14520	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵) ∈ Word (𝐼 × 2o))
146	87, 88, 145	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵) ∈ Word (𝐼 × 2o))
147		ccatrid 14533	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) = (𝐴 ++ (𝑓 prefix 𝑐)))
148	79, 147	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) = (𝐴 ++ (𝑓 prefix 𝑐)))
149	148	oveq1d 7420	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)) = ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
150		ccatass 14534	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o) ∧ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
151	79, 87, 88, 150	syl3anc 1371	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
152		ccatass 14534	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o) ∧ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o)) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
153	74, 77, 87, 152	syl3anc 1371	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
154	125, 108	eleqtrdi 2843	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ (ℤ≥‘0))
155		eluzfz2 13505	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝑓) ∈ (ℤ≥‘0) → (♯‘𝑓) ∈ (0...(♯‘𝑓)))
156	154, 155	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ (0...(♯‘𝑓)))
157		ccatpfx 14647	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 ∈ Word (𝐼 × 2o) ∧ 𝑐 ∈ (0...(♯‘𝑓)) ∧ (♯‘𝑓) ∈ (0...(♯‘𝑓))) → ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝑓 prefix (♯‘𝑓)))
158	75, 69, 156, 157	syl3anc 1371	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝑓 prefix (♯‘𝑓)))
159		pfxid 14630	. . . . . . . . . . . . . . . . . . . . 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 7421	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))) = (𝐴 ++ 𝑓))
163	153, 162	eqtrd 2772	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ 𝑓))
164	163	oveq1d 7420	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = ((𝐴 ++ 𝑓) ++ 𝐵))
165	149, 151, 164	3eqtr2rd 2779	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ 𝑓) ++ 𝐵) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
166		ccatlen 14521	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o)) → (♯‘(𝐴 ++ (𝑓 prefix 𝑐))) = ((♯‘𝐴) + (♯‘(𝑓 prefix 𝑐))))
167	74, 77, 166	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘(𝐴 ++ (𝑓 prefix 𝑐))) = ((♯‘𝐴) + (♯‘(𝑓 prefix 𝑐))))
168		pfxlen 14629	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ Word (𝐼 × 2o) ∧ 𝑐 ∈ (0...(♯‘𝑓))) → (♯‘(𝑓 prefix 𝑐)) = 𝑐)
169	75, 69, 168	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘(𝑓 prefix 𝑐)) = 𝑐)
170	169	oveq2d 7421	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + (♯‘(𝑓 prefix 𝑐))) = ((♯‘𝐴) + 𝑐))
171	167, 170	eqtr2d 2773	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) = (♯‘(𝐴 ++ (𝑓 prefix 𝑐))))
172		hash0 14323	. . . . . . . . . . . . . . . . 17 ⊢ (♯‘∅) = 0
173	172	oveq2i 7416	. . . . . . . . . . . . . . . 16 ⊢ (((♯‘𝐴) + 𝑐) + (♯‘∅)) = (((♯‘𝐴) + 𝑐) + 0)
174	107, 111	nn0addcld 12532	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) ∈ ℕ0)
175	174	nn0cnd 12530	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) ∈ ℂ)
176	175	addridd 11410	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((♯‘𝐴) + 𝑐) + 0) = ((♯‘𝐴) + 𝑐))
177	173, 176	eqtr2id 2785	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) = (((♯‘𝐴) + 𝑐) + (♯‘∅)))
178	79, 144, 146, 83, 165, 171, 177	splval2 14703	. . . . . . . . . . . . . 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 19584	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 → ((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) = (𝑎 ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))), 𝑏 ∈ (𝐼 × 2o) ↦ (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀‘𝑏)”⟩⟩)) ∧ (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o))⟶𝑊))
182	181	simprd 496	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o))⟶𝑊)
183		ffn 6714	. . . . . . . . . . . . . 14 ⊢ ((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o))⟶𝑊 → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o)))
184	72, 182, 183	3syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o)))
185		fnovrn 7578	. . . . . . . . . . . . 13 ⊢ (((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o)) ∧ ((♯‘𝐴) + 𝑐) ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) ∧ 𝑢 ∈ (𝐼 × 2o)) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)))
186	184, 140, 70, 185	syl3anc 1371	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)))
187	180, 186	eqeltrd 2833	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)))
188	1, 2, 3, 4	efgi2 19587	. . . . . . . . . . 11 ⊢ ((((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 ∧ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵))
189	72, 187, 188	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵))
190	1, 2, 3, 4, 9, 10, 6	efgcpbllema 19616	. . . . . . . . . 10 ⊢ (𝑓𝐿(𝑐(𝑇‘𝑓)𝑢) ↔ (𝑓 ∈ 𝑊 ∧ (𝑐(𝑇‘𝑓)𝑢) ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵)))
191	67, 71, 189, 190	syl3anbrc 1343	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑓𝐿(𝑐(𝑇‘𝑓)𝑢))
192		vex 3478	. . . . . . . . . . 11 ⊢ 𝑎 ∈ V
193		vex 3478	. . . . . . . . . . 11 ⊢ 𝑓 ∈ V
194	192, 193	elec 8743	. . . . . . . . . 10 ⊢ (𝑎 ∈ [𝑓]𝐿 ↔ 𝑓𝐿𝑎)
195		breq2 5151	. . . . . . . . . 10 ⊢ (𝑎 = (𝑐(𝑇‘𝑓)𝑢) → (𝑓𝐿𝑎 ↔ 𝑓𝐿(𝑐(𝑇‘𝑓)𝑢)))
196	194, 195	bitrid 282	. . . . . . . . 9 ⊢ (𝑎 = (𝑐(𝑇‘𝑓)𝑢) → (𝑎 ∈ [𝑓]𝐿 ↔ 𝑓𝐿(𝑐(𝑇‘𝑓)𝑢)))
197	191, 196	syl5ibrcom 246	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑎 = (𝑐(𝑇‘𝑓)𝑢) → 𝑎 ∈ [𝑓]𝐿))
198	197	rexlimdvva 3211	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (∃𝑐 ∈ (0...(♯‘𝑓))∃𝑢 ∈ (𝐼 × 2o)𝑎 = (𝑐(𝑇‘𝑓)𝑢) → 𝑎 ∈ [𝑓]𝐿))
199	66, 198	sylbid 239	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝑎 ∈ ran (𝑇‘𝑓) → 𝑎 ∈ [𝑓]𝐿))
200	199	ssrdv 3987	. . . . 5 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)
201	200	ralrimiva 3146	. . . 4 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)
202	1	fvexi 6902	. . . . . 6 ⊢ 𝑊 ∈ V
203		erex 8723	. . . . . 6 ⊢ (𝐿 Er 𝑊 → (𝑊 ∈ V → 𝐿 ∈ V))
204	60, 202, 203	mpisyl 21	. . . . 5 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐿 ∈ V)
205		ereq1 8706	. . . . . . 7 ⊢ (𝑟 = 𝐿 → (𝑟 Er 𝑊 ↔ 𝐿 Er 𝑊))
206		eceq2 8739	. . . . . . . . 9 ⊢ (𝑟 = 𝐿 → [𝑓]𝑟 = [𝑓]𝐿)
207	206	sseq2d 4013	. . . . . . . 8 ⊢ (𝑟 = 𝐿 → (ran (𝑇‘𝑓) ⊆ [𝑓]𝑟 ↔ ran (𝑇‘𝑓) ⊆ [𝑓]𝐿))
208	207	ralbidv 3177	. . . . . . 7 ⊢ (𝑟 = 𝐿 → (∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟 ↔ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿))
209	205, 208	anbi12d 631	. . . . . 6 ⊢ (𝑟 = 𝐿 → ((𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟) ↔ (𝐿 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)))
210	209	elabg 3665	. . . . 5 ⊢ (𝐿 ∈ V → (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ↔ (𝐿 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)))
211	204, 210	syl 17	. . . 4 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ↔ (𝐿 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)))
212	60, 201, 211	mpbir2and 711	. . 3 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)})
213		intss1 4966	. . 3 ⊢ (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} → ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ⊆ 𝐿)
214	212, 213	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ⊆ 𝐿)
215	5, 214	eqsstrid 4029	1 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ∼ ⊆ 𝐿)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  {cab 2709  ∀wral 3061  ∃wrex 3070  {crab 3432  Vcvv 3474   ∖ cdif 3944   ⊆ wss 3947  ∅c0 4321  {csn 4627  {cpr 4629  ⟨cop 4633  ⟨cotp 4635  ∩ cint 4949  ∪ ciun 4996   class class class wbr 5147  {copab 5209   ↦ cmpt 5230   I cid 5572   × cxp 5673  ran crn 5676  Rel wrel 5680   Fn wfn 6535  ⟶wf 6536  ‘cfv 6540  (class class class)co 7405   ∈ cmpo 7407  1_oc1o 8455  2_oc2o 8456   Er wer 8696  [cec 8697  0cc0 11106  1c1 11107   + caddc 11109   − cmin 11440  ℕ₀cn0 12468  ℤcz 12554  ℤ_≥cuz 12818  ...cfz 13480  ..^cfzo 13623  ♯chash 14286  Word cword 14460   ++ cconcat 14516   substr csubstr 14586   prefix cpfx 14616   splice csplice 14695  ⟨“cs2 14788   ~_FG cefg 19568

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-ot 4636  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-er 8699  df-ec 8701  df-map 8818  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-n0 12469  df-z 12555  df-uz 12819  df-fz 13481  df-fzo 13624  df-hash 14287  df-word 14461  df-concat 14517  df-s1 14542  df-substr 14587  df-pfx 14617  df-splice 14696  df-s2 14795  df-efg 19571

This theorem is referenced by:  efgcpbl  19618