This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pfxccatin12

Description: The subword of a concatenation of two words within both of the concatenated words. (Contributed by Alexander van der Vekens, 5-Apr-2018) (Revised by AV, 9-May-2020)

Ref Expression
Hypothesis swrdccatin2.l ⊢ 𝐿 = ( ♯ ‘ 𝐴 )
Assertion pfxccatin12 ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 swrdccatin2.l ⊢ 𝐿 = ( ♯ ‘ 𝐴 )
2 1 pfxccatin12lem2c ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) ) ) )
3 swrdvalfn ⊢ ( ( ( 𝐴 ++ 𝐵 ) ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) Fn ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
4 2 3 syl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) Fn ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
5 swrdcl ⊢ ( 𝐴 ∈ Word 𝑉 → ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ∈ Word 𝑉 )
6 pfxcl ⊢ ( 𝐵 ∈ Word 𝑉 → ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ∈ Word 𝑉 )
7 ccatvalfn ⊢ ( ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ∈ Word 𝑉 ∧ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ∈ Word 𝑉 ) → ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) Fn ( 0 ..^ ( ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) + ( ♯ ‘ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) )
8 5 6 7 syl2an ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) Fn ( 0 ..^ ( ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) + ( ♯ ‘ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) )
9 8 adantr ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) Fn ( 0 ..^ ( ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) + ( ♯ ‘ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) )
10 simpll ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → 𝐴 ∈ Word 𝑉 )
11 simprl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → 𝑀 ∈ ( 0 ... 𝐿 ) )
12 lencl ⊢ ( 𝐴 ∈ Word 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
13 nn0fz0 ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝐴 ) ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
14 12 13 sylib ⊢ ( 𝐴 ∈ Word 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
15 1 14 eqeltrid ⊢ ( 𝐴 ∈ Word 𝑉 → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
16 15 ad2antrr ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
17 swrdlen ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) → ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) = ( 𝐿 − 𝑀 ) )
18 10 11 16 17 syl3anc ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) = ( 𝐿 − 𝑀 ) )
19 lencl ⊢ ( 𝐵 ∈ Word 𝑉 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
20 19 nn0zd ⊢ ( 𝐵 ∈ Word 𝑉 → ( ♯ ‘ 𝐵 ) ∈ ℤ )
21 elfzmlbp ⊢ ( ( ( ♯ ‘ 𝐵 ) ∈ ℤ ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝑁 − 𝐿 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) )
22 20 21 sylan ⊢ ( ( 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝑁 − 𝐿 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) )
23 pfxlen ⊢ ( ( 𝐵 ∈ Word 𝑉 ∧ ( 𝑁 − 𝐿 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) ) → ( ♯ ‘ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) = ( 𝑁 − 𝐿 ) )
24 22 23 syldan ⊢ ( ( 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ♯ ‘ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) = ( 𝑁 − 𝐿 ) )
25 24 ad2ant2l ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ♯ ‘ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) = ( 𝑁 − 𝐿 ) )
26 18 25 oveq12d ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) + ( ♯ ‘ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) = ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) )
27 elfz2nn0 ⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) )
28 nn0cn ⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℂ )
29 28 ad2antll ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ) → 𝐿 ∈ ℂ )
30 nn0cn ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℂ )
31 30 ad2antrl ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ) → 𝑀 ∈ ℂ )
32 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
33 32 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ) → 𝑁 ∈ ℂ )
34 29 31 33 3jca ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) )
35 34 ex ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ) )
36 elfzelz ⊢ ( 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → 𝑁 ∈ ℤ )
37 35 36 syl11 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( 𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ) )
38 37 3adant3 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → ( 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( 𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ) )
39 27 38 sylbi ⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) → ( 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( 𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ) )
40 39 imp ⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) )
41 npncan3 ⊢ ( ( 𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) = ( 𝑁 − 𝑀 ) )
42 40 41 syl ⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) = ( 𝑁 − 𝑀 ) )
43 42 adantl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) = ( 𝑁 − 𝑀 ) )
44 26 43 eqtr2d ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( 𝑁 − 𝑀 ) = ( ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) + ( ♯ ‘ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) )
45 44 oveq2d ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( 0 ..^ ( 𝑁 − 𝑀 ) ) = ( 0 ..^ ( ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) + ( ♯ ‘ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) )
46 45 fneq2d ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) Fn ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↔ ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) Fn ( 0 ..^ ( ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) + ( ♯ ‘ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) ) )
47 9 46 mpbird ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) Fn ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
48 simprl ⊢ ( ( 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) )
49 simpr ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
50 49 anim2i ⊢ ( ( 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → ( 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) )
51 50 ancomd ⊢ ( ( 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → ( 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) )
52 1 pfxccatin12lem3 ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → ( ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑘 ) = ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ‘ 𝑘 ) ) )
53 48 51 52 sylc ⊢ ( ( 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → ( ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑘 ) = ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ‘ 𝑘 ) )
54 5 6 anim12i ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ∈ Word 𝑉 ∧ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ∈ Word 𝑉 ) )
55 54 adantr ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ∈ Word 𝑉 ∧ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ∈ Word 𝑉 ) )
56 55 ad2antrl ⊢ ( ( 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ∈ Word 𝑉 ∧ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ∈ Word 𝑉 ) )
57 simpl ⊢ ( ( 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) )
58 18 oveq2d ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( 0 ..^ ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ) = ( 0 ..^ ( 𝐿 − 𝑀 ) ) )
59 58 ad2antrl ⊢ ( ( 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → ( 0 ..^ ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ) = ( 0 ..^ ( 𝐿 − 𝑀 ) ) )
60 57 59 eleqtrrd ⊢ ( ( 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ) )
61 df-3an ⊢ ( ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ∈ Word 𝑉 ∧ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ∈ Word 𝑉 ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ) ) ↔ ( ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ∈ Word 𝑉 ∧ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ∈ Word 𝑉 ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ) ) )
62 56 60 61 sylanbrc ⊢ ( ( 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ∈ Word 𝑉 ∧ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ∈ Word 𝑉 ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ) ) )
63 ccatval1 ⊢ ( ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ∈ Word 𝑉 ∧ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ∈ Word 𝑉 ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ) ) → ( ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ‘ 𝑘 ) = ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ‘ 𝑘 ) )
64 62 63 syl ⊢ ( ( 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → ( ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ‘ 𝑘 ) = ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ‘ 𝑘 ) )
65 53 64 eqtr4d ⊢ ( ( 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → ( ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑘 ) = ( ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ‘ 𝑘 ) )
66 simprl ⊢ ( ( ¬ 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) )
67 49 anim2i ⊢ ( ( ¬ 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → ( ¬ 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) )
68 67 ancomd ⊢ ( ( ¬ 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → ( 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) )
69 1 pfxccatin12lem2 ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → ( ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑘 ) = ( ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ‘ ( 𝑘 − ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ) ) ) )
70 66 68 69 sylc ⊢ ( ( ¬ 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → ( ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑘 ) = ( ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ‘ ( 𝑘 − ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ) ) )
71 55 ad2antrl ⊢ ( ( ¬ 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ∈ Word 𝑉 ∧ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ∈ Word 𝑉 ) )
72 elfzuz ⊢ ( 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) )
73 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) → 𝑁 ∈ ℤ )
74 id ⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) → ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) )
75 74 3expia ⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 ∈ ℤ → ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) ) )
76 75 ancoms ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑁 ∈ ℤ → ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) ) )
77 76 3adant3 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → ( 𝑁 ∈ ℤ → ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) ) )
78 27 77 sylbi ⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) → ( 𝑁 ∈ ℤ → ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) ) )
79 73 78 syl5com ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) → ( 𝑀 ∈ ( 0 ... 𝐿 ) → ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) ) )
80 72 79 syl ⊢ ( 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( 𝑀 ∈ ( 0 ... 𝐿 ) → ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) ) )
81 80 impcom ⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) )
82 81 adantl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) )
83 82 ad2antrl ⊢ ( ( ¬ 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) )
84 pfxccatin12lem4 ⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → 𝑘 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) ) )
85 83 68 84 sylc ⊢ ( ( ¬ 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → 𝑘 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) )
86 18 26 oveq12d ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ..^ ( ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) + ( ♯ ‘ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) = ( ( 𝐿 − 𝑀 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) )
87 86 ad2antrl ⊢ ( ( ¬ 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → ( ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ..^ ( ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) + ( ♯ ‘ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) = ( ( 𝐿 − 𝑀 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) )
88 85 87 eleqtrrd ⊢ ( ( ¬ 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → 𝑘 ∈ ( ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ..^ ( ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) + ( ♯ ‘ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) )
89 df-3an ⊢ ( ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ∈ Word 𝑉 ∧ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ∈ Word 𝑉 ∧ 𝑘 ∈ ( ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ..^ ( ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) + ( ♯ ‘ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) ) ↔ ( ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ∈ Word 𝑉 ∧ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ∈ Word 𝑉 ) ∧ 𝑘 ∈ ( ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ..^ ( ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) + ( ♯ ‘ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) ) )
90 71 88 89 sylanbrc ⊢ ( ( ¬ 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ∈ Word 𝑉 ∧ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ∈ Word 𝑉 ∧ 𝑘 ∈ ( ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ..^ ( ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) + ( ♯ ‘ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) ) )
91 ccatval2 ⊢ ( ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ∈ Word 𝑉 ∧ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ∈ Word 𝑉 ∧ 𝑘 ∈ ( ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ..^ ( ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) + ( ♯ ‘ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) ) → ( ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ‘ 𝑘 ) = ( ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ‘ ( 𝑘 − ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ) ) )
92 90 91 syl ⊢ ( ( ¬ 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → ( ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ‘ 𝑘 ) = ( ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ‘ ( 𝑘 − ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ) ) )
93 70 92 eqtr4d ⊢ ( ( ¬ 𝑘 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → ( ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑘 ) = ( ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ‘ 𝑘 ) )
94 65 93 pm2.61ian ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑘 ) = ( ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ‘ 𝑘 ) )
95 4 47 94 eqfnfvd ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) )
96 95 ex ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) )