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