Metamath Proof Explorer

Theorem ccat2s1lenOLD

Description: Obsolete version of ccat2s1len as of 14-Jan-2024. The length of the concatenation of two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ccat2s1lenOLD 
|- ( ( X e. V /\ Y e. V ) -> ( # ` ( <" X "> ++ <" Y "> ) ) = 2 )

Proof

Step Hyp Ref Expression
1 s1cl 
 |-  ( X e. V -> <" X "> e. Word V )
2 s1cl 
 |-  ( Y e. V -> <" Y "> e. Word V )
3 ccatlenOLD 
 |-  ( ( <" 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 syl2an 
 |-  ( ( X e. V /\ Y e. V ) -> ( # ` ( <" X "> ++ <" Y "> ) ) = 2 )