Description: The length of the concatenation of a word with a singleton word. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Revised by AV, 4-Mar-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ccatws1len | |- ( W e. Word V -> ( # ` ( W ++ <" X "> ) ) = ( ( # ` W ) + 1 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | s1cli | |- <" X "> e. Word _V |
|
| 2 | ccatlen | |- ( ( W e. Word V /\ <" X "> e. Word _V ) -> ( # ` ( W ++ <" X "> ) ) = ( ( # ` W ) + ( # ` <" X "> ) ) ) |
|
| 3 | 1 2 | mpan2 | |- ( W e. Word V -> ( # ` ( W ++ <" X "> ) ) = ( ( # ` W ) + ( # ` <" X "> ) ) ) |
| 4 | s1len | |- ( # ` <" X "> ) = 1 |
|
| 5 | 4 | oveq2i | |- ( ( # ` W ) + ( # ` <" X "> ) ) = ( ( # ` W ) + 1 ) |
| 6 | 3 5 | eqtrdi | |- ( W e. Word V -> ( # ` ( W ++ <" X "> ) ) = ( ( # ` W ) + 1 ) ) |