Theorem efgcpbllemb 19276

Description: Lemma for efgrelex 19272. 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 19245	. 2 ⊢ ∼ = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)}
6		efgcpbllem.1	. . . . . . 7 ⊢ 𝐿 = {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑊 ∧ ((𝐴 ++ 𝑖) ++ 𝐵) ∼ ((𝐴 ++ 𝑗) ++ 𝐵))}
7	6	relopabiv 5719	. . . . . 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 19275	. . . . . . . 8 ⊢ (𝑓𝐿𝑔 ↔ (𝑓 ∈ 𝑊 ∧ 𝑔 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵)))
12	11	simp2bi 1144	. . . . . . 7 ⊢ (𝑓𝐿𝑔 → 𝑔 ∈ 𝑊)
13	12	adantl 481	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → 𝑔 ∈ 𝑊)
14	11	simp1bi 1143	. . . . . . 7 ⊢ (𝑓𝐿𝑔 → 𝑓 ∈ 𝑊)
15	14	adantl 481	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → 𝑓 ∈ 𝑊)
16	1, 2	efger 19239	. . . . . . . 8 ⊢ ∼ Er 𝑊
17	16	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → ∼ Er 𝑊)
18	11	simp3bi 1145	. . . . . . . 8 ⊢ (𝑓𝐿𝑔 → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵))
19	18	adantl 481	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵))
20	17, 19	ersym 8468	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))
21	1, 2, 3, 4, 9, 10, 6	efgcpbllema 19275	. . . . . 6 ⊢ (𝑔𝐿𝑓 ↔ (𝑔 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
22	13, 15, 20, 21	syl3anbrc 1341	. . . . 5 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → 𝑔𝐿𝑓)
23	14	ad2antrl 724	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → 𝑓 ∈ 𝑊)
24	1, 2, 3, 4, 9, 10, 6	efgcpbllema 19275	. . . . . . . 8 ⊢ (𝑔𝐿ℎ ↔ (𝑔 ∈ 𝑊 ∧ ℎ ∈ 𝑊 ∧ ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵)))
25	24	simp2bi 1144	. . . . . . 7 ⊢ (𝑔𝐿ℎ → ℎ ∈ 𝑊)
26	25	ad2antll 725	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ℎ ∈ 𝑊)
27	16	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ∼ Er 𝑊)
28	18	ad2antrl 724	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵))
29	24	simp3bi 1145	. . . . . . . 8 ⊢ (𝑔𝐿ℎ → ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵))
30	29	ad2antll 725	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵))
31	27, 28, 30	ertrd 8472	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵))
32	1, 2, 3, 4, 9, 10, 6	efgcpbllema 19275	. . . . . 6 ⊢ (𝑓𝐿ℎ ↔ (𝑓 ∈ 𝑊 ∧ ℎ ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵)))
33	23, 26, 31, 32	syl3anbrc 1341	. . . . 5 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → 𝑓𝐿ℎ)
34	16	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ∼ Er 𝑊)
35		fviss 6827	. . . . . . . . . . . . . 14 ⊢ ( I ‘Word (𝐼 × 2o)) ⊆ Word (𝐼 × 2o)
36	1, 35	eqsstri 3951	. . . . . . . . . . . . 13 ⊢ 𝑊 ⊆ Word (𝐼 × 2o)
37		simpll 763	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐴 ∈ 𝑊)
38	36, 37	sselid 3915	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐴 ∈ Word (𝐼 × 2o))
39		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝑓 ∈ 𝑊)
40	36, 39	sselid 3915	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝑓 ∈ Word (𝐼 × 2o))
41		ccatcl 14205	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ 𝑓 ∈ Word (𝐼 × 2o)) → (𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o))
42	38, 40, 41	syl2anc 583	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o))
43		simplr 765	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐵 ∈ 𝑊)
44	36, 43	sselid 3915	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐵 ∈ Word (𝐼 × 2o))
45		ccatcl 14205	. . . . . . . . . . 11 ⊢ (((𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ Word (𝐼 × 2o))
46	42, 44, 45	syl2anc 583	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ Word (𝐼 × 2o))
47	1	efgrcl 19236	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o)))
48	47	simprd 495	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑊 → 𝑊 = Word (𝐼 × 2o))
49	48	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝑊 = Word (𝐼 × 2o))
50	46, 49	eleqtrrd 2842	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊)
51	34, 50	erref 8476	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))
52	51	ex 412	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝑓 ∈ 𝑊 → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
53	52	pm4.71d 561	. . . . . 6 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝑓 ∈ 𝑊 ↔ (𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))))
54	1, 2, 3, 4, 9, 10, 6	efgcpbllema 19275	. . . . . . 7 ⊢ (𝑓𝐿𝑓 ↔ (𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
55		df-3an 1087	. . . . . . 7 ⊢ ((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)) ↔ ((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊) ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
56		anidm 564	. . . . . . . 8 ⊢ ((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊) ↔ 𝑓 ∈ 𝑊)
57	56	anbi1i 623	. . . . . . 7 ⊢ (((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊) ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)) ↔ (𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
58	54, 55, 57	3bitri 296	. . . . . 6 ⊢ (𝑓𝐿𝑓 ↔ (𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
59	53, 58	bitr4di 288	. . . . 5 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝑓 ∈ 𝑊 ↔ 𝑓𝐿𝑓))
60	8, 22, 33, 59	iserd 8482	. . . 4 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐿 Er 𝑊)
61	1, 2, 3, 4	efgtf 19243	. . . . . . . . . 10 ⊢ (𝑓 ∈ 𝑊 → ((𝑇‘𝑓) = (𝑎 ∈ (0...(♯‘𝑓)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑓 splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀‘𝑏)”⟩⟩)) ∧ (𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊))
62	61	simprd 495	. . . . . . . . 9 ⊢ (𝑓 ∈ 𝑊 → (𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊)
63	62	adantl 481	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊)
64		ffn 6584	. . . . . . . 8 ⊢ ((𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊 → (𝑇‘𝑓) Fn ((0...(♯‘𝑓)) × (𝐼 × 2o)))
65		ovelrn 7426	. . . . . . . 8 ⊢ ((𝑇‘𝑓) Fn ((0...(♯‘𝑓)) × (𝐼 × 2o)) → (𝑎 ∈ ran (𝑇‘𝑓) ↔ ∃𝑐 ∈ (0...(♯‘𝑓))∃𝑢 ∈ (𝐼 × 2o)𝑎 = (𝑐(𝑇‘𝑓)𝑢)))
66	63, 64, 65	3syl 18	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝑎 ∈ ran (𝑇‘𝑓) ↔ ∃𝑐 ∈ (0...(♯‘𝑓))∃𝑢 ∈ (𝐼 × 2o)𝑎 = (𝑐(𝑇‘𝑓)𝑢)))
67		simplr 765	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑓 ∈ 𝑊)
68	62	ad2antlr 723	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊)
69		simprl 767	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑐 ∈ (0...(♯‘𝑓)))
70		simprr 769	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑢 ∈ (𝐼 × 2o))
71	68, 69, 70	fovrnd 7422	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐(𝑇‘𝑓)𝑢) ∈ 𝑊)
72	50	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊)
73	37	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝐴 ∈ 𝑊)
74	36, 73	sselid 3915	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝐴 ∈ Word (𝐼 × 2o))
75	40	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑓 ∈ Word (𝐼 × 2o))
76		pfxcl 14318	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ Word (𝐼 × 2o) → (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o))
77	75, 76	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o))
78		ccatcl 14205	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o)) → (𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o))
79	74, 77, 78	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o))
80	3	efgmf 19234	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑀:(𝐼 × 2o)⟶(𝐼 × 2o)
81	80	ffvelrni 6942	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ (𝐼 × 2o) → (𝑀‘𝑢) ∈ (𝐼 × 2o))
82	81	ad2antll 725	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑀‘𝑢) ∈ (𝐼 × 2o))
83	70, 82	s2cld 14512	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ⟨“𝑢(𝑀‘𝑢)”⟩ ∈ Word (𝐼 × 2o))
84		ccatcl 14205	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑢(𝑀‘𝑢)”⟩ ∈ Word (𝐼 × 2o)) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o))
85	79, 83, 84	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o))
86		swrdcl 14286	. . . . . . . . . . . . . . 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 14221	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o) ∧ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
90	85, 87, 88, 89	syl3anc 1369	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
91		ccatcl 14205	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑢(𝑀‘𝑢)”⟩ ∈ Word (𝐼 × 2o)) → ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o))
92	77, 83, 91	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o))
93		ccatass 14221	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o) ∧ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o)) → ((𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
94	74, 92, 87, 93	syl3anc 1369	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
95		ccatass 14221	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑢(𝑀‘𝑢)”⟩ ∈ Word (𝐼 × 2o)) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩)))
96	74, 77, 83, 95	syl3anc 1369	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩)))
97	96	oveq1d 7270	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = ((𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
98	1, 2, 3, 4	efgtval 19244	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ 𝑊 ∧ 𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o)) → (𝑐(𝑇‘𝑓)𝑢) = (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀‘𝑢)”⟩⟩))
99	67, 69, 70, 98	syl3anc 1369	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐(𝑇‘𝑓)𝑢) = (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀‘𝑢)”⟩⟩))
100		splval 14392	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ 𝑊 ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑐 ∈ (0...(♯‘𝑓)) ∧ ⟨“𝑢(𝑀‘𝑢)”⟩ ∈ Word (𝐼 × 2o))) → (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀‘𝑢)”⟩⟩) = (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
101	67, 69, 69, 83, 100	syl13anc 1370	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀‘𝑢)”⟩⟩) = (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
102	99, 101	eqtrd 2778	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐(𝑇‘𝑓)𝑢) = (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
103	102	oveq2d 7271	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) = (𝐴 ++ (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
104	94, 97, 103	3eqtr4rd 2789	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
105	104	oveq1d 7270	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) = ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵))
106		lencl 14164	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ Word (𝐼 × 2o) → (♯‘𝐴) ∈ ℕ0)
107	74, 106	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐴) ∈ ℕ0)
108		nn0uz 12549	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ0 = (ℤ≥‘0)
109	107, 108	eleqtrdi 2849	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐴) ∈ (ℤ≥‘0))
110		elfznn0 13278	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ (0...(♯‘𝑓)) → 𝑐 ∈ ℕ0)
111	110	ad2antrl 724	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑐 ∈ ℕ0)
112		uzaddcl 12573	. . . . . . . . . . . . . . . . 17 ⊢ (((♯‘𝐴) ∈ (ℤ≥‘0) ∧ 𝑐 ∈ ℕ0) → ((♯‘𝐴) + 𝑐) ∈ (ℤ≥‘0))
113	109, 111, 112	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) ∈ (ℤ≥‘0))
114	42	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o))
115		ccatlen 14206	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → (♯‘((𝐴 ++ 𝑓) ++ 𝐵)) = ((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵)))
116	114, 88, 115	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘((𝐴 ++ 𝑓) ++ 𝐵)) = ((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵)))
117		ccatlen 14206	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ 𝑓 ∈ Word (𝐼 × 2o)) → (♯‘(𝐴 ++ 𝑓)) = ((♯‘𝐴) + (♯‘𝑓)))
118	74, 75, 117	syl2anc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘(𝐴 ++ 𝑓)) = ((♯‘𝐴) + (♯‘𝑓)))
119		elfzuz3 13182	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 ∈ (0...(♯‘𝑓)) → (♯‘𝑓) ∈ (ℤ≥‘𝑐))
120	119	ad2antrl 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ (ℤ≥‘𝑐))
121	107	nn0zd 12353	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐴) ∈ ℤ)
122		eluzadd 12542	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((♯‘𝑓) ∈ (ℤ≥‘𝑐) ∧ (♯‘𝐴) ∈ ℤ) → ((♯‘𝑓) + (♯‘𝐴)) ∈ (ℤ≥‘(𝑐 + (♯‘𝐴))))
123	120, 121, 122	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝑓) + (♯‘𝐴)) ∈ (ℤ≥‘(𝑐 + (♯‘𝐴))))
124		lencl 14164	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∈ Word (𝐼 × 2o) → (♯‘𝑓) ∈ ℕ0)
125	75, 124	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ ℕ0)
126	125	nn0cnd 12225	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ ℂ)
127	107	nn0cnd 12225	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐴) ∈ ℂ)
128	126, 127	addcomd 11107	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝑓) + (♯‘𝐴)) = ((♯‘𝐴) + (♯‘𝑓)))
129	111	nn0cnd 12225	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑐 ∈ ℂ)
130	129, 127	addcomd 11107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐 + (♯‘𝐴)) = ((♯‘𝐴) + 𝑐))
131	130	fveq2d 6760	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (ℤ≥‘(𝑐 + (♯‘𝐴))) = (ℤ≥‘((♯‘𝐴) + 𝑐)))
132	123, 128, 131	3eltr3d 2853	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + (♯‘𝑓)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)))
133	118, 132	eqeltrd 2839	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘(𝐴 ++ 𝑓)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)))
134		lencl 14164	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ Word (𝐼 × 2o) → (♯‘𝐵) ∈ ℕ0)
135	88, 134	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐵) ∈ ℕ0)
136		uzaddcl 12573	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘(𝐴 ++ 𝑓)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)) ∧ (♯‘𝐵) ∈ ℕ0) → ((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)))
137	133, 135, 136	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)))
138	116, 137	eqeltrd 2839	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘((𝐴 ++ 𝑓) ++ 𝐵)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)))
139		elfzuzb 13179	. . . . . . . . . . . . . . . 16 ⊢ (((♯‘𝐴) + 𝑐) ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) ↔ (((♯‘𝐴) + 𝑐) ∈ (ℤ≥‘0) ∧ (♯‘((𝐴 ++ 𝑓) ++ 𝐵)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐))))
140	113, 138, 139	sylanbrc 582	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))))
141	1, 2, 3, 4	efgtval 19244	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 ∧ ((♯‘𝐴) + 𝑐) ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) ∧ 𝑢 ∈ (𝐼 × 2o)) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨((♯‘𝐴) + 𝑐), ((♯‘𝐴) + 𝑐), ⟨“𝑢(𝑀‘𝑢)”⟩⟩))
142	72, 140, 70, 141	syl3anc 1369	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨((♯‘𝐴) + 𝑐), ((♯‘𝐴) + 𝑐), ⟨“𝑢(𝑀‘𝑢)”⟩⟩))
143		wrd0 14170	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ Word (𝐼 × 2o)
144	143	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ∅ ∈ Word (𝐼 × 2o))
145		ccatcl 14205	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵) ∈ Word (𝐼 × 2o))
146	87, 88, 145	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵) ∈ Word (𝐼 × 2o))
147		ccatrid 14220	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) = (𝐴 ++ (𝑓 prefix 𝑐)))
148	79, 147	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) = (𝐴 ++ (𝑓 prefix 𝑐)))
149	148	oveq1d 7270	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)) = ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
150		ccatass 14221	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o) ∧ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
151	79, 87, 88, 150	syl3anc 1369	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
152		ccatass 14221	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o) ∧ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o)) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
153	74, 77, 87, 152	syl3anc 1369	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
154	125, 108	eleqtrdi 2849	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ (ℤ≥‘0))
155		eluzfz2 13193	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝑓) ∈ (ℤ≥‘0) → (♯‘𝑓) ∈ (0...(♯‘𝑓)))
156	154, 155	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ (0...(♯‘𝑓)))
157		ccatpfx 14342	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 ∈ Word (𝐼 × 2o) ∧ 𝑐 ∈ (0...(♯‘𝑓)) ∧ (♯‘𝑓) ∈ (0...(♯‘𝑓))) → ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝑓 prefix (♯‘𝑓)))
158	75, 69, 156, 157	syl3anc 1369	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝑓 prefix (♯‘𝑓)))
159		pfxid 14325	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ Word (𝐼 × 2o) → (𝑓 prefix (♯‘𝑓)) = 𝑓)
160	75, 159	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑓 prefix (♯‘𝑓)) = 𝑓)
161	158, 160	eqtrd 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = 𝑓)
162	161	oveq2d 7271	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))) = (𝐴 ++ 𝑓))
163	153, 162	eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ 𝑓))
164	163	oveq1d 7270	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = ((𝐴 ++ 𝑓) ++ 𝐵))
165	149, 151, 164	3eqtr2rd 2785	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ 𝑓) ++ 𝐵) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
166		ccatlen 14206	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o)) → (♯‘(𝐴 ++ (𝑓 prefix 𝑐))) = ((♯‘𝐴) + (♯‘(𝑓 prefix 𝑐))))
167	74, 77, 166	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘(𝐴 ++ (𝑓 prefix 𝑐))) = ((♯‘𝐴) + (♯‘(𝑓 prefix 𝑐))))
168		pfxlen 14324	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ Word (𝐼 × 2o) ∧ 𝑐 ∈ (0...(♯‘𝑓))) → (♯‘(𝑓 prefix 𝑐)) = 𝑐)
169	75, 69, 168	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘(𝑓 prefix 𝑐)) = 𝑐)
170	169	oveq2d 7271	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + (♯‘(𝑓 prefix 𝑐))) = ((♯‘𝐴) + 𝑐))
171	167, 170	eqtr2d 2779	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) = (♯‘(𝐴 ++ (𝑓 prefix 𝑐))))
172		hash0 14010	. . . . . . . . . . . . . . . . 17 ⊢ (♯‘∅) = 0
173	172	oveq2i 7266	. . . . . . . . . . . . . . . 16 ⊢ (((♯‘𝐴) + 𝑐) + (♯‘∅)) = (((♯‘𝐴) + 𝑐) + 0)
174	107, 111	nn0addcld 12227	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) ∈ ℕ0)
175	174	nn0cnd 12225	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) ∈ ℂ)
176	175	addid1d 11105	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((♯‘𝐴) + 𝑐) + 0) = ((♯‘𝐴) + 𝑐))
177	173, 176	eqtr2id 2792	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) = (((♯‘𝐴) + 𝑐) + (♯‘∅)))
178	79, 144, 146, 83, 165, 171, 177	splval2 14398	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨((♯‘𝐴) + 𝑐), ((♯‘𝐴) + 𝑐), ⟨“𝑢(𝑀‘𝑢)”⟩⟩) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
179	142, 178	eqtrd 2778	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
180	90, 105, 179	3eqtr4d 2788	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) = (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢))
181	1, 2, 3, 4	efgtf 19243	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 → ((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) = (𝑎 ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))), 𝑏 ∈ (𝐼 × 2o) ↦ (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀‘𝑏)”⟩⟩)) ∧ (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o))⟶𝑊))
182	181	simprd 495	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o))⟶𝑊)
183		ffn 6584	. . . . . . . . . . . . . 14 ⊢ ((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o))⟶𝑊 → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o)))
184	72, 182, 183	3syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o)))
185		fnovrn 7425	. . . . . . . . . . . . 13 ⊢ (((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o)) ∧ ((♯‘𝐴) + 𝑐) ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) ∧ 𝑢 ∈ (𝐼 × 2o)) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)))
186	184, 140, 70, 185	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)))
187	180, 186	eqeltrd 2839	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)))
188	1, 2, 3, 4	efgi2 19246	. . . . . . . . . . 11 ⊢ ((((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 ∧ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵))
189	72, 187, 188	syl2anc 583	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵))
190	1, 2, 3, 4, 9, 10, 6	efgcpbllema 19275	. . . . . . . . . 10 ⊢ (𝑓𝐿(𝑐(𝑇‘𝑓)𝑢) ↔ (𝑓 ∈ 𝑊 ∧ (𝑐(𝑇‘𝑓)𝑢) ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵)))
191	67, 71, 189, 190	syl3anbrc 1341	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑓𝐿(𝑐(𝑇‘𝑓)𝑢))
192		vex 3426	. . . . . . . . . . 11 ⊢ 𝑎 ∈ V
193		vex 3426	. . . . . . . . . . 11 ⊢ 𝑓 ∈ V
194	192, 193	elec 8500	. . . . . . . . . 10 ⊢ (𝑎 ∈ [𝑓]𝐿 ↔ 𝑓𝐿𝑎)
195		breq2 5074	. . . . . . . . . 10 ⊢ (𝑎 = (𝑐(𝑇‘𝑓)𝑢) → (𝑓𝐿𝑎 ↔ 𝑓𝐿(𝑐(𝑇‘𝑓)𝑢)))
196	194, 195	syl5bb 282	. . . . . . . . 9 ⊢ (𝑎 = (𝑐(𝑇‘𝑓)𝑢) → (𝑎 ∈ [𝑓]𝐿 ↔ 𝑓𝐿(𝑐(𝑇‘𝑓)𝑢)))
197	191, 196	syl5ibrcom 246	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑎 = (𝑐(𝑇‘𝑓)𝑢) → 𝑎 ∈ [𝑓]𝐿))
198	197	rexlimdvva 3222	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (∃𝑐 ∈ (0...(♯‘𝑓))∃𝑢 ∈ (𝐼 × 2o)𝑎 = (𝑐(𝑇‘𝑓)𝑢) → 𝑎 ∈ [𝑓]𝐿))
199	66, 198	sylbid 239	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝑎 ∈ ran (𝑇‘𝑓) → 𝑎 ∈ [𝑓]𝐿))
200	199	ssrdv 3923	. . . . 5 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)
201	200	ralrimiva 3107	. . . 4 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)
202	1	fvexi 6770	. . . . . 6 ⊢ 𝑊 ∈ V
203		erex 8480	. . . . . 6 ⊢ (𝐿 Er 𝑊 → (𝑊 ∈ V → 𝐿 ∈ V))
204	60, 202, 203	mpisyl 21	. . . . 5 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐿 ∈ V)
205		ereq1 8463	. . . . . . 7 ⊢ (𝑟 = 𝐿 → (𝑟 Er 𝑊 ↔ 𝐿 Er 𝑊))
206		eceq2 8496	. . . . . . . . 9 ⊢ (𝑟 = 𝐿 → [𝑓]𝑟 = [𝑓]𝐿)
207	206	sseq2d 3949	. . . . . . . 8 ⊢ (𝑟 = 𝐿 → (ran (𝑇‘𝑓) ⊆ [𝑓]𝑟 ↔ ran (𝑇‘𝑓) ⊆ [𝑓]𝐿))
208	207	ralbidv 3120	. . . . . . 7 ⊢ (𝑟 = 𝐿 → (∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟 ↔ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿))
209	205, 208	anbi12d 630	. . . . . 6 ⊢ (𝑟 = 𝐿 → ((𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟) ↔ (𝐿 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)))
210	209	elabg 3600	. . . . 5 ⊢ (𝐿 ∈ V → (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ↔ (𝐿 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)))
211	204, 210	syl 17	. . . 4 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ↔ (𝐿 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)))
212	60, 201, 211	mpbir2and 709	. . 3 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)})
213		intss1 4891	. . 3 ⊢ (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} → ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ⊆ 𝐿)
214	212, 213	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ⊆ 𝐿)
215	5, 214	eqsstrid 3965	1 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ∼ ⊆ 𝐿)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  {cab 2715  ∀wral 3063  ∃wrex 3064  {crab 3067  Vcvv 3422   ∖ cdif 3880   ⊆ wss 3883  ∅c0 4253  {csn 4558  {cpr 4560  ⟨cop 4564  ⟨cotp 4566  ∩ cint 4876  ∪ ciun 4921   class class class wbr 5070  {copab 5132   ↦ cmpt 5153   I cid 5479   × cxp 5578  ran crn 5581  Rel wrel 5585   Fn wfn 6413  ⟶wf 6414  ‘cfv 6418  (class class class)co 7255   ∈ cmpo 7257  1_oc1o 8260  2_oc2o 8261   Er wer 8453  [cec 8454  0cc0 10802  1c1 10803   + caddc 10805   − cmin 11135  ℕ₀cn0 12163  ℤcz 12249  ℤ_≥cuz 12511  ...cfz 13168  ..^cfzo 13311  ♯chash 13972  Word cword 14145   ++ cconcat 14201   substr csubstr 14281   prefix cpfx 14311   splice csplice 14390  ⟨“cs2 14482   ~_FG cefg 19227

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-ot 4567  df-uni 4837  df-int 4877  df-iun 4923  df-iin 4924  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-1st 7804  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-1o 8267  df-2o 8268  df-er 8456  df-ec 8458  df-map 8575  df-en 8692  df-dom 8693  df-sdom 8694  df-fin 8695  df-card 9628  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-nn 11904  df-n0 12164  df-z 12250  df-uz 12512  df-fz 13169  df-fzo 13312  df-hash 13973  df-word 14146  df-concat 14202  df-s1 14229  df-substr 14282  df-pfx 14312  df-splice 14391  df-s2 14489  df-efg 19230

This theorem is referenced by:  efgcpbl  19277