Description: The length of the concatenation of two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Revised by JJ, 14-Jan-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ccat2s1len | |- ( # ` ( <" X "> ++ <" Y "> ) ) = 2 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | s1cli | |- <" X "> e. Word _V |
|
| 2 | s1cli | |- <" Y "> e. Word _V |
|
| 3 | ccatlen | |- ( ( <" X "> e. Word _V /\ <" Y "> e. Word _V ) -> ( # ` ( <" X "> ++ <" Y "> ) ) = ( ( # ` <" X "> ) + ( # ` <" Y "> ) ) ) |
|
| 4 | s1len | |- ( # ` <" X "> ) = 1 |
|
| 5 | s1len | |- ( # ` <" Y "> ) = 1 |
|
| 6 | 4 5 | oveq12i | |- ( ( # ` <" X "> ) + ( # ` <" Y "> ) ) = ( 1 + 1 ) |
| 7 | 1p1e2 | |- ( 1 + 1 ) = 2 |
|
| 8 | 6 7 | eqtri | |- ( ( # ` <" X "> ) + ( # ` <" Y "> ) ) = 2 |
| 9 | 3 8 | eqtrdi | |- ( ( <" X "> e. Word _V /\ <" Y "> e. Word _V ) -> ( # ` ( <" X "> ++ <" Y "> ) ) = 2 ) |
| 10 | 1 2 9 | mp2an | |- ( # ` ( <" X "> ++ <" Y "> ) ) = 2 |