Metamath Proof Explorer

Theorem ccatcl

Description: The concatenation of two words is a word. (Contributed by FL, 2-Feb-2014) (Proof shortened by Stefan O'Rear, 15-Aug-2015) (Proof shortened by AV, 29-Apr-2020)

Ref Expression
Assertion ccatcl ⊢S∈WordB∧T∈WordB→S++T∈WordB

Proof

Step Hyp Ref Expression
1 ccatfval ⊢S∈WordB∧T∈WordB→S++T=x∈0..^S+T⟼ifx∈0..^SS⁡xT⁡x−S
2 wrdf ⊢S∈WordB→S:0..^S⟶B
3 2 ad2antrr ⊢S∈WordB∧T∈WordB∧x∈0..^S+T→S:0..^S⟶B
4 3 ffvelrnda ⊢S∈WordB∧T∈WordB∧x∈0..^S+T∧x∈0..^S→S⁡x∈B
5 wrdf ⊢T∈WordB→T:0..^T⟶B
6 5 ad3antlr ⊢S∈WordB∧T∈WordB∧x∈0..^S+T∧¬x∈0..^S→T:0..^T⟶B
7 simpr ⊢S∈WordB∧T∈WordB∧x∈0..^S+T→x∈0..^S+T
8 7 anim1i ⊢S∈WordB∧T∈WordB∧x∈0..^S+T∧¬x∈0..^S→x∈0..^S+T∧¬x∈0..^S
9 lencl ⊢S∈WordB→S∈ℕ0
10 9 nn0zd ⊢S∈WordB→S∈ℤ
11 lencl ⊢T∈WordB→T∈ℕ0
12 11 nn0zd ⊢T∈WordB→T∈ℤ
13 10 12 anim12i ⊢S∈WordB∧T∈WordB→S∈ℤ∧T∈ℤ
14 13 ad2antrr ⊢S∈WordB∧T∈WordB∧x∈0..^S+T∧¬x∈0..^S→S∈ℤ∧T∈ℤ
15 fzocatel ⊢x∈0..^S+T∧¬x∈0..^S∧S∈ℤ∧T∈ℤ→x−S∈0..^T
16 8 14 15 syl2anc ⊢S∈WordB∧T∈WordB∧x∈0..^S+T∧¬x∈0..^S→x−S∈0..^T
17 6 16 ffvelrnd ⊢S∈WordB∧T∈WordB∧x∈0..^S+T∧¬x∈0..^S→T⁡x−S∈B
18 4 17 ifclda ⊢S∈WordB∧T∈WordB∧x∈0..^S+T→ifx∈0..^SS⁡xT⁡x−S∈B
19 18 fmpttd ⊢S∈WordB∧T∈WordB→x∈0..^S+T⟼ifx∈0..^SS⁡xT⁡x−S:0..^S+T⟶B
20 iswrdi ⊢x∈0..^S+T⟼ifx∈0..^SS⁡xT⁡x−S:0..^S+T⟶B→x∈0..^S+T⟼ifx∈0..^SS⁡xT⁡x−S∈WordB
21 19 20 syl ⊢S∈WordB∧T∈WordB→x∈0..^S+T⟼ifx∈0..^SS⁡xT⁡x−S∈WordB
22 1 21 eqeltrd ⊢S∈WordB∧T∈WordB→S++T∈WordB