Metamath Proof Explorer

Theorem ccat2s1p1

Description: Extract the first of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Revised by JJ, 20-Jan-2024)

Ref Expression
Assertion ccat2s1p1 
|- ( X e. V -> ( ( <" X "> ++ <" Y "> ) ` 0 ) = X )

Proof

Step Hyp Ref Expression
1 s1cli 
 |-  <" X "> e. Word _V
2 s1cli 
 |-  <" Y "> e. Word _V
3 s1len 
 |-  ( # ` <" X "> ) = 1
4 1nn 
 |-  1 e. NN
5 3 4 eqeltri 
 |-  ( # ` <" X "> ) e. NN
6 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( # ` <" X "> ) ) <-> ( # ` <" X "> ) e. NN )
7 5 6 mpbir 
 |-  0 e. ( 0 ..^ ( # ` <" X "> ) )
8 ccatval1 
 |-  ( ( <" X "> e. Word _V /\ <" Y "> e. Word _V /\ 0 e. ( 0 ..^ ( # ` <" X "> ) ) ) -> ( ( <" X "> ++ <" Y "> ) ` 0 ) = ( <" X "> ` 0 ) )
9 1 2 7 8 mp3an 
 |-  ( ( <" X "> ++ <" Y "> ) ` 0 ) = ( <" X "> ` 0 )
10 s1fv 
 |-  ( X e. V -> ( <" X "> ` 0 ) = X )
11 9 10 syl5eq 
 |-  ( X e. V -> ( ( <" X "> ++ <" Y "> ) ` 0 ) = X )