Theorem efgcpbllemb 18873

Description: Lemma for efgrelex 18869. 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 18842	. 2 ⊢ ∼ = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)}
6		efgcpbllem.1	. . . . . . 7 ⊢ 𝐿 = {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑊 ∧ ((𝐴 ++ 𝑖) ++ 𝐵) ∼ ((𝐴 ++ 𝑗) ++ 𝐵))}
7	6	relopabi 5658	. . . . . 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 18872	. . . . . . . 8 ⊢ (𝑓𝐿𝑔 ↔ (𝑓 ∈ 𝑊 ∧ 𝑔 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵)))
12	11	simp2bi 1143	. . . . . . 7 ⊢ (𝑓𝐿𝑔 → 𝑔 ∈ 𝑊)
13	12	adantl 485	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → 𝑔 ∈ 𝑊)
14	11	simp1bi 1142	. . . . . . 7 ⊢ (𝑓𝐿𝑔 → 𝑓 ∈ 𝑊)
15	14	adantl 485	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → 𝑓 ∈ 𝑊)
16	1, 2	efger 18836	. . . . . . . 8 ⊢ ∼ Er 𝑊
17	16	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → ∼ Er 𝑊)
18	11	simp3bi 1144	. . . . . . . 8 ⊢ (𝑓𝐿𝑔 → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵))
19	18	adantl 485	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵))
20	17, 19	ersym 8284	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))
21	1, 2, 3, 4, 9, 10, 6	efgcpbllema 18872	. . . . . 6 ⊢ (𝑔𝐿𝑓 ↔ (𝑔 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
22	13, 15, 20, 21	syl3anbrc 1340	. . . . 5 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → 𝑔𝐿𝑓)
23	14	ad2antrl 727	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → 𝑓 ∈ 𝑊)
24	1, 2, 3, 4, 9, 10, 6	efgcpbllema 18872	. . . . . . . 8 ⊢ (𝑔𝐿ℎ ↔ (𝑔 ∈ 𝑊 ∧ ℎ ∈ 𝑊 ∧ ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵)))
25	24	simp2bi 1143	. . . . . . 7 ⊢ (𝑔𝐿ℎ → ℎ ∈ 𝑊)
26	25	ad2antll 728	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ℎ ∈ 𝑊)
27	16	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ∼ Er 𝑊)
28	18	ad2antrl 727	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵))
29	24	simp3bi 1144	. . . . . . . 8 ⊢ (𝑔𝐿ℎ → ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵))
30	29	ad2antll 728	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵))
31	27, 28, 30	ertrd 8288	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵))
32	1, 2, 3, 4, 9, 10, 6	efgcpbllema 18872	. . . . . 6 ⊢ (𝑓𝐿ℎ ↔ (𝑓 ∈ 𝑊 ∧ ℎ ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵)))
33	23, 26, 31, 32	syl3anbrc 1340	. . . . 5 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → 𝑓𝐿ℎ)
34	16	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ∼ Er 𝑊)
35		fviss 6716	. . . . . . . . . . . . . 14 ⊢ ( I ‘Word (𝐼 × 2o)) ⊆ Word (𝐼 × 2o)
36	1, 35	eqsstri 3949	. . . . . . . . . . . . 13 ⊢ 𝑊 ⊆ Word (𝐼 × 2o)
37		simpll 766	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐴 ∈ 𝑊)
38	36, 37	sseldi 3913	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐴 ∈ Word (𝐼 × 2o))
39		simpr 488	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝑓 ∈ 𝑊)
40	36, 39	sseldi 3913	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝑓 ∈ Word (𝐼 × 2o))
41		ccatcl 13917	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ 𝑓 ∈ Word (𝐼 × 2o)) → (𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o))
42	38, 40, 41	syl2anc 587	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o))
43		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐵 ∈ 𝑊)
44	36, 43	sseldi 3913	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐵 ∈ Word (𝐼 × 2o))
45		ccatcl 13917	. . . . . . . . . . 11 ⊢ (((𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ Word (𝐼 × 2o))
46	42, 44, 45	syl2anc 587	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ Word (𝐼 × 2o))
47	1	efgrcl 18833	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o)))
48	47	simprd 499	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑊 → 𝑊 = Word (𝐼 × 2o))
49	48	ad2antrr 725	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝑊 = Word (𝐼 × 2o))
50	46, 49	eleqtrrd 2893	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊)
51	34, 50	erref 8292	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))
52	51	ex 416	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝑓 ∈ 𝑊 → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
53	52	pm4.71d 565	. . . . . 6 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝑓 ∈ 𝑊 ↔ (𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))))
54	1, 2, 3, 4, 9, 10, 6	efgcpbllema 18872	. . . . . . 7 ⊢ (𝑓𝐿𝑓 ↔ (𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
55		df-3an 1086	. . . . . . 7 ⊢ ((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)) ↔ ((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊) ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
56		anidm 568	. . . . . . . 8 ⊢ ((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊) ↔ 𝑓 ∈ 𝑊)
57	56	anbi1i 626	. . . . . . 7 ⊢ (((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊) ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)) ↔ (𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
58	54, 55, 57	3bitri 300	. . . . . 6 ⊢ (𝑓𝐿𝑓 ↔ (𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))
59	53, 58	syl6bbr 292	. . . . 5 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝑓 ∈ 𝑊 ↔ 𝑓𝐿𝑓))
60	8, 22, 33, 59	iserd 8298	. . . 4 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐿 Er 𝑊)
61	1, 2, 3, 4	efgtf 18840	. . . . . . . . . 10 ⊢ (𝑓 ∈ 𝑊 → ((𝑇‘𝑓) = (𝑎 ∈ (0...(♯‘𝑓)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑓 splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀‘𝑏)”⟩⟩)) ∧ (𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊))
62	61	simprd 499	. . . . . . . . 9 ⊢ (𝑓 ∈ 𝑊 → (𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊)
63	62	adantl 485	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊)
64		ffn 6487	. . . . . . . 8 ⊢ ((𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊 → (𝑇‘𝑓) Fn ((0...(♯‘𝑓)) × (𝐼 × 2o)))
65		ovelrn 7304	. . . . . . . 8 ⊢ ((𝑇‘𝑓) Fn ((0...(♯‘𝑓)) × (𝐼 × 2o)) → (𝑎 ∈ ran (𝑇‘𝑓) ↔ ∃𝑐 ∈ (0...(♯‘𝑓))∃𝑢 ∈ (𝐼 × 2o)𝑎 = (𝑐(𝑇‘𝑓)𝑢)))
66	63, 64, 65	3syl 18	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝑎 ∈ ran (𝑇‘𝑓) ↔ ∃𝑐 ∈ (0...(♯‘𝑓))∃𝑢 ∈ (𝐼 × 2o)𝑎 = (𝑐(𝑇‘𝑓)𝑢)))
67		simplr 768	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑓 ∈ 𝑊)
68	62	ad2antlr 726	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊)
69		simprl 770	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑐 ∈ (0...(♯‘𝑓)))
70		simprr 772	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑢 ∈ (𝐼 × 2o))
71	68, 69, 70	fovrnd 7300	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐(𝑇‘𝑓)𝑢) ∈ 𝑊)
72	50	adantr 484	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊)
73	37	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝐴 ∈ 𝑊)
74	36, 73	sseldi 3913	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝐴 ∈ Word (𝐼 × 2o))
75	40	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑓 ∈ Word (𝐼 × 2o))
76		pfxcl 14030	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ Word (𝐼 × 2o) → (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o))
77	75, 76	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o))
78		ccatcl 13917	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o)) → (𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o))
79	74, 77, 78	syl2anc 587	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o))
80	3	efgmf 18831	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑀:(𝐼 × 2o)⟶(𝐼 × 2o)
81	80	ffvelrni 6827	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ (𝐼 × 2o) → (𝑀‘𝑢) ∈ (𝐼 × 2o))
82	81	ad2antll 728	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑀‘𝑢) ∈ (𝐼 × 2o))
83	70, 82	s2cld 14224	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ⟨“𝑢(𝑀‘𝑢)”⟩ ∈ Word (𝐼 × 2o))
84		ccatcl 13917	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑢(𝑀‘𝑢)”⟩ ∈ Word (𝐼 × 2o)) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o))
85	79, 83, 84	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o))
86		swrdcl 13998	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ Word (𝐼 × 2o) → (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o))
87	75, 86	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o))
88	44	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝐵 ∈ Word (𝐼 × 2o))
89		ccatass 13933	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o) ∧ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
90	85, 87, 88, 89	syl3anc 1368	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
91		ccatcl 13917	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑢(𝑀‘𝑢)”⟩ ∈ Word (𝐼 × 2o)) → ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o))
92	77, 83, 91	syl2anc 587	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o))
93		ccatass 13933	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ∈ Word (𝐼 × 2o) ∧ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o)) → ((𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
94	74, 92, 87, 93	syl3anc 1368	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
95		ccatass 13933	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑢(𝑀‘𝑢)”⟩ ∈ Word (𝐼 × 2o)) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩)))
96	74, 77, 83, 95	syl3anc 1368	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩)))
97	96	oveq1d 7150	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = ((𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
98	1, 2, 3, 4	efgtval 18841	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ 𝑊 ∧ 𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o)) → (𝑐(𝑇‘𝑓)𝑢) = (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀‘𝑢)”⟩⟩))
99	67, 69, 70, 98	syl3anc 1368	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐(𝑇‘𝑓)𝑢) = (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀‘𝑢)”⟩⟩))
100		splval 14104	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ 𝑊 ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑐 ∈ (0...(♯‘𝑓)) ∧ ⟨“𝑢(𝑀‘𝑢)”⟩ ∈ Word (𝐼 × 2o))) → (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀‘𝑢)”⟩⟩) = (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
101	67, 69, 69, 83, 100	syl13anc 1369	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀‘𝑢)”⟩⟩) = (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
102	99, 101	eqtrd 2833	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐(𝑇‘𝑓)𝑢) = (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
103	102	oveq2d 7151	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) = (𝐴 ++ (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
104	94, 97, 103	3eqtr4rd 2844	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
105	104	oveq1d 7150	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) = ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵))
106		lencl 13876	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ Word (𝐼 × 2o) → (♯‘𝐴) ∈ ℕ0)
107	74, 106	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐴) ∈ ℕ0)
108		nn0uz 12268	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ0 = (ℤ≥‘0)
109	107, 108	eleqtrdi 2900	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐴) ∈ (ℤ≥‘0))
110		elfznn0 12995	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ (0...(♯‘𝑓)) → 𝑐 ∈ ℕ0)
111	110	ad2antrl 727	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑐 ∈ ℕ0)
112		uzaddcl 12292	. . . . . . . . . . . . . . . . 17 ⊢ (((♯‘𝐴) ∈ (ℤ≥‘0) ∧ 𝑐 ∈ ℕ0) → ((♯‘𝐴) + 𝑐) ∈ (ℤ≥‘0))
113	109, 111, 112	syl2anc 587	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) ∈ (ℤ≥‘0))
114	42	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o))
115		ccatlen 13918	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → (♯‘((𝐴 ++ 𝑓) ++ 𝐵)) = ((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵)))
116	114, 88, 115	syl2anc 587	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘((𝐴 ++ 𝑓) ++ 𝐵)) = ((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵)))
117		ccatlen 13918	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ 𝑓 ∈ Word (𝐼 × 2o)) → (♯‘(𝐴 ++ 𝑓)) = ((♯‘𝐴) + (♯‘𝑓)))
118	74, 75, 117	syl2anc 587	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘(𝐴 ++ 𝑓)) = ((♯‘𝐴) + (♯‘𝑓)))
119		elfzuz3 12899	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 ∈ (0...(♯‘𝑓)) → (♯‘𝑓) ∈ (ℤ≥‘𝑐))
120	119	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ (ℤ≥‘𝑐))
121	107	nn0zd 12073	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐴) ∈ ℤ)
122		eluzadd 12261	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((♯‘𝑓) ∈ (ℤ≥‘𝑐) ∧ (♯‘𝐴) ∈ ℤ) → ((♯‘𝑓) + (♯‘𝐴)) ∈ (ℤ≥‘(𝑐 + (♯‘𝐴))))
123	120, 121, 122	syl2anc 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝑓) + (♯‘𝐴)) ∈ (ℤ≥‘(𝑐 + (♯‘𝐴))))
124		lencl 13876	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∈ Word (𝐼 × 2o) → (♯‘𝑓) ∈ ℕ0)
125	75, 124	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ ℕ0)
126	125	nn0cnd 11945	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ ℂ)
127	107	nn0cnd 11945	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐴) ∈ ℂ)
128	126, 127	addcomd 10831	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝑓) + (♯‘𝐴)) = ((♯‘𝐴) + (♯‘𝑓)))
129	111	nn0cnd 11945	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑐 ∈ ℂ)
130	129, 127	addcomd 10831	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐 + (♯‘𝐴)) = ((♯‘𝐴) + 𝑐))
131	130	fveq2d 6649	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (ℤ≥‘(𝑐 + (♯‘𝐴))) = (ℤ≥‘((♯‘𝐴) + 𝑐)))
132	123, 128, 131	3eltr3d 2904	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + (♯‘𝑓)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)))
133	118, 132	eqeltrd 2890	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘(𝐴 ++ 𝑓)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)))
134		lencl 13876	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ Word (𝐼 × 2o) → (♯‘𝐵) ∈ ℕ0)
135	88, 134	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐵) ∈ ℕ0)
136		uzaddcl 12292	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘(𝐴 ++ 𝑓)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)) ∧ (♯‘𝐵) ∈ ℕ0) → ((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)))
137	133, 135, 136	syl2anc 587	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)))
138	116, 137	eqeltrd 2890	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘((𝐴 ++ 𝑓) ++ 𝐵)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐)))
139		elfzuzb 12896	. . . . . . . . . . . . . . . 16 ⊢ (((♯‘𝐴) + 𝑐) ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) ↔ (((♯‘𝐴) + 𝑐) ∈ (ℤ≥‘0) ∧ (♯‘((𝐴 ++ 𝑓) ++ 𝐵)) ∈ (ℤ≥‘((♯‘𝐴) + 𝑐))))
140	113, 138, 139	sylanbrc 586	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))))
141	1, 2, 3, 4	efgtval 18841	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 ∧ ((♯‘𝐴) + 𝑐) ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) ∧ 𝑢 ∈ (𝐼 × 2o)) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨((♯‘𝐴) + 𝑐), ((♯‘𝐴) + 𝑐), ⟨“𝑢(𝑀‘𝑢)”⟩⟩))
142	72, 140, 70, 141	syl3anc 1368	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨((♯‘𝐴) + 𝑐), ((♯‘𝐴) + 𝑐), ⟨“𝑢(𝑀‘𝑢)”⟩⟩))
143		wrd0 13882	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ Word (𝐼 × 2o)
144	143	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ∅ ∈ Word (𝐼 × 2o))
145		ccatcl 13917	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵) ∈ Word (𝐼 × 2o))
146	87, 88, 145	syl2anc 587	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵) ∈ Word (𝐼 × 2o))
147		ccatrid 13932	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) = (𝐴 ++ (𝑓 prefix 𝑐)))
148	79, 147	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) = (𝐴 ++ (𝑓 prefix 𝑐)))
149	148	oveq1d 7150	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)) = ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
150		ccatass 13933	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o) ∧ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
151	79, 87, 88, 150	syl3anc 1368	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
152		ccatass 13933	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o) ∧ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o)) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
153	74, 77, 87, 152	syl3anc 1368	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
154	125, 108	eleqtrdi 2900	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ (ℤ≥‘0))
155		eluzfz2 12910	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝑓) ∈ (ℤ≥‘0) → (♯‘𝑓) ∈ (0...(♯‘𝑓)))
156	154, 155	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ (0...(♯‘𝑓)))
157		ccatpfx 14054	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 ∈ Word (𝐼 × 2o) ∧ 𝑐 ∈ (0...(♯‘𝑓)) ∧ (♯‘𝑓) ∈ (0...(♯‘𝑓))) → ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝑓 prefix (♯‘𝑓)))
158	75, 69, 156, 157	syl3anc 1368	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝑓 prefix (♯‘𝑓)))
159		pfxid 14037	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ Word (𝐼 × 2o) → (𝑓 prefix (♯‘𝑓)) = 𝑓)
160	75, 159	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑓 prefix (♯‘𝑓)) = 𝑓)
161	158, 160	eqtrd 2833	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = 𝑓)
162	161	oveq2d 7151	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))) = (𝐴 ++ 𝑓))
163	153, 162	eqtrd 2833	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ 𝑓))
164	163	oveq1d 7150	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = ((𝐴 ++ 𝑓) ++ 𝐵))
165	149, 151, 164	3eqtr2rd 2840	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ 𝑓) ++ 𝐵) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
166		ccatlen 13918	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o)) → (♯‘(𝐴 ++ (𝑓 prefix 𝑐))) = ((♯‘𝐴) + (♯‘(𝑓 prefix 𝑐))))
167	74, 77, 166	syl2anc 587	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘(𝐴 ++ (𝑓 prefix 𝑐))) = ((♯‘𝐴) + (♯‘(𝑓 prefix 𝑐))))
168		pfxlen 14036	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ Word (𝐼 × 2o) ∧ 𝑐 ∈ (0...(♯‘𝑓))) → (♯‘(𝑓 prefix 𝑐)) = 𝑐)
169	75, 69, 168	syl2anc 587	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘(𝑓 prefix 𝑐)) = 𝑐)
170	169	oveq2d 7151	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + (♯‘(𝑓 prefix 𝑐))) = ((♯‘𝐴) + 𝑐))
171	167, 170	eqtr2d 2834	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) = (♯‘(𝐴 ++ (𝑓 prefix 𝑐))))
172		hash0 13724	. . . . . . . . . . . . . . . . 17 ⊢ (♯‘∅) = 0
173	172	oveq2i 7146	. . . . . . . . . . . . . . . 16 ⊢ (((♯‘𝐴) + 𝑐) + (♯‘∅)) = (((♯‘𝐴) + 𝑐) + 0)
174	107, 111	nn0addcld 11947	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) ∈ ℕ0)
175	174	nn0cnd 11945	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) ∈ ℂ)
176	175	addid1d 10829	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((♯‘𝐴) + 𝑐) + 0) = ((♯‘𝐴) + 𝑐))
177	173, 176	syl5req 2846	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) = (((♯‘𝐴) + 𝑐) + (♯‘∅)))
178	79, 144, 146, 83, 165, 171, 177	splval2 14110	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨((♯‘𝐴) + 𝑐), ((♯‘𝐴) + 𝑐), ⟨“𝑢(𝑀‘𝑢)”⟩⟩) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
179	142, 178	eqtrd 2833	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀‘𝑢)”⟩) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
180	90, 105, 179	3eqtr4d 2843	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) = (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢))
181	1, 2, 3, 4	efgtf 18840	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 → ((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) = (𝑎 ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))), 𝑏 ∈ (𝐼 × 2o) ↦ (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀‘𝑏)”⟩⟩)) ∧ (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o))⟶𝑊))
182	181	simprd 499	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o))⟶𝑊)
183		ffn 6487	. . . . . . . . . . . . . 14 ⊢ ((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o))⟶𝑊 → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o)))
184	72, 182, 183	3syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o)))
185		fnovrn 7303	. . . . . . . . . . . . 13 ⊢ (((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o)) ∧ ((♯‘𝐴) + 𝑐) ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) ∧ 𝑢 ∈ (𝐼 × 2o)) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)))
186	184, 140, 70, 185	syl3anc 1368	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)))
187	180, 186	eqeltrd 2890	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)))
188	1, 2, 3, 4	efgi2 18843	. . . . . . . . . . 11 ⊢ ((((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 ∧ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵))
189	72, 187, 188	syl2anc 587	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵))
190	1, 2, 3, 4, 9, 10, 6	efgcpbllema 18872	. . . . . . . . . 10 ⊢ (𝑓𝐿(𝑐(𝑇‘𝑓)𝑢) ↔ (𝑓 ∈ 𝑊 ∧ (𝑐(𝑇‘𝑓)𝑢) ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵)))
191	67, 71, 189, 190	syl3anbrc 1340	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑓𝐿(𝑐(𝑇‘𝑓)𝑢))
192		vex 3444	. . . . . . . . . . 11 ⊢ 𝑎 ∈ V
193		vex 3444	. . . . . . . . . . 11 ⊢ 𝑓 ∈ V
194	192, 193	elec 8316	. . . . . . . . . 10 ⊢ (𝑎 ∈ [𝑓]𝐿 ↔ 𝑓𝐿𝑎)
195		breq2 5034	. . . . . . . . . 10 ⊢ (𝑎 = (𝑐(𝑇‘𝑓)𝑢) → (𝑓𝐿𝑎 ↔ 𝑓𝐿(𝑐(𝑇‘𝑓)𝑢)))
196	194, 195	syl5bb 286	. . . . . . . . 9 ⊢ (𝑎 = (𝑐(𝑇‘𝑓)𝑢) → (𝑎 ∈ [𝑓]𝐿 ↔ 𝑓𝐿(𝑐(𝑇‘𝑓)𝑢)))
197	191, 196	syl5ibrcom 250	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑎 = (𝑐(𝑇‘𝑓)𝑢) → 𝑎 ∈ [𝑓]𝐿))
198	197	rexlimdvva 3253	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (∃𝑐 ∈ (0...(♯‘𝑓))∃𝑢 ∈ (𝐼 × 2o)𝑎 = (𝑐(𝑇‘𝑓)𝑢) → 𝑎 ∈ [𝑓]𝐿))
199	66, 198	sylbid 243	. . . . . 6 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝑎 ∈ ran (𝑇‘𝑓) → 𝑎 ∈ [𝑓]𝐿))
200	199	ssrdv 3921	. . . . 5 ⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)
201	200	ralrimiva 3149	. . . 4 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)
202	1	fvexi 6659	. . . . . 6 ⊢ 𝑊 ∈ V
203		erex 8296	. . . . . 6 ⊢ (𝐿 Er 𝑊 → (𝑊 ∈ V → 𝐿 ∈ V))
204	60, 202, 203	mpisyl 21	. . . . 5 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐿 ∈ V)
205		ereq1 8279	. . . . . . 7 ⊢ (𝑟 = 𝐿 → (𝑟 Er 𝑊 ↔ 𝐿 Er 𝑊))
206		eceq2 8312	. . . . . . . . 9 ⊢ (𝑟 = 𝐿 → [𝑓]𝑟 = [𝑓]𝐿)
207	206	sseq2d 3947	. . . . . . . 8 ⊢ (𝑟 = 𝐿 → (ran (𝑇‘𝑓) ⊆ [𝑓]𝑟 ↔ ran (𝑇‘𝑓) ⊆ [𝑓]𝐿))
208	207	ralbidv 3162	. . . . . . 7 ⊢ (𝑟 = 𝐿 → (∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟 ↔ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿))
209	205, 208	anbi12d 633	. . . . . 6 ⊢ (𝑟 = 𝐿 → ((𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟) ↔ (𝐿 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)))
210	209	elabg 3614	. . . . 5 ⊢ (𝐿 ∈ V → (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ↔ (𝐿 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)))
211	204, 210	syl 17	. . . 4 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ↔ (𝐿 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)))
212	60, 201, 211	mpbir2and 712	. . 3 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)})
213		intss1 4853	. . 3 ⊢ (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} → ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ⊆ 𝐿)
214	212, 213	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ⊆ 𝐿)
215	5, 214	eqsstrid 3963	1 ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ∼ ⊆ 𝐿)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  {cab 2776  ∀wral 3106  ∃wrex 3107  {crab 3110  Vcvv 3441   ∖ cdif 3878   ⊆ wss 3881  ∅c0 4243  {csn 4525  {cpr 4527  ⟨cop 4531  ⟨cotp 4533  ∩ cint 4838  ∪ ciun 4881   class class class wbr 5030  {copab 5092   ↦ cmpt 5110   I cid 5424   × cxp 5517  ran crn 5520  Rel wrel 5524   Fn wfn 6319  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135   ∈ cmpo 7137  1_oc1o 8078  2_oc2o 8079   Er wer 8269  [cec 8270  0cc0 10526  1c1 10527   + caddc 10529   − cmin 10859  ℕ₀cn0 11885  ℤcz 11969  ℤ_≥cuz 12231  ...cfz 12885  ..^cfzo 13028  ♯chash 13686  Word cword 13857   ++ cconcat 13913   substr csubstr 13993   prefix cpfx 14023   splice csplice 14102  ⟨“cs2 14194   ~_FG cefg 18824

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-ot 4534  df-uni 4801  df-int 4839  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-2o 8086  df-oadd 8089  df-er 8272  df-ec 8274  df-map 8391  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-card 9352  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11626  df-n0 11886  df-z 11970  df-uz 12232  df-fz 12886  df-fzo 13029  df-hash 13687  df-word 13858  df-concat 13914  df-s1 13941  df-substr 13994  df-pfx 14024  df-splice 14103  df-s2 14201  df-efg 18827

This theorem is referenced by:  efgcpbl  18874