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 ∈ Word B ∧ T ∈ Word B → S ++ T ∈ Word B

Proof

Step Hyp Ref Expression
1 ccatfval ⊢ S ∈ Word B ∧ T ∈ Word B → S ++ T = x ∈ 0 ..^ S + T ⟼ if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S
2 wrdf ⊢ S ∈ Word B → S : 0 ..^ S ⟶ B
3 2 ad2antrr ⊢ S ∈ Word B ∧ T ∈ Word B ∧ x ∈ 0 ..^ S + T → S : 0 ..^ S ⟶ B
4 3 ffvelcdmda ⊢ S ∈ Word B ∧ T ∈ Word B ∧ x ∈ 0 ..^ S + T ∧ x ∈ 0 ..^ S → S ⁡ x ∈ B
5 wrdf ⊢ T ∈ Word B → T : 0 ..^ T ⟶ B
6 5 ad3antlr ⊢ S ∈ Word B ∧ T ∈ Word B ∧ x ∈ 0 ..^ S + T ∧ ¬ x ∈ 0 ..^ S → T : 0 ..^ T ⟶ B
7 simpr ⊢ S ∈ Word B ∧ T ∈ Word B ∧ x ∈ 0 ..^ S + T → x ∈ 0 ..^ S + T
8 7 anim1i ⊢ S ∈ Word B ∧ T ∈ Word B ∧ x ∈ 0 ..^ S + T ∧ ¬ x ∈ 0 ..^ S → x ∈ 0 ..^ S + T ∧ ¬ x ∈ 0 ..^ S
9 lencl ⊢ S ∈ Word B → S ∈ ℕ 0
10 9 nn0zd ⊢ S ∈ Word B → S ∈ ℤ
11 lencl ⊢ T ∈ Word B → T ∈ ℕ 0
12 11 nn0zd ⊢ T ∈ Word B → T ∈ ℤ
13 10 12 anim12i ⊢ S ∈ Word B ∧ T ∈ Word B → S ∈ ℤ ∧ T ∈ ℤ
14 13 ad2antrr ⊢ S ∈ Word B ∧ T ∈ Word B ∧ 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 ∈ Word B ∧ T ∈ Word B ∧ x ∈ 0 ..^ S + T ∧ ¬ x ∈ 0 ..^ S → x − S ∈ 0 ..^ T
17 6 16 ffvelcdmd ⊢ S ∈ Word B ∧ T ∈ Word B ∧ x ∈ 0 ..^ S + T ∧ ¬ x ∈ 0 ..^ S → T ⁡ x − S ∈ B
18 4 17 ifclda ⊢ S ∈ Word B ∧ T ∈ Word B ∧ x ∈ 0 ..^ S + T → if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S ∈ B
19 18 fmpttd ⊢ S ∈ Word B ∧ T ∈ Word B → x ∈ 0 ..^ S + T ⟼ if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S : 0 ..^ S + T ⟶ B
20 iswrdi ⊢ x ∈ 0 ..^ S + T ⟼ if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S : 0 ..^ S + T ⟶ B → x ∈ 0 ..^ S + T ⟼ if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S ∈ Word B
21 19 20 syl ⊢ S ∈ Word B ∧ T ∈ Word B → x ∈ 0 ..^ S + T ⟼ if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S ∈ Word B
22 1 21 eqeltrd ⊢ S ∈ Word B ∧ T ∈ Word B → S ++ T ∈ Word B