This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )