Metamath Proof Explorer

Theorem ccatass

Description: Associative law for concatenation of words. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion ccatass ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) = ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 ccatcl ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( 𝑆 ++ 𝑇 ) ∈ Word 𝐵 )
2 ccatcl ⊢ ( ( ( 𝑆 ++ 𝑇 ) ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) ∈ Word 𝐵 )
3 1 2 stoic3 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) ∈ Word 𝐵 )
4 wrdfn ⊢ ( ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) ∈ Word 𝐵 → ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) Fn ( 0 ..^ ( ♯ ‘ ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) ) ) )
5 3 4 syl ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) Fn ( 0 ..^ ( ♯ ‘ ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) ) ) )
6 ccatlen ⊢ ( ( ( 𝑆 ++ 𝑇 ) ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ♯ ‘ ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) ) = ( ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) )
7 1 6 stoic3 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ♯ ‘ ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) ) = ( ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) )
8 ccatlen ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) = ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) )
9 8 3adant3 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) = ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) )
10 9 oveq1d ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) = ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) )
11 7 10 eqtrd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ♯ ‘ ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) ) = ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) )
12 11 oveq2d ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( 0 ..^ ( ♯ ‘ ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) ) ) = ( 0 ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) )
13 12 fneq2d ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) Fn ( 0 ..^ ( ♯ ‘ ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) ) ) ↔ ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) Fn ( 0 ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) )
14 5 13 mpbid ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) Fn ( 0 ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) )
15 simp1 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → 𝑆 ∈ Word 𝐵 )
16 ccatcl ⊢ ( ( 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( 𝑇 ++ 𝑈 ) ∈ Word 𝐵 )
17 16 3adant1 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( 𝑇 ++ 𝑈 ) ∈ Word 𝐵 )
18 ccatcl ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ ( 𝑇 ++ 𝑈 ) ∈ Word 𝐵 ) → ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) ∈ Word 𝐵 )
19 15 17 18 syl2anc ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) ∈ Word 𝐵 )
20 wrdfn ⊢ ( ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) ∈ Word 𝐵 → ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) Fn ( 0 ..^ ( ♯ ‘ ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) ) ) )
21 19 20 syl ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) Fn ( 0 ..^ ( ♯ ‘ ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) ) ) )
22 ccatlen ⊢ ( ( 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ♯ ‘ ( 𝑇 ++ 𝑈 ) ) = ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) )
23 22 3adant1 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ♯ ‘ ( 𝑇 ++ 𝑈 ) ) = ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) )
24 23 oveq2d ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ( 𝑇 ++ 𝑈 ) ) ) = ( ( ♯ ‘ 𝑆 ) + ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) )
25 ccatlen ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ ( 𝑇 ++ 𝑈 ) ∈ Word 𝐵 ) → ( ♯ ‘ ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) ) = ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ( 𝑇 ++ 𝑈 ) ) ) )
26 15 17 25 syl2anc ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ♯ ‘ ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) ) = ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ( 𝑇 ++ 𝑈 ) ) ) )
27 lencl ⊢ ( 𝑆 ∈ Word 𝐵 → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
28 27 3ad2ant1 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
29 28 nn0cnd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ♯ ‘ 𝑆 ) ∈ ℂ )
30 lencl ⊢ ( 𝑇 ∈ Word 𝐵 → ( ♯ ‘ 𝑇 ) ∈ ℕ0 )
31 30 3ad2ant2 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ♯ ‘ 𝑇 ) ∈ ℕ0 )
32 31 nn0cnd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ♯ ‘ 𝑇 ) ∈ ℂ )
33 lencl ⊢ ( 𝑈 ∈ Word 𝐵 → ( ♯ ‘ 𝑈 ) ∈ ℕ0 )
34 33 3ad2ant3 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ♯ ‘ 𝑈 ) ∈ ℕ0 )
35 34 nn0cnd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ♯ ‘ 𝑈 ) ∈ ℂ )
36 29 32 35 addassd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) = ( ( ♯ ‘ 𝑆 ) + ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) )
37 24 26 36 3eqtr4d ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ♯ ‘ ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) ) = ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) )
38 37 oveq2d ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( 0 ..^ ( ♯ ‘ ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) ) ) = ( 0 ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) )
39 38 fneq2d ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) Fn ( 0 ..^ ( ♯ ‘ ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) ) ) ↔ ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) Fn ( 0 ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) )
40 21 39 mpbid ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) Fn ( 0 ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) )
41 28 nn0zd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ♯ ‘ 𝑆 ) ∈ ℤ )
42 fzospliti ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ( ♯ ‘ 𝑆 ) ∈ ℤ ) → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∨ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) )
43 42 ex ⊢ ( 𝑥 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) → ( ( ♯ ‘ 𝑆 ) ∈ ℤ → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∨ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) ) )
44 41 43 mpan9 ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∨ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) )
45 simp2 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → 𝑇 ∈ Word 𝐵 )
46 id ⊢ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
47 ccatval1 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
48 15 45 46 47 syl2an3an ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
49 1 3adant3 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( 𝑆 ++ 𝑇 ) ∈ Word 𝐵 )
50 49 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 ++ 𝑇 ) ∈ Word 𝐵 )
51 simpl3 ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → 𝑈 ∈ Word 𝐵 )
52 41 uzidd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑆 ) ) )
53 uzaddcl ⊢ ( ( ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑆 ) ) ∧ ( ♯ ‘ 𝑇 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑆 ) ) )
54 52 31 53 syl2anc ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑆 ) ) )
55 fzoss2 ⊢ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑆 ) ) → ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
56 54 55 syl ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
57 9 oveq2d ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( 0 ..^ ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
58 56 57 sseqtrrd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⊆ ( 0 ..^ ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) ) )
59 58 sselda ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) ) )
60 ccatval1 ⊢ ( ( ( 𝑆 ++ 𝑇 ) ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) ) ) → ( ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) ‘ 𝑥 ) = ( ( 𝑆 ++ 𝑇 ) ‘ 𝑥 ) )
61 50 51 59 60 syl3anc ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) ‘ 𝑥 ) = ( ( 𝑆 ++ 𝑇 ) ‘ 𝑥 ) )
62 ccatval1 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ ( 𝑇 ++ 𝑈 ) ∈ Word 𝐵 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
63 15 17 46 62 syl2an3an ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
64 48 61 63 3eqtr4d ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) ‘ 𝑥 ) = ( ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) ‘ 𝑥 ) )
65 31 nn0zd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ♯ ‘ 𝑇 ) ∈ ℤ )
66 41 65 zaddcld ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ℤ )
67 fzospliti ⊢ ( ( 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ℤ ) → ( 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ∨ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) )
68 67 ex ⊢ ( 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) → ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ℤ → ( 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ∨ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) ) )
69 66 68 mpan9 ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ∨ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) )
70 id ⊢ ( 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) → 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
71 ccatval2 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝑥 ) = ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) )
72 15 45 70 71 syl2an3an ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝑥 ) = ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) )
73 simpl2 ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → 𝑇 ∈ Word 𝐵 )
74 simpl3 ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → 𝑈 ∈ Word 𝐵 )
75 fzosubel3 ⊢ ( ( 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) → ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
76 75 ex ⊢ ( 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) → ( ( ♯ ‘ 𝑇 ) ∈ ℤ → ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) )
77 65 76 mpan9 ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
78 ccatval1 ⊢ ( ( 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ∧ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) = ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) )
79 73 74 77 78 syl3anc ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) = ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) )
80 72 79 eqtr4d ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝑥 ) = ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) )
81 49 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( 𝑆 ++ 𝑇 ) ∈ Word 𝐵 )
82 fzoss1 ⊢ ( ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 0 ) → ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
83 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
84 82 83 eleq2s ⊢ ( ( ♯ ‘ 𝑆 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
85 28 84 syl ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
86 85 57 sseqtrrd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ⊆ ( 0 ..^ ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) ) )
87 86 sselda ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) ) )
88 81 74 87 60 syl3anc ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) ‘ 𝑥 ) = ( ( 𝑆 ++ 𝑇 ) ‘ 𝑥 ) )
89 simpl1 ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → 𝑆 ∈ Word 𝐵 )
90 17 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( 𝑇 ++ 𝑈 ) ∈ Word 𝐵 )
91 66 uzidd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
92 uzaddcl ⊢ ( ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ∧ ( ♯ ‘ 𝑈 ) ∈ ℕ0 ) → ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
93 91 34 92 syl2anc ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
94 fzoss2 ⊢ ( ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) → ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ⊆ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) )
95 93 94 syl ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ⊆ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) )
96 24 36 eqtr4d ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ( 𝑇 ++ 𝑈 ) ) ) = ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) )
97 96 oveq2d ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ( 𝑇 ++ 𝑈 ) ) ) ) = ( ( ♯ ‘ 𝑆 ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) )
98 95 97 sseqtrrd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ⊆ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ( 𝑇 ++ 𝑈 ) ) ) ) )
99 98 sselda ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ( 𝑇 ++ 𝑈 ) ) ) ) )
100 ccatval2 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ ( 𝑇 ++ 𝑈 ) ∈ Word 𝐵 ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ( 𝑇 ++ 𝑈 ) ) ) ) ) → ( ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) ‘ 𝑥 ) = ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) )
101 89 90 99 100 syl3anc ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) ‘ 𝑥 ) = ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) )
102 80 88 101 3eqtr4d ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) ‘ 𝑥 ) = ( ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) ‘ 𝑥 ) )
103 9 oveq2d ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( 𝑥 − ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) ) = ( 𝑥 − ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
104 103 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( 𝑥 − ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) ) = ( 𝑥 − ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
105 elfzoelz ⊢ ( 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) → 𝑥 ∈ ℤ )
106 105 zcnd ⊢ ( 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) → 𝑥 ∈ ℂ )
107 106 adantl ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → 𝑥 ∈ ℂ )
108 29 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( ♯ ‘ 𝑆 ) ∈ ℂ )
109 32 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( ♯ ‘ 𝑇 ) ∈ ℂ )
110 107 108 109 subsub4d ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( ( 𝑥 − ( ♯ ‘ 𝑆 ) ) − ( ♯ ‘ 𝑇 ) ) = ( 𝑥 − ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
111 104 110 eqtr4d ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( 𝑥 − ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) ) = ( ( 𝑥 − ( ♯ ‘ 𝑆 ) ) − ( ♯ ‘ 𝑇 ) ) )
112 111 fveq2d ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( 𝑈 ‘ ( 𝑥 − ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) ) ) = ( 𝑈 ‘ ( ( 𝑥 − ( ♯ ‘ 𝑆 ) ) − ( ♯ ‘ 𝑇 ) ) ) )
113 simpl2 ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → 𝑇 ∈ Word 𝐵 )
114 simpl3 ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → 𝑈 ∈ Word 𝐵 )
115 36 oveq2d ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) = ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) )
116 115 eleq2d ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ↔ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) ) )
117 116 biimpa ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) )
118 34 nn0zd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ♯ ‘ 𝑈 ) ∈ ℤ )
119 65 118 zaddcld ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ∈ ℤ )
120 41 65 119 3jca ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( ♯ ‘ 𝑆 ) ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ∈ ℤ ) )
121 120 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( ( ♯ ‘ 𝑆 ) ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ∈ ℤ ) )
122 fzosubel2 ⊢ ( ( 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) ∧ ( ( ♯ ‘ 𝑆 ) ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ∈ ℤ ) ) → ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) )
123 117 121 122 syl2anc ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) )
124 ccatval2 ⊢ ( ( 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ∧ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) = ( 𝑈 ‘ ( ( 𝑥 − ( ♯ ‘ 𝑆 ) ) − ( ♯ ‘ 𝑇 ) ) ) )
125 113 114 123 124 syl3anc ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) = ( 𝑈 ‘ ( ( 𝑥 − ( ♯ ‘ 𝑆 ) ) − ( ♯ ‘ 𝑇 ) ) ) )
126 112 125 eqtr4d ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( 𝑈 ‘ ( 𝑥 − ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) ) ) = ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) )
127 49 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( 𝑆 ++ 𝑇 ) ∈ Word 𝐵 )
128 9 10 oveq12d ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) ..^ ( ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) = ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) )
129 128 eleq2d ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( 𝑥 ∈ ( ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) ..^ ( ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ↔ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) )
130 129 biimpar ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → 𝑥 ∈ ( ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) ..^ ( ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) )
131 ccatval2 ⊢ ( ( ( 𝑆 ++ 𝑇 ) ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ∧ 𝑥 ∈ ( ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) ..^ ( ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) ‘ 𝑥 ) = ( 𝑈 ‘ ( 𝑥 − ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) ) ) )
132 127 114 130 131 syl3anc ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) ‘ 𝑥 ) = ( 𝑈 ‘ ( 𝑥 − ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) ) ) )
133 simpl1 ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → 𝑆 ∈ Word 𝐵 )
134 17 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( 𝑇 ++ 𝑈 ) ∈ Word 𝐵 )
135 fzoss1 ⊢ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑆 ) ) → ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ⊆ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) )
136 54 135 syl ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ⊆ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) )
137 136 97 sseqtrrd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ⊆ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ( 𝑇 ++ 𝑈 ) ) ) ) )
138 137 sselda ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ( 𝑇 ++ 𝑈 ) ) ) ) )
139 133 134 138 100 syl3anc ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) ‘ 𝑥 ) = ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) )
140 126 132 139 3eqtr4d ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) ‘ 𝑥 ) = ( ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) ‘ 𝑥 ) )
141 102 140 jaodan ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ ( 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ∨ 𝑥 ∈ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) ) → ( ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) ‘ 𝑥 ) = ( ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) ‘ 𝑥 ) )
142 69 141 syldan ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) ‘ 𝑥 ) = ( ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) ‘ 𝑥 ) )
143 64 142 jaodan ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∨ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) ) → ( ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) ‘ 𝑥 ) = ( ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) ‘ 𝑥 ) )
144 44 143 syldan ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) ‘ 𝑥 ) = ( ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) ‘ 𝑥 ) )
145 14 40 144 eqfnfvd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ) → ( ( 𝑆 ++ 𝑇 ) ++ 𝑈 ) = ( 𝑆 ++ ( 𝑇 ++ 𝑈 ) ) )