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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ccatfval | |
|
2 | 1 | fveq2d | |
3 | fvex | |
|
4 | fvex | |
|
5 | 3 4 | ifex | |
6 | eqid | |
|
7 | 5 6 | fnmpti | |
8 | hashfn | |
|
9 | 7 8 | mp1i | |
10 | lencl | |
|
11 | lencl | |
|
12 | nn0addcl | |
|
13 | 10 11 12 | syl2an | |
14 | hashfzo0 | |
|
15 | 13 14 | syl | |
16 | 2 9 15 | 3eqtrd | |