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 ⟨ 𝑋 , 𝑍 ⟩ ) )