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

Metamath Proof Explorer

Theorem ccatswrd

Description: Joining two adjacent subwords makes a longer subword. (Contributed by Stefan O'Rear, 20-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 swrdcl ⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ∈ Word 𝐴 )
2 1 adantr ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ∈ Word 𝐴 )
3 swrdcl ⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ∈ Word 𝐴 )
4 3 adantr ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ∈ Word 𝐴 )
5 ccatcl ⊢ ( ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ∈ Word 𝐴 ∧ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ∈ Word 𝐴 ) → ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ∈ Word 𝐴 )
6 2 4 5 syl2anc ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ∈ Word 𝐴 )
7 wrdfn ⊢ ( ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ∈ Word 𝐴 → ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) Fn ( 0 ..^ ( ♯ ‘ ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) )
8 6 7 syl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) Fn ( 0 ..^ ( ♯ ‘ ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) )
9 ccatlen ⊢ ( ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ∈ Word 𝐴 ∧ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ∈ Word 𝐴 ) → ( ♯ ‘ ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) = ( ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) )
10 2 4 9 syl2anc ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ♯ ‘ ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) = ( ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) )
11 simpl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑆 ∈ Word 𝐴 )
12 simpr1 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑋 ∈ ( 0 ... 𝑌 ) )
13 simpr2 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑌 ∈ ( 0 ... 𝑍 ) )
14 simpr3 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
15 fzass4 ⊢ ( ( 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑍 ∈ ( 𝑌 ... ( ♯ ‘ 𝑆 ) ) ) ↔ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) )
16 15 biimpri ⊢ ( ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑍 ∈ ( 𝑌 ... ( ♯ ‘ 𝑆 ) ) ) )
17 16 simpld ⊢ ( ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
18 13 14 17 syl2anc ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
19 swrdlen ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝑌 − 𝑋 ) )
20 11 12 18 19 syl3anc ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝑌 − 𝑋 ) )
21 swrdlen ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) = ( 𝑍 − 𝑌 ) )
22 21 3adant3r1 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) = ( 𝑍 − 𝑌 ) )
23 20 22 oveq12d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) = ( ( 𝑌 − 𝑋 ) + ( 𝑍 − 𝑌 ) ) )
24 13 elfzelzd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑌 ∈ ℤ )
25 24 zcnd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑌 ∈ ℂ )
26 12 elfzelzd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑋 ∈ ℤ )
27 26 zcnd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑋 ∈ ℂ )
28 14 elfzelzd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑍 ∈ ℤ )
29 28 zcnd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑍 ∈ ℂ )
30 25 27 29 npncan3d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( 𝑌 − 𝑋 ) + ( 𝑍 − 𝑌 ) ) = ( 𝑍 − 𝑋 ) )
31 10 23 30 3eqtrd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ♯ ‘ ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) = ( 𝑍 − 𝑋 ) )
32 31 oveq2d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 0 ..^ ( ♯ ‘ ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) = ( 0 ..^ ( 𝑍 − 𝑋 ) ) )
33 32 fneq2d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) Fn ( 0 ..^ ( ♯ ‘ ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) ↔ ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) Fn ( 0 ..^ ( 𝑍 − 𝑋 ) ) ) )
34 8 33 mpbid ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) Fn ( 0 ..^ ( 𝑍 − 𝑋 ) ) )
35 swrdcl ⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 substr ⟨ 𝑋 , 𝑍 ⟩ ) ∈ Word 𝐴 )
36 35 adantr ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑆 substr ⟨ 𝑋 , 𝑍 ⟩ ) ∈ Word 𝐴 )
37 wrdfn ⊢ ( ( 𝑆 substr ⟨ 𝑋 , 𝑍 ⟩ ) ∈ Word 𝐴 → ( 𝑆 substr ⟨ 𝑋 , 𝑍 ⟩ ) Fn ( 0 ..^ ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑍 ⟩ ) ) ) )
38 36 37 syl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑆 substr ⟨ 𝑋 , 𝑍 ⟩ ) Fn ( 0 ..^ ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑍 ⟩ ) ) ) )
39 fzass4 ⊢ ( ( 𝑋 ∈ ( 0 ... 𝑍 ) ∧ 𝑌 ∈ ( 𝑋 ... 𝑍 ) ) ↔ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ) )
40 39 biimpri ⊢ ( ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ) → ( 𝑋 ∈ ( 0 ... 𝑍 ) ∧ 𝑌 ∈ ( 𝑋 ... 𝑍 ) ) )
41 40 simpld ⊢ ( ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ) → 𝑋 ∈ ( 0 ... 𝑍 ) )
42 12 13 41 syl2anc ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑋 ∈ ( 0 ... 𝑍 ) )
43 swrdlen ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑋 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑍 ⟩ ) ) = ( 𝑍 − 𝑋 ) )
44 11 42 14 43 syl3anc ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑍 ⟩ ) ) = ( 𝑍 − 𝑋 ) )
45 44 oveq2d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 0 ..^ ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑍 ⟩ ) ) ) = ( 0 ..^ ( 𝑍 − 𝑋 ) ) )
46 45 fneq2d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( 𝑆 substr ⟨ 𝑋 , 𝑍 ⟩ ) Fn ( 0 ..^ ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑍 ⟩ ) ) ) ↔ ( 𝑆 substr ⟨ 𝑋 , 𝑍 ⟩ ) Fn ( 0 ..^ ( 𝑍 − 𝑋 ) ) ) )
47 38 46 mpbid ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑆 substr ⟨ 𝑋 , 𝑍 ⟩ ) Fn ( 0 ..^ ( 𝑍 − 𝑋 ) ) )
48 24 26 zsubcld ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑌 − 𝑋 ) ∈ ℤ )
49 48 anim1ci ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑍 − 𝑋 ) ) ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑍 − 𝑋 ) ) ∧ ( 𝑌 − 𝑋 ) ∈ ℤ ) )
50 fzospliti ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( 𝑍 − 𝑋 ) ) ∧ ( 𝑌 − 𝑋 ) ∈ ℤ ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑌 − 𝑋 ) ) ∨ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) )
51 49 50 syl ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑍 − 𝑋 ) ) ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑌 − 𝑋 ) ) ∨ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) )
52 1 ad2antrr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑌 − 𝑋 ) ) ) → ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ∈ Word 𝐴 )
53 3 ad2antrr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑌 − 𝑋 ) ) ) → ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ∈ Word 𝐴 )
54 20 oveq2d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 0 ..^ ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ) = ( 0 ..^ ( 𝑌 − 𝑋 ) ) )
55 54 eleq2d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ↔ 𝑥 ∈ ( 0 ..^ ( 𝑌 − 𝑋 ) ) ) )
56 55 biimpar ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑌 − 𝑋 ) ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ) )
57 ccatval1 ⊢ ( ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ∈ Word 𝐴 ∧ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ) → ( ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ‘ 𝑥 ) )
58 52 53 56 57 syl3anc ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑌 − 𝑋 ) ) ) → ( ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ‘ 𝑥 ) )
59 simpll ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑌 − 𝑋 ) ) ) → 𝑆 ∈ Word 𝐴 )
60 simplr1 ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑌 − 𝑋 ) ) ) → 𝑋 ∈ ( 0 ... 𝑌 ) )
61 18 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑌 − 𝑋 ) ) ) → 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
62 simpr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑌 − 𝑋 ) ) ) → 𝑥 ∈ ( 0 ..^ ( 𝑌 − 𝑋 ) ) )
63 swrdfv ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑌 − 𝑋 ) ) ) → ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) )
64 59 60 61 62 63 syl31anc ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑌 − 𝑋 ) ) ) → ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) )
65 58 64 eqtrd ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑌 − 𝑋 ) ) ) → ( ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) )
66 1 ad2antrr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) → ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ∈ Word 𝐴 )
67 3 ad2antrr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) → ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ∈ Word 𝐴 )
68 23 30 eqtrd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) = ( 𝑍 − 𝑋 ) )
69 20 68 oveq12d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ..^ ( ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) = ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) )
70 69 eleq2d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑥 ∈ ( ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ..^ ( ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) ↔ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) )
71 70 biimpar ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) → 𝑥 ∈ ( ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ..^ ( ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) )
72 ccatval2 ⊢ ( ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ∈ Word 𝐴 ∧ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ∈ Word 𝐴 ∧ 𝑥 ∈ ( ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ..^ ( ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) ) → ( ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ) )
73 66 67 71 72 syl3anc ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) → ( ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ) )
74 simpll ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) → 𝑆 ∈ Word 𝐴 )
75 simplr2 ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) → 𝑌 ∈ ( 0 ... 𝑍 ) )
76 simplr3 ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) → 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
77 20 oveq2d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑥 − ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ) = ( 𝑥 − ( 𝑌 − 𝑋 ) ) )
78 77 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) → ( 𝑥 − ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ) = ( 𝑥 − ( 𝑌 − 𝑋 ) ) )
79 30 oveq2d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( 𝑌 − 𝑋 ) ..^ ( ( 𝑌 − 𝑋 ) + ( 𝑍 − 𝑌 ) ) ) = ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) )
80 79 eleq2d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( ( 𝑌 − 𝑋 ) + ( 𝑍 − 𝑌 ) ) ) ↔ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) )
81 80 biimpar ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) → 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( ( 𝑌 − 𝑋 ) + ( 𝑍 − 𝑌 ) ) ) )
82 28 24 zsubcld ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑍 − 𝑌 ) ∈ ℤ )
83 82 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) → ( 𝑍 − 𝑌 ) ∈ ℤ )
84 fzosubel3 ⊢ ( ( 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( ( 𝑌 − 𝑋 ) + ( 𝑍 − 𝑌 ) ) ) ∧ ( 𝑍 − 𝑌 ) ∈ ℤ ) → ( 𝑥 − ( 𝑌 − 𝑋 ) ) ∈ ( 0 ..^ ( 𝑍 − 𝑌 ) ) )
85 81 83 84 syl2anc ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) → ( 𝑥 − ( 𝑌 − 𝑋 ) ) ∈ ( 0 ..^ ( 𝑍 − 𝑌 ) ) )
86 78 85 eqeltrd ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) → ( 𝑥 − ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ∈ ( 0 ..^ ( 𝑍 − 𝑌 ) ) )
87 swrdfv ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ∧ ( 𝑥 − ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ∈ ( 0 ..^ ( 𝑍 − 𝑌 ) ) ) → ( ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ) = ( 𝑆 ‘ ( ( 𝑥 − ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ) + 𝑌 ) ) )
88 74 75 76 86 87 syl31anc ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) → ( ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ) = ( 𝑆 ‘ ( ( 𝑥 − ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ) + 𝑌 ) ) )
89 77 oveq1d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( 𝑥 − ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ) + 𝑌 ) = ( ( 𝑥 − ( 𝑌 − 𝑋 ) ) + 𝑌 ) )
90 89 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) → ( ( 𝑥 − ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ) + 𝑌 ) = ( ( 𝑥 − ( 𝑌 − 𝑋 ) ) + 𝑌 ) )
91 elfzoelz ⊢ ( 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) → 𝑥 ∈ ℤ )
92 91 zcnd ⊢ ( 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) → 𝑥 ∈ ℂ )
93 92 adantl ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) → 𝑥 ∈ ℂ )
94 25 27 subcld ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑌 − 𝑋 ) ∈ ℂ )
95 94 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) → ( 𝑌 − 𝑋 ) ∈ ℂ )
96 25 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) → 𝑌 ∈ ℂ )
97 93 95 96 subadd23d ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) → ( ( 𝑥 − ( 𝑌 − 𝑋 ) ) + 𝑌 ) = ( 𝑥 + ( 𝑌 − ( 𝑌 − 𝑋 ) ) ) )
98 25 27 nncand ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑌 − ( 𝑌 − 𝑋 ) ) = 𝑋 )
99 98 oveq2d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑥 + ( 𝑌 − ( 𝑌 − 𝑋 ) ) ) = ( 𝑥 + 𝑋 ) )
100 99 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) → ( 𝑥 + ( 𝑌 − ( 𝑌 − 𝑋 ) ) ) = ( 𝑥 + 𝑋 ) )
101 90 97 100 3eqtrd ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) → ( ( 𝑥 − ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ) + 𝑌 ) = ( 𝑥 + 𝑋 ) )
102 101 fveq2d ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) → ( 𝑆 ‘ ( ( 𝑥 − ( ♯ ‘ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ) + 𝑌 ) ) = ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) )
103 73 88 102 3eqtrd ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) → ( ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) )
104 65 103 jaodan ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ ( 𝑥 ∈ ( 0 ..^ ( 𝑌 − 𝑋 ) ) ∨ 𝑥 ∈ ( ( 𝑌 − 𝑋 ) ..^ ( 𝑍 − 𝑋 ) ) ) ) → ( ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) )
105 51 104 syldan ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑍 − 𝑋 ) ) ) → ( ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) )
106 simpll ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑍 − 𝑋 ) ) ) → 𝑆 ∈ Word 𝐴 )
107 42 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑍 − 𝑋 ) ) ) → 𝑋 ∈ ( 0 ... 𝑍 ) )
108 simplr3 ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑍 − 𝑋 ) ) ) → 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
109 simpr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑍 − 𝑋 ) ) ) → 𝑥 ∈ ( 0 ..^ ( 𝑍 − 𝑋 ) ) )
110 swrdfv ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑋 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑍 − 𝑋 ) ) ) → ( ( 𝑆 substr ⟨ 𝑋 , 𝑍 ⟩ ) ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) )
111 106 107 108 109 110 syl31anc ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑍 − 𝑋 ) ) ) → ( ( 𝑆 substr ⟨ 𝑋 , 𝑍 ⟩ ) ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) )
112 105 111 eqtr4d ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑍 − 𝑋 ) ) ) → ( ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( ( 𝑆 substr ⟨ 𝑋 , 𝑍 ⟩ ) ‘ 𝑥 ) )
113 34 47 112 eqfnfvd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) = ( 𝑆 substr ⟨ 𝑋 , 𝑍 ⟩ ) )