Metamath Proof Explorer

Theorem ccatass

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

Ref Expression
Assertion ccatass 
|- ( ( S e. Word B /\ T e. Word B /\ U e. Word B ) -> ( ( S ++ T ) ++ U ) = ( S ++ ( T ++ U ) ) )

Proof

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