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

Metamath Proof Explorer

Theorem ccatpfx

Description: Concatenating a prefix with an adjacent subword makes a longer prefix. (Contributed by AV, 7-May-2020)

Ref Expression
Assertion ccatpfx ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) = ( 𝑆 prefix 𝑍 ) )

Proof

Step Hyp Ref Expression
1 pfxcl ⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 prefix 𝑌 ) ∈ Word 𝐴 )
2 swrdcl ⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ∈ Word 𝐴 )
3 ccatcl ⊢ ( ( ( 𝑆 prefix 𝑌 ) ∈ Word 𝐴 ∧ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ∈ Word 𝐴 ) → ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ∈ Word 𝐴 )
4 1 2 3 syl2anc ⊢ ( 𝑆 ∈ Word 𝐴 → ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ∈ Word 𝐴 )
5 wrdfn ⊢ ( ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ∈ Word 𝐴 → ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) Fn ( 0 ..^ ( ♯ ‘ ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) )
6 4 5 syl ⊢ ( 𝑆 ∈ Word 𝐴 → ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) Fn ( 0 ..^ ( ♯ ‘ ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) )
7 6 adantr ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) Fn ( 0 ..^ ( ♯ ‘ ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) )
8 ccatlen ⊢ ( ( ( 𝑆 prefix 𝑌 ) ∈ Word 𝐴 ∧ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ∈ Word 𝐴 ) → ( ♯ ‘ ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) = ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) )
9 1 2 8 syl2anc ⊢ ( 𝑆 ∈ Word 𝐴 → ( ♯ ‘ ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) = ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) )
10 9 adantr ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ♯ ‘ ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) = ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) )
11 fzass4 ⊢ ( ( 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑍 ∈ ( 𝑌 ... ( ♯ ‘ 𝑆 ) ) ) ↔ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) )
12 11 biimpri ⊢ ( ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑍 ∈ ( 𝑌 ... ( ♯ ‘ 𝑆 ) ) ) )
13 12 simpld ⊢ ( ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
14 pfxlen ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) = 𝑌 )
15 13 14 sylan2 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) = 𝑌 )
16 swrdlen ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) = ( 𝑍 − 𝑌 ) )
17 16 3expb ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) = ( 𝑍 − 𝑌 ) )
18 15 17 oveq12d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) = ( 𝑌 + ( 𝑍 − 𝑌 ) ) )
19 elfzelz ⊢ ( 𝑌 ∈ ( 0 ... 𝑍 ) → 𝑌 ∈ ℤ )
20 19 zcnd ⊢ ( 𝑌 ∈ ( 0 ... 𝑍 ) → 𝑌 ∈ ℂ )
21 elfzelz ⊢ ( 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) → 𝑍 ∈ ℤ )
22 21 zcnd ⊢ ( 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) → 𝑍 ∈ ℂ )
23 pncan3 ⊢ ( ( 𝑌 ∈ ℂ ∧ 𝑍 ∈ ℂ ) → ( 𝑌 + ( 𝑍 − 𝑌 ) ) = 𝑍 )
24 20 22 23 syl2an ⊢ ( ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑌 + ( 𝑍 − 𝑌 ) ) = 𝑍 )
25 24 adantl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑌 + ( 𝑍 − 𝑌 ) ) = 𝑍 )
26 10 18 25 3eqtrd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ♯ ‘ ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) = 𝑍 )
27 26 oveq2d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 0 ..^ ( ♯ ‘ ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) = ( 0 ..^ 𝑍 ) )
28 27 fneq2d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) Fn ( 0 ..^ ( ♯ ‘ ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) ↔ ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) Fn ( 0 ..^ 𝑍 ) ) )
29 7 28 mpbid ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) Fn ( 0 ..^ 𝑍 ) )
30 pfxfn ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 prefix 𝑍 ) Fn ( 0 ..^ 𝑍 ) )
31 30 adantrl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑆 prefix 𝑍 ) Fn ( 0 ..^ 𝑍 ) )
32 id ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑍 ) → 𝑥 ∈ ( 0 ..^ 𝑍 ) )
33 19 ad2antrl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑌 ∈ ℤ )
34 fzospliti ⊢ ( ( 𝑥 ∈ ( 0 ..^ 𝑍 ) ∧ 𝑌 ∈ ℤ ) → ( 𝑥 ∈ ( 0 ..^ 𝑌 ) ∨ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) )
35 32 33 34 syl2anr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑍 ) ) → ( 𝑥 ∈ ( 0 ..^ 𝑌 ) ∨ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) )
36 1 ad2antrr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑌 ) ) → ( 𝑆 prefix 𝑌 ) ∈ Word 𝐴 )
37 2 ad2antrr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑌 ) ) → ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ∈ Word 𝐴 )
38 15 oveq2d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 0 ..^ ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) = ( 0 ..^ 𝑌 ) )
39 38 eleq2d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) ↔ 𝑥 ∈ ( 0 ..^ 𝑌 ) ) )
40 39 biimpar ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑌 ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) )
41 ccatval1 ⊢ ( ( ( 𝑆 prefix 𝑌 ) ∈ Word 𝐴 ∧ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) ) → ( ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( ( 𝑆 prefix 𝑌 ) ‘ 𝑥 ) )
42 36 37 40 41 syl3anc ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑌 ) ) → ( ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( ( 𝑆 prefix 𝑌 ) ‘ 𝑥 ) )
43 simpl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑆 ∈ Word 𝐴 )
44 13 adantl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
45 id ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑌 ) → 𝑥 ∈ ( 0 ..^ 𝑌 ) )
46 pfxfv ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑌 ) ) → ( ( 𝑆 prefix 𝑌 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
47 43 44 45 46 syl2an3an ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑌 ) ) → ( ( 𝑆 prefix 𝑌 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
48 42 47 eqtrd ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑌 ) ) → ( ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
49 1 ad2antrr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( 𝑆 prefix 𝑌 ) ∈ Word 𝐴 )
50 2 ad2antrr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ∈ Word 𝐴 )
51 18 25 eqtrd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) = 𝑍 )
52 15 51 oveq12d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ..^ ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) = ( 𝑌 ..^ 𝑍 ) )
53 52 eleq2d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑥 ∈ ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ..^ ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) ↔ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) )
54 53 biimpar ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → 𝑥 ∈ ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ..^ ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) )
55 ccatval2 ⊢ ( ( ( 𝑆 prefix 𝑌 ) ∈ Word 𝐴 ∧ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ∈ Word 𝐴 ∧ 𝑥 ∈ ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ..^ ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) ) → ( ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) ) )
56 49 50 54 55 syl3anc ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) ) )
57 id ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) )
58 57 3expb ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) )
59 15 oveq2d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) = ( 𝑥 − 𝑌 ) )
60 59 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) = ( 𝑥 − 𝑌 ) )
61 id ⊢ ( 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) → 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) )
62 fzosubel ⊢ ( ( 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ∧ 𝑌 ∈ ℤ ) → ( 𝑥 − 𝑌 ) ∈ ( ( 𝑌 − 𝑌 ) ..^ ( 𝑍 − 𝑌 ) ) )
63 61 33 62 syl2anr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( 𝑥 − 𝑌 ) ∈ ( ( 𝑌 − 𝑌 ) ..^ ( 𝑍 − 𝑌 ) ) )
64 20 subidd ⊢ ( 𝑌 ∈ ( 0 ... 𝑍 ) → ( 𝑌 − 𝑌 ) = 0 )
65 64 oveq1d ⊢ ( 𝑌 ∈ ( 0 ... 𝑍 ) → ( ( 𝑌 − 𝑌 ) ..^ ( 𝑍 − 𝑌 ) ) = ( 0 ..^ ( 𝑍 − 𝑌 ) ) )
66 65 eleq2d ⊢ ( 𝑌 ∈ ( 0 ... 𝑍 ) → ( ( 𝑥 − 𝑌 ) ∈ ( ( 𝑌 − 𝑌 ) ..^ ( 𝑍 − 𝑌 ) ) ↔ ( 𝑥 − 𝑌 ) ∈ ( 0 ..^ ( 𝑍 − 𝑌 ) ) ) )
67 66 ad2antrl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( 𝑥 − 𝑌 ) ∈ ( ( 𝑌 − 𝑌 ) ..^ ( 𝑍 − 𝑌 ) ) ↔ ( 𝑥 − 𝑌 ) ∈ ( 0 ..^ ( 𝑍 − 𝑌 ) ) ) )
68 67 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( ( 𝑥 − 𝑌 ) ∈ ( ( 𝑌 − 𝑌 ) ..^ ( 𝑍 − 𝑌 ) ) ↔ ( 𝑥 − 𝑌 ) ∈ ( 0 ..^ ( 𝑍 − 𝑌 ) ) ) )
69 63 68 mpbid ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( 𝑥 − 𝑌 ) ∈ ( 0 ..^ ( 𝑍 − 𝑌 ) ) )
70 60 69 eqeltrd ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) ∈ ( 0 ..^ ( 𝑍 − 𝑌 ) ) )
71 swrdfv ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ∧ ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) ∈ ( 0 ..^ ( 𝑍 − 𝑌 ) ) ) → ( ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) ) = ( 𝑆 ‘ ( ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) + 𝑌 ) ) )
72 58 70 71 syl2an2r ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) ) = ( 𝑆 ‘ ( ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) + 𝑌 ) ) )
73 59 oveq1d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) + 𝑌 ) = ( ( 𝑥 − 𝑌 ) + 𝑌 ) )
74 73 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) + 𝑌 ) = ( ( 𝑥 − 𝑌 ) + 𝑌 ) )
75 elfzoelz ⊢ ( 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) → 𝑥 ∈ ℤ )
76 75 zcnd ⊢ ( 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) → 𝑥 ∈ ℂ )
77 20 ad2antrl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑌 ∈ ℂ )
78 npcan ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑌 ∈ ℂ ) → ( ( 𝑥 − 𝑌 ) + 𝑌 ) = 𝑥 )
79 76 77 78 syl2anr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( ( 𝑥 − 𝑌 ) + 𝑌 ) = 𝑥 )
80 74 79 eqtrd ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) + 𝑌 ) = 𝑥 )
81 80 fveq2d ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( 𝑆 ‘ ( ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) + 𝑌 ) ) = ( 𝑆 ‘ 𝑥 ) )
82 56 72 81 3eqtrd ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
83 48 82 jaodan ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ ( 𝑥 ∈ ( 0 ..^ 𝑌 ) ∨ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) ) → ( ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
84 35 83 syldan ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑍 ) ) → ( ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
85 pfxfv ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑍 ) ) → ( ( 𝑆 prefix 𝑍 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
86 85 3expa ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑍 ) ) → ( ( 𝑆 prefix 𝑍 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
87 86 adantlrl ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑍 ) ) → ( ( 𝑆 prefix 𝑍 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
88 84 87 eqtr4d ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑍 ) ) → ( ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( ( 𝑆 prefix 𝑍 ) ‘ 𝑥 ) )
89 29 31 88 eqfnfvd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) = ( 𝑆 prefix 𝑍 ) )
90 89 3impb ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) = ( 𝑆 prefix 𝑍 ) )