Metamath Proof Explorer


Theorem ccat2s1p1OLD

Description: Obsolete version of ccat2s1p1 as of 20-Jan-2024. Extract the first of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 s1cl
 |-  ( X e. V -> <" X "> e. Word V )
2 1 adantr
 |-  ( ( X e. V /\ Y e. V ) -> <" X "> e. Word V )
3 s1cl
 |-  ( Y e. V -> <" Y "> e. Word V )
4 3 adantl
 |-  ( ( X e. V /\ Y e. V ) -> <" Y "> e. Word V )
5 s1len
 |-  ( # ` <" X "> ) = 1
6 5 a1i
 |-  ( X e. V -> ( # ` <" X "> ) = 1 )
7 1nn
 |-  1 e. NN
8 6 7 eqeltrdi
 |-  ( X e. V -> ( # ` <" X "> ) e. NN )
9 lbfzo0
 |-  ( 0 e. ( 0 ..^ ( # ` <" X "> ) ) <-> ( # ` <" X "> ) e. NN )
10 8 9 sylibr
 |-  ( X e. V -> 0 e. ( 0 ..^ ( # ` <" X "> ) ) )
11 10 adantr
 |-  ( ( X e. V /\ Y e. V ) -> 0 e. ( 0 ..^ ( # ` <" X "> ) ) )
12 ccatval1OLD
 |-  ( ( <" X "> e. Word V /\ <" Y "> e. Word V /\ 0 e. ( 0 ..^ ( # ` <" X "> ) ) ) -> ( ( <" X "> ++ <" Y "> ) ` 0 ) = ( <" X "> ` 0 ) )
13 2 4 11 12 syl3anc
 |-  ( ( X e. V /\ Y e. V ) -> ( ( <" X "> ++ <" Y "> ) ` 0 ) = ( <" X "> ` 0 ) )
14 s1fv
 |-  ( X e. V -> ( <" X "> ` 0 ) = X )
15 14 adantr
 |-  ( ( X e. V /\ Y e. V ) -> ( <" X "> ` 0 ) = X )
16 13 15 eqtrd
 |-  ( ( X e. V /\ Y e. V ) -> ( ( <" X "> ++ <" Y "> ) ` 0 ) = X )