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 )