MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ccatass Structured version   Visualization version   GIF version

Theorem ccatass 13749
Description: Associative law for concatenation of words. (Contributed by Stefan O'Rear, 15-Aug-2015.)
Assertion
Ref Expression
ccatass ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ++ 𝑈) = (𝑆 ++ (𝑇 ++ 𝑈)))

Proof of Theorem ccatass
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 ccatcl 13735 . . . . 5 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵) → (𝑆 ++ 𝑇) ∈ Word 𝐵)
2 ccatcl 13735 . . . . 5 (((𝑆 ++ 𝑇) ∈ Word 𝐵𝑈 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ++ 𝑈) ∈ Word 𝐵)
31, 2stoic3 1740 . . . 4 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ++ 𝑈) ∈ Word 𝐵)
4 wrdf 13675 . . . 4 (((𝑆 ++ 𝑇) ++ 𝑈) ∈ Word 𝐵 → ((𝑆 ++ 𝑇) ++ 𝑈):(0..^(♯‘((𝑆 ++ 𝑇) ++ 𝑈)))⟶𝐵)
5 ffn 6341 . . . 4 (((𝑆 ++ 𝑇) ++ 𝑈):(0..^(♯‘((𝑆 ++ 𝑇) ++ 𝑈)))⟶𝐵 → ((𝑆 ++ 𝑇) ++ 𝑈) Fn (0..^(♯‘((𝑆 ++ 𝑇) ++ 𝑈))))
63, 4, 53syl 18 . . 3 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ++ 𝑈) Fn (0..^(♯‘((𝑆 ++ 𝑇) ++ 𝑈))))
7 ccatlen 13736 . . . . . . 7 (((𝑆 ++ 𝑇) ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (♯‘((𝑆 ++ 𝑇) ++ 𝑈)) = ((♯‘(𝑆 ++ 𝑇)) + (♯‘𝑈)))
81, 7stoic3 1740 . . . . . 6 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (♯‘((𝑆 ++ 𝑇) ++ 𝑈)) = ((♯‘(𝑆 ++ 𝑇)) + (♯‘𝑈)))
9 ccatlen 13736 . . . . . . . 8 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵) → (♯‘(𝑆 ++ 𝑇)) = ((♯‘𝑆) + (♯‘𝑇)))
1093adant3 1113 . . . . . . 7 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (♯‘(𝑆 ++ 𝑇)) = ((♯‘𝑆) + (♯‘𝑇)))
1110oveq1d 6989 . . . . . 6 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → ((♯‘(𝑆 ++ 𝑇)) + (♯‘𝑈)) = (((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))
128, 11eqtrd 2807 . . . . 5 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (♯‘((𝑆 ++ 𝑇) ++ 𝑈)) = (((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))
1312oveq2d 6990 . . . 4 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (0..^(♯‘((𝑆 ++ 𝑇) ++ 𝑈))) = (0..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈))))
1413fneq2d 6277 . . 3 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (((𝑆 ++ 𝑇) ++ 𝑈) Fn (0..^(♯‘((𝑆 ++ 𝑇) ++ 𝑈))) ↔ ((𝑆 ++ 𝑇) ++ 𝑈) Fn (0..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))))
156, 14mpbid 224 . 2 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ++ 𝑈) Fn (0..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈))))
16 simp1 1117 . . . . 5 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → 𝑆 ∈ Word 𝐵)
17 ccatcl 13735 . . . . . 6 ((𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (𝑇 ++ 𝑈) ∈ Word 𝐵)
18173adant1 1111 . . . . 5 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (𝑇 ++ 𝑈) ∈ Word 𝐵)
19 ccatcl 13735 . . . . 5 ((𝑆 ∈ Word 𝐵 ∧ (𝑇 ++ 𝑈) ∈ Word 𝐵) → (𝑆 ++ (𝑇 ++ 𝑈)) ∈ Word 𝐵)
2016, 18, 19syl2anc 576 . . . 4 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (𝑆 ++ (𝑇 ++ 𝑈)) ∈ Word 𝐵)
21 wrdf 13675 . . . 4 ((𝑆 ++ (𝑇 ++ 𝑈)) ∈ Word 𝐵 → (𝑆 ++ (𝑇 ++ 𝑈)):(0..^(♯‘(𝑆 ++ (𝑇 ++ 𝑈))))⟶𝐵)
22 ffn 6341 . . . 4 ((𝑆 ++ (𝑇 ++ 𝑈)):(0..^(♯‘(𝑆 ++ (𝑇 ++ 𝑈))))⟶𝐵 → (𝑆 ++ (𝑇 ++ 𝑈)) Fn (0..^(♯‘(𝑆 ++ (𝑇 ++ 𝑈)))))
2320, 21, 223syl 18 . . 3 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (𝑆 ++ (𝑇 ++ 𝑈)) Fn (0..^(♯‘(𝑆 ++ (𝑇 ++ 𝑈)))))
24 ccatlen 13736 . . . . . . . 8 ((𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (♯‘(𝑇 ++ 𝑈)) = ((♯‘𝑇) + (♯‘𝑈)))
25243adant1 1111 . . . . . . 7 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (♯‘(𝑇 ++ 𝑈)) = ((♯‘𝑇) + (♯‘𝑈)))
2625oveq2d 6990 . . . . . 6 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → ((♯‘𝑆) + (♯‘(𝑇 ++ 𝑈))) = ((♯‘𝑆) + ((♯‘𝑇) + (♯‘𝑈))))
27 ccatlen 13736 . . . . . . 7 ((𝑆 ∈ Word 𝐵 ∧ (𝑇 ++ 𝑈) ∈ Word 𝐵) → (♯‘(𝑆 ++ (𝑇 ++ 𝑈))) = ((♯‘𝑆) + (♯‘(𝑇 ++ 𝑈))))
2816, 18, 27syl2anc 576 . . . . . 6 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (♯‘(𝑆 ++ (𝑇 ++ 𝑈))) = ((♯‘𝑆) + (♯‘(𝑇 ++ 𝑈))))
29 lencl 13692 . . . . . . . . 9 (𝑆 ∈ Word 𝐵 → (♯‘𝑆) ∈ ℕ0)
30293ad2ant1 1114 . . . . . . . 8 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (♯‘𝑆) ∈ ℕ0)
3130nn0cnd 11767 . . . . . . 7 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (♯‘𝑆) ∈ ℂ)
32 lencl 13692 . . . . . . . . 9 (𝑇 ∈ Word 𝐵 → (♯‘𝑇) ∈ ℕ0)
33323ad2ant2 1115 . . . . . . . 8 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (♯‘𝑇) ∈ ℕ0)
3433nn0cnd 11767 . . . . . . 7 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (♯‘𝑇) ∈ ℂ)
35 lencl 13692 . . . . . . . . 9 (𝑈 ∈ Word 𝐵 → (♯‘𝑈) ∈ ℕ0)
36353ad2ant3 1116 . . . . . . . 8 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (♯‘𝑈) ∈ ℕ0)
3736nn0cnd 11767 . . . . . . 7 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (♯‘𝑈) ∈ ℂ)
3831, 34, 37addassd 10460 . . . . . 6 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)) = ((♯‘𝑆) + ((♯‘𝑇) + (♯‘𝑈))))
3926, 28, 383eqtr4d 2817 . . . . 5 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (♯‘(𝑆 ++ (𝑇 ++ 𝑈))) = (((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))
4039oveq2d 6990 . . . 4 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (0..^(♯‘(𝑆 ++ (𝑇 ++ 𝑈)))) = (0..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈))))
4140fneq2d 6277 . . 3 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → ((𝑆 ++ (𝑇 ++ 𝑈)) Fn (0..^(♯‘(𝑆 ++ (𝑇 ++ 𝑈)))) ↔ (𝑆 ++ (𝑇 ++ 𝑈)) Fn (0..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))))
4223, 41mpbid 224 . 2 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (𝑆 ++ (𝑇 ++ 𝑈)) Fn (0..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈))))
4330nn0zd 11896 . . . 4 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (♯‘𝑆) ∈ ℤ)
44 fzospliti 12882 . . . . 5 ((𝑥 ∈ (0..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈))) ∧ (♯‘𝑆) ∈ ℤ) → (𝑥 ∈ (0..^(♯‘𝑆)) ∨ 𝑥 ∈ ((♯‘𝑆)..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))))
4544ancoms 451 . . . 4 (((♯‘𝑆) ∈ ℤ ∧ 𝑥 ∈ (0..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → (𝑥 ∈ (0..^(♯‘𝑆)) ∨ 𝑥 ∈ ((♯‘𝑆)..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))))
4643, 45sylan 572 . . 3 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → (𝑥 ∈ (0..^(♯‘𝑆)) ∨ 𝑥 ∈ ((♯‘𝑆)..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))))
47 simpl1 1172 . . . . . 6 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → 𝑆 ∈ Word 𝐵)
48 simpl2 1173 . . . . . 6 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → 𝑇 ∈ Word 𝐵)
49 simpr 477 . . . . . 6 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → 𝑥 ∈ (0..^(♯‘𝑆)))
50 ccatval1 13738 . . . . . 6 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑥 ∈ (0..^(♯‘𝑆))) → ((𝑆 ++ 𝑇)‘𝑥) = (𝑆𝑥))
5147, 48, 49, 50syl3anc 1352 . . . . 5 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → ((𝑆 ++ 𝑇)‘𝑥) = (𝑆𝑥))
5213adant3 1113 . . . . . . 7 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (𝑆 ++ 𝑇) ∈ Word 𝐵)
5352adantr 473 . . . . . 6 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → (𝑆 ++ 𝑇) ∈ Word 𝐵)
54 simpl3 1174 . . . . . 6 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → 𝑈 ∈ Word 𝐵)
55 uzid 12071 . . . . . . . . . . 11 ((♯‘𝑆) ∈ ℤ → (♯‘𝑆) ∈ (ℤ‘(♯‘𝑆)))
5643, 55syl 17 . . . . . . . . . 10 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (♯‘𝑆) ∈ (ℤ‘(♯‘𝑆)))
57 uzaddcl 12116 . . . . . . . . . 10 (((♯‘𝑆) ∈ (ℤ‘(♯‘𝑆)) ∧ (♯‘𝑇) ∈ ℕ0) → ((♯‘𝑆) + (♯‘𝑇)) ∈ (ℤ‘(♯‘𝑆)))
5856, 33, 57syl2anc 576 . . . . . . . . 9 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → ((♯‘𝑆) + (♯‘𝑇)) ∈ (ℤ‘(♯‘𝑆)))
59 fzoss2 12878 . . . . . . . . 9 (((♯‘𝑆) + (♯‘𝑇)) ∈ (ℤ‘(♯‘𝑆)) → (0..^(♯‘𝑆)) ⊆ (0..^((♯‘𝑆) + (♯‘𝑇))))
6058, 59syl 17 . . . . . . . 8 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (0..^(♯‘𝑆)) ⊆ (0..^((♯‘𝑆) + (♯‘𝑇))))
6110oveq2d 6990 . . . . . . . 8 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (0..^(♯‘(𝑆 ++ 𝑇))) = (0..^((♯‘𝑆) + (♯‘𝑇))))
6260, 61sseqtr4d 3891 . . . . . . 7 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (0..^(♯‘𝑆)) ⊆ (0..^(♯‘(𝑆 ++ 𝑇))))
6362sselda 3851 . . . . . 6 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → 𝑥 ∈ (0..^(♯‘(𝑆 ++ 𝑇))))
64 ccatval1 13738 . . . . . 6 (((𝑆 ++ 𝑇) ∈ Word 𝐵𝑈 ∈ Word 𝐵𝑥 ∈ (0..^(♯‘(𝑆 ++ 𝑇)))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = ((𝑆 ++ 𝑇)‘𝑥))
6553, 54, 63, 64syl3anc 1352 . . . . 5 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = ((𝑆 ++ 𝑇)‘𝑥))
6618adantr 473 . . . . . 6 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → (𝑇 ++ 𝑈) ∈ Word 𝐵)
67 ccatval1 13738 . . . . . 6 ((𝑆 ∈ Word 𝐵 ∧ (𝑇 ++ 𝑈) ∈ Word 𝐵𝑥 ∈ (0..^(♯‘𝑆))) → ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥) = (𝑆𝑥))
6847, 66, 49, 67syl3anc 1352 . . . . 5 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥) = (𝑆𝑥))
6951, 65, 683eqtr4d 2817 . . . 4 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥))
7033nn0zd 11896 . . . . . . 7 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (♯‘𝑇) ∈ ℤ)
7143, 70zaddcld 11902 . . . . . 6 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → ((♯‘𝑆) + (♯‘𝑇)) ∈ ℤ)
72 fzospliti 12882 . . . . . . 7 ((𝑥 ∈ ((♯‘𝑆)..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈))) ∧ ((♯‘𝑆) + (♯‘𝑇)) ∈ ℤ) → (𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) ∨ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))))
7372ancoms 451 . . . . . 6 ((((♯‘𝑆) + (♯‘𝑇)) ∈ ℤ ∧ 𝑥 ∈ ((♯‘𝑆)..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → (𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) ∨ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))))
7471, 73sylan 572 . . . . 5 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → (𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) ∨ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))))
75 simpl1 1172 . . . . . . . . 9 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → 𝑆 ∈ Word 𝐵)
76 simpl2 1173 . . . . . . . . 9 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → 𝑇 ∈ Word 𝐵)
77 simpr 477 . . . . . . . . 9 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))))
78 ccatval2 13739 . . . . . . . . 9 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝑥) = (𝑇‘(𝑥 − (♯‘𝑆))))
7975, 76, 77, 78syl3anc 1352 . . . . . . . 8 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝑥) = (𝑇‘(𝑥 − (♯‘𝑆))))
80 simpl3 1174 . . . . . . . . 9 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → 𝑈 ∈ Word 𝐵)
81 fzosubel3 12911 . . . . . . . . . . 11 ((𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) ∧ (♯‘𝑇) ∈ ℤ) → (𝑥 − (♯‘𝑆)) ∈ (0..^(♯‘𝑇)))
8281ancoms 451 . . . . . . . . . 10 (((♯‘𝑇) ∈ ℤ ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → (𝑥 − (♯‘𝑆)) ∈ (0..^(♯‘𝑇)))
8370, 82sylan 572 . . . . . . . . 9 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → (𝑥 − (♯‘𝑆)) ∈ (0..^(♯‘𝑇)))
84 ccatval1 13738 . . . . . . . . 9 ((𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵 ∧ (𝑥 − (♯‘𝑆)) ∈ (0..^(♯‘𝑇))) → ((𝑇 ++ 𝑈)‘(𝑥 − (♯‘𝑆))) = (𝑇‘(𝑥 − (♯‘𝑆))))
8576, 80, 83, 84syl3anc 1352 . . . . . . . 8 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → ((𝑇 ++ 𝑈)‘(𝑥 − (♯‘𝑆))) = (𝑇‘(𝑥 − (♯‘𝑆))))
8679, 85eqtr4d 2810 . . . . . . 7 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝑥) = ((𝑇 ++ 𝑈)‘(𝑥 − (♯‘𝑆))))
8752adantr 473 . . . . . . . 8 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → (𝑆 ++ 𝑇) ∈ Word 𝐵)
88 fzoss1 12877 . . . . . . . . . . . 12 ((♯‘𝑆) ∈ (ℤ‘0) → ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) ⊆ (0..^((♯‘𝑆) + (♯‘𝑇))))
89 nn0uz 12092 . . . . . . . . . . . 12 0 = (ℤ‘0)
9088, 89eleq2s 2877 . . . . . . . . . . 11 ((♯‘𝑆) ∈ ℕ0 → ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) ⊆ (0..^((♯‘𝑆) + (♯‘𝑇))))
9130, 90syl 17 . . . . . . . . . 10 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) ⊆ (0..^((♯‘𝑆) + (♯‘𝑇))))
9291, 61sseqtr4d 3891 . . . . . . . . 9 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) ⊆ (0..^(♯‘(𝑆 ++ 𝑇))))
9392sselda 3851 . . . . . . . 8 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → 𝑥 ∈ (0..^(♯‘(𝑆 ++ 𝑇))))
9487, 80, 93, 64syl3anc 1352 . . . . . . 7 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = ((𝑆 ++ 𝑇)‘𝑥))
9518adantr 473 . . . . . . . 8 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → (𝑇 ++ 𝑈) ∈ Word 𝐵)
96 uzid 12071 . . . . . . . . . . . . 13 (((♯‘𝑆) + (♯‘𝑇)) ∈ ℤ → ((♯‘𝑆) + (♯‘𝑇)) ∈ (ℤ‘((♯‘𝑆) + (♯‘𝑇))))
9771, 96syl 17 . . . . . . . . . . . 12 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → ((♯‘𝑆) + (♯‘𝑇)) ∈ (ℤ‘((♯‘𝑆) + (♯‘𝑇))))
98 uzaddcl 12116 . . . . . . . . . . . 12 ((((♯‘𝑆) + (♯‘𝑇)) ∈ (ℤ‘((♯‘𝑆) + (♯‘𝑇))) ∧ (♯‘𝑈) ∈ ℕ0) → (((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)) ∈ (ℤ‘((♯‘𝑆) + (♯‘𝑇))))
9997, 36, 98syl2anc 576 . . . . . . . . . . 11 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)) ∈ (ℤ‘((♯‘𝑆) + (♯‘𝑇))))
100 fzoss2 12878 . . . . . . . . . . 11 ((((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)) ∈ (ℤ‘((♯‘𝑆) + (♯‘𝑇))) → ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) ⊆ ((♯‘𝑆)..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈))))
10199, 100syl 17 . . . . . . . . . 10 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) ⊆ ((♯‘𝑆)..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈))))
10226, 38eqtr4d 2810 . . . . . . . . . . 11 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → ((♯‘𝑆) + (♯‘(𝑇 ++ 𝑈))) = (((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))
103102oveq2d 6990 . . . . . . . . . 10 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → ((♯‘𝑆)..^((♯‘𝑆) + (♯‘(𝑇 ++ 𝑈)))) = ((♯‘𝑆)..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈))))
104101, 103sseqtr4d 3891 . . . . . . . . 9 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) ⊆ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘(𝑇 ++ 𝑈)))))
105104sselda 3851 . . . . . . . 8 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘(𝑇 ++ 𝑈)))))
106 ccatval2 13739 . . . . . . . 8 ((𝑆 ∈ Word 𝐵 ∧ (𝑇 ++ 𝑈) ∈ Word 𝐵𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘(𝑇 ++ 𝑈))))) → ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥) = ((𝑇 ++ 𝑈)‘(𝑥 − (♯‘𝑆))))
10775, 95, 105, 106syl3anc 1352 . . . . . . 7 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥) = ((𝑇 ++ 𝑈)‘(𝑥 − (♯‘𝑆))))
10886, 94, 1073eqtr4d 2817 . . . . . 6 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥))
10910oveq2d 6990 . . . . . . . . . . 11 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (𝑥 − (♯‘(𝑆 ++ 𝑇))) = (𝑥 − ((♯‘𝑆) + (♯‘𝑇))))
110109adantr 473 . . . . . . . . . 10 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → (𝑥 − (♯‘(𝑆 ++ 𝑇))) = (𝑥 − ((♯‘𝑆) + (♯‘𝑇))))
111 elfzoelz 12852 . . . . . . . . . . . . 13 (𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈))) → 𝑥 ∈ ℤ)
112111zcnd 11899 . . . . . . . . . . . 12 (𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈))) → 𝑥 ∈ ℂ)
113112adantl 474 . . . . . . . . . . 11 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → 𝑥 ∈ ℂ)
11431adantr 473 . . . . . . . . . . 11 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → (♯‘𝑆) ∈ ℂ)
11534adantr 473 . . . . . . . . . . 11 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → (♯‘𝑇) ∈ ℂ)
116113, 114, 115subsub4d 10827 . . . . . . . . . 10 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → ((𝑥 − (♯‘𝑆)) − (♯‘𝑇)) = (𝑥 − ((♯‘𝑆) + (♯‘𝑇))))
117110, 116eqtr4d 2810 . . . . . . . . 9 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → (𝑥 − (♯‘(𝑆 ++ 𝑇))) = ((𝑥 − (♯‘𝑆)) − (♯‘𝑇)))
118117fveq2d 6500 . . . . . . . 8 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → (𝑈‘(𝑥 − (♯‘(𝑆 ++ 𝑇)))) = (𝑈‘((𝑥 − (♯‘𝑆)) − (♯‘𝑇))))
119 simpl2 1173 . . . . . . . . 9 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → 𝑇 ∈ Word 𝐵)
120 simpl3 1174 . . . . . . . . 9 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → 𝑈 ∈ Word 𝐵)
12138oveq2d 6990 . . . . . . . . . . . 12 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈))) = (((♯‘𝑆) + (♯‘𝑇))..^((♯‘𝑆) + ((♯‘𝑇) + (♯‘𝑈)))))
122121eleq2d 2844 . . . . . . . . . . 11 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈))) ↔ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^((♯‘𝑆) + ((♯‘𝑇) + (♯‘𝑈))))))
123122biimpa 469 . . . . . . . . . 10 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^((♯‘𝑆) + ((♯‘𝑇) + (♯‘𝑈)))))
12443adantr 473 . . . . . . . . . 10 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → (♯‘𝑆) ∈ ℤ)
12570adantr 473 . . . . . . . . . 10 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → (♯‘𝑇) ∈ ℤ)
12636nn0zd 11896 . . . . . . . . . . . 12 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (♯‘𝑈) ∈ ℤ)
12770, 126zaddcld 11902 . . . . . . . . . . 11 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → ((♯‘𝑇) + (♯‘𝑈)) ∈ ℤ)
128127adantr 473 . . . . . . . . . 10 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → ((♯‘𝑇) + (♯‘𝑈)) ∈ ℤ)
129 fzosubel2 12910 . . . . . . . . . 10 ((𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^((♯‘𝑆) + ((♯‘𝑇) + (♯‘𝑈)))) ∧ ((♯‘𝑆) ∈ ℤ ∧ (♯‘𝑇) ∈ ℤ ∧ ((♯‘𝑇) + (♯‘𝑈)) ∈ ℤ)) → (𝑥 − (♯‘𝑆)) ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑈))))
130123, 124, 125, 128, 129syl13anc 1353 . . . . . . . . 9 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → (𝑥 − (♯‘𝑆)) ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑈))))
131 ccatval2 13739 . . . . . . . . 9 ((𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵 ∧ (𝑥 − (♯‘𝑆)) ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑈)))) → ((𝑇 ++ 𝑈)‘(𝑥 − (♯‘𝑆))) = (𝑈‘((𝑥 − (♯‘𝑆)) − (♯‘𝑇))))
132119, 120, 130, 131syl3anc 1352 . . . . . . . 8 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → ((𝑇 ++ 𝑈)‘(𝑥 − (♯‘𝑆))) = (𝑈‘((𝑥 − (♯‘𝑆)) − (♯‘𝑇))))
133118, 132eqtr4d 2810 . . . . . . 7 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → (𝑈‘(𝑥 − (♯‘(𝑆 ++ 𝑇)))) = ((𝑇 ++ 𝑈)‘(𝑥 − (♯‘𝑆))))
13452adantr 473 . . . . . . . 8 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → (𝑆 ++ 𝑇) ∈ Word 𝐵)
13510, 11oveq12d 6992 . . . . . . . . . 10 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → ((♯‘(𝑆 ++ 𝑇))..^((♯‘(𝑆 ++ 𝑇)) + (♯‘𝑈))) = (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈))))
136135eleq2d 2844 . . . . . . . . 9 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (𝑥 ∈ ((♯‘(𝑆 ++ 𝑇))..^((♯‘(𝑆 ++ 𝑇)) + (♯‘𝑈))) ↔ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))))
137136biimpar 470 . . . . . . . 8 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → 𝑥 ∈ ((♯‘(𝑆 ++ 𝑇))..^((♯‘(𝑆 ++ 𝑇)) + (♯‘𝑈))))
138 ccatval2 13739 . . . . . . . 8 (((𝑆 ++ 𝑇) ∈ Word 𝐵𝑈 ∈ Word 𝐵𝑥 ∈ ((♯‘(𝑆 ++ 𝑇))..^((♯‘(𝑆 ++ 𝑇)) + (♯‘𝑈)))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = (𝑈‘(𝑥 − (♯‘(𝑆 ++ 𝑇)))))
139134, 120, 137, 138syl3anc 1352 . . . . . . 7 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = (𝑈‘(𝑥 − (♯‘(𝑆 ++ 𝑇)))))
140 simpl1 1172 . . . . . . . 8 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → 𝑆 ∈ Word 𝐵)
14118adantr 473 . . . . . . . 8 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → (𝑇 ++ 𝑈) ∈ Word 𝐵)
142 fzoss1 12877 . . . . . . . . . . 11 (((♯‘𝑆) + (♯‘𝑇)) ∈ (ℤ‘(♯‘𝑆)) → (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈))) ⊆ ((♯‘𝑆)..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈))))
14358, 142syl 17 . . . . . . . . . 10 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈))) ⊆ ((♯‘𝑆)..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈))))
144143, 103sseqtr4d 3891 . . . . . . . . 9 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈))) ⊆ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘(𝑇 ++ 𝑈)))))
145144sselda 3851 . . . . . . . 8 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘(𝑇 ++ 𝑈)))))
146140, 141, 145, 106syl3anc 1352 . . . . . . 7 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥) = ((𝑇 ++ 𝑈)‘(𝑥 − (♯‘𝑆))))
147133, 139, 1463eqtr4d 2817 . . . . . 6 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥))
148108, 147jaodan 941 . . . . 5 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ (𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) ∨ 𝑥 ∈ (((♯‘𝑆) + (♯‘𝑇))..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈))))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥))
14974, 148syldan 583 . . . 4 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥))
15069, 149jaodan 941 . . 3 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ (𝑥 ∈ (0..^(♯‘𝑆)) ∨ 𝑥 ∈ ((♯‘𝑆)..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈))))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥))
15146, 150syldan 583 . 2 (((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(((♯‘𝑆) + (♯‘𝑇)) + (♯‘𝑈)))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥))
15215, 42, 151eqfnfvd 6628 1 ((𝑆 ∈ Word 𝐵𝑇 ∈ Word 𝐵𝑈 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ++ 𝑈) = (𝑆 ++ (𝑇 ++ 𝑈)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387  wo 834  w3a 1069   = wceq 1508  wcel 2051  wss 3822   Fn wfn 6180  wf 6181  cfv 6185  (class class class)co 6974  cc 10331  0cc0 10333   + caddc 10336  cmin 10668  0cn0 11705  cz 11791  cuz 12056  ..^cfzo 12847  chash 13503  Word cword 13670   ++ cconcat 13731
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2743  ax-rep 5045  ax-sep 5056  ax-nul 5063  ax-pow 5115  ax-pr 5182  ax-un 7277  ax-cnex 10389  ax-resscn 10390  ax-1cn 10391  ax-icn 10392  ax-addcl 10393  ax-addrcl 10394  ax-mulcl 10395  ax-mulrcl 10396  ax-mulcom 10397  ax-addass 10398  ax-mulass 10399  ax-distr 10400  ax-i2m1 10401  ax-1ne0 10402  ax-1rid 10403  ax-rnegex 10404  ax-rrecex 10405  ax-cnre 10406  ax-pre-lttri 10407  ax-pre-lttrn 10408  ax-pre-ltadd 10409  ax-pre-mulgt0 10410
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-ne 2961  df-nel 3067  df-ral 3086  df-rex 3087  df-reu 3088  df-rab 3090  df-v 3410  df-sbc 3675  df-csb 3780  df-dif 3825  df-un 3827  df-in 3829  df-ss 3836  df-pss 3838  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4709  df-int 4746  df-iun 4790  df-br 4926  df-opab 4988  df-mpt 5005  df-tr 5027  df-id 5308  df-eprel 5313  df-po 5322  df-so 5323  df-fr 5362  df-we 5364  df-xp 5409  df-rel 5410  df-cnv 5411  df-co 5412  df-dm 5413  df-rn 5414  df-res 5415  df-ima 5416  df-pred 5983  df-ord 6029  df-on 6030  df-lim 6031  df-suc 6032  df-iota 6149  df-fun 6187  df-fn 6188  df-f 6189  df-f1 6190  df-fo 6191  df-f1o 6192  df-fv 6193  df-riota 6935  df-ov 6977  df-oprab 6978  df-mpo 6979  df-om 7395  df-1st 7499  df-2nd 7500  df-wrecs 7748  df-recs 7810  df-rdg 7848  df-1o 7903  df-oadd 7907  df-er 8087  df-en 8305  df-dom 8306  df-sdom 8307  df-fin 8308  df-card 9160  df-pnf 10474  df-mnf 10475  df-xr 10476  df-ltxr 10477  df-le 10478  df-sub 10670  df-neg 10671  df-nn 11438  df-n0 11706  df-z 11792  df-uz 12057  df-fz 12707  df-fzo 12848  df-hash 13504  df-word 13671  df-concat 13732
This theorem is referenced by:  ccatw2s1ass  13792  cats1cat  14083  cats2cat  14084  frmdmnd  17877  efginvrel2  18623  efgredleme  18640  efgredlemc  18642  efgcpbllemb  18653  numclwwlk1lem2foalem  27904  numclwwlk1lem2foalemOLD  27905  numclwwlk1lem2fo  27915  numclwwlk1lem2foOLD  27920  signstfvc  31523
  Copyright terms: Public domain W3C validator