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∈WordB∧T∈WordB∧U∈WordB→S++T++U=S++T++U

Proof

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