Metamath Proof Explorer


Theorem ccatlen

Description: The length of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by JJ, 1-Jan-2024)

Ref Expression
Assertion ccatlen SWordATWordBS++T=S+T

Proof

Step Hyp Ref Expression
1 ccatfval SWordATWordBS++T=x0..^S+Tifx0..^SSxTxS
2 1 fveq2d SWordATWordBS++T=x0..^S+Tifx0..^SSxTxS
3 fvex SxV
4 fvex TxSV
5 3 4 ifex ifx0..^SSxTxSV
6 eqid x0..^S+Tifx0..^SSxTxS=x0..^S+Tifx0..^SSxTxS
7 5 6 fnmpti x0..^S+Tifx0..^SSxTxSFn0..^S+T
8 hashfn x0..^S+Tifx0..^SSxTxSFn0..^S+Tx0..^S+Tifx0..^SSxTxS=0..^S+T
9 7 8 mp1i SWordATWordBx0..^S+Tifx0..^SSxTxS=0..^S+T
10 lencl SWordAS0
11 lencl TWordBT0
12 nn0addcl S0T0S+T0
13 10 11 12 syl2an SWordATWordBS+T0
14 hashfzo0 S+T00..^S+T=S+T
15 13 14 syl SWordATWordB0..^S+T=S+T
16 2 9 15 3eqtrd SWordATWordBS++T=S+T