Theorem ccat2s1p2

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

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

Proof

Step	Hyp	Ref	Expression
1		s1cli	|- <" X "> e. Word _V
2		s1cli	|- <" Y "> e. Word _V
3		1z	|- 1 e. ZZ
4		2z	|- 2 e. ZZ
5		1lt2	|- 1 < 2
6		fzolb	|- ( 1 e. ( 1 ..^ 2 ) <-> ( 1 e. ZZ /\ 2 e. ZZ /\ 1 < 2 ) )
7	3 4 5 6	mpbir3an	|- 1 e. ( 1 ..^ 2 )
8		s1len	|- ( # ` <" X "> ) = 1
9		s1len	|- ( # ` <" Y "> ) = 1
10	8 9	oveq12i	|- ( ( # ` <" X "> ) + ( # ` <" Y "> ) ) = ( 1 + 1 )
11		1p1e2	|- ( 1 + 1 ) = 2
12	10 11	eqtri	|- ( ( # ` <" X "> ) + ( # ` <" Y "> ) ) = 2
13	8 12	oveq12i	|- ( ( # ` <" X "> ) ..^ ( ( # ` <" X "> ) + ( # ` <" Y "> ) ) ) = ( 1 ..^ 2 )
14	7 13	eleqtrri	|- 1 e. ( ( # ` <" X "> ) ..^ ( ( # ` <" X "> ) + ( # ` <" Y "> ) ) )
15		ccatval2	|- ( ( <" X "> e. Word _V /\ <" Y "> e. Word _V /\ 1 e. ( ( # ` <" X "> ) ..^ ( ( # ` <" X "> ) + ( # ` <" Y "> ) ) ) ) -> ( ( <" X "> ++ <" Y "> ) ` 1 ) = ( <" Y "> ` ( 1 - ( # ` <" X "> ) ) ) )
16	1 2 14 15	mp3an	|- ( ( <" X "> ++ <" Y "> ) ` 1 ) = ( <" Y "> ` ( 1 - ( # ` <" X "> ) ) )
17	8	oveq2i	|- ( 1 - ( # ` <" X "> ) ) = ( 1 - 1 )
18		1m1e0	|- ( 1 - 1 ) = 0
19	17 18	eqtri	|- ( 1 - ( # ` <" X "> ) ) = 0
20	19	fveq2i	|- ( <" Y "> ` ( 1 - ( # ` <" X "> ) ) ) = ( <" Y "> ` 0 )
21	16 20	eqtri	|- ( ( <" X "> ++ <" Y "> ) ` 1 ) = ( <" Y "> ` 0 )
22		s1fv	|- ( Y e. V -> ( <" Y "> ` 0 ) = Y )
23	21 22	eqtrid	|- ( Y e. V -> ( ( <" X "> ++ <" Y "> ) ` 1 ) = Y )