Metamath Proof Explorer

Theorem ccat2s1p2OLD

Description: Obsolete version of ccat2s1p2 as of 20-Jan-2024. Extract the second 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 ccat2s1p2OLD 
|- ( ( X e. V /\ Y e. V ) -> ( ( <" X "> ++ <" Y "> ) ` 1 ) = Y )

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 1z 
 |-  1 e. ZZ
6 2z 
 |-  2 e. ZZ
7 1lt2 
 |-  1 < 2
8 fzolb 
 |-  ( 1 e. ( 1 ..^ 2 ) <-> ( 1 e. ZZ /\ 2 e. ZZ /\ 1 < 2 ) )
9 5 6 7 8 mpbir3an 
 |-  1 e. ( 1 ..^ 2 )
10 s1len 
 |-  ( # ` <" X "> ) = 1
11 s1len 
 |-  ( # ` <" Y "> ) = 1
12 10 11 oveq12i 
 |-  ( ( # ` <" X "> ) + ( # ` <" Y "> ) ) = ( 1 + 1 )
13 1p1e2 
 |-  ( 1 + 1 ) = 2
14 12 13 eqtri 
 |-  ( ( # ` <" X "> ) + ( # ` <" Y "> ) ) = 2
15 10 14 oveq12i 
 |-  ( ( # ` <" X "> ) ..^ ( ( # ` <" X "> ) + ( # ` <" Y "> ) ) ) = ( 1 ..^ 2 )
16 9 15 eleqtrri 
 |-  1 e. ( ( # ` <" X "> ) ..^ ( ( # ` <" X "> ) + ( # ` <" Y "> ) ) )
17 16 a1i 
 |-  ( ( X e. V /\ Y e. V ) -> 1 e. ( ( # ` <" X "> ) ..^ ( ( # ` <" X "> ) + ( # ` <" Y "> ) ) ) )
18 ccatval2 
 |-  ( ( <" X "> e. Word V /\ <" Y "> e. Word V /\ 1 e. ( ( # ` <" X "> ) ..^ ( ( # ` <" X "> ) + ( # ` <" Y "> ) ) ) ) -> ( ( <" X "> ++ <" Y "> ) ` 1 ) = ( <" Y "> ` ( 1 - ( # ` <" X "> ) ) ) )
19 2 4 17 18 syl3anc 
 |-  ( ( X e. V /\ Y e. V ) -> ( ( <" X "> ++ <" Y "> ) ` 1 ) = ( <" Y "> ` ( 1 - ( # ` <" X "> ) ) ) )
20 10 oveq2i 
 |-  ( 1 - ( # ` <" X "> ) ) = ( 1 - 1 )
21 1m1e0 
 |-  ( 1 - 1 ) = 0
22 20 21 eqtri 
 |-  ( 1 - ( # ` <" X "> ) ) = 0
23 22 a1i 
 |-  ( Y e. V -> ( 1 - ( # ` <" X "> ) ) = 0 )
24 23 fveq2d 
 |-  ( Y e. V -> ( <" Y "> ` ( 1 - ( # ` <" X "> ) ) ) = ( <" Y "> ` 0 ) )
25 s1fv 
 |-  ( Y e. V -> ( <" Y "> ` 0 ) = Y )
26 24 25 eqtrd 
 |-  ( Y e. V -> ( <" Y "> ` ( 1 - ( # ` <" X "> ) ) ) = Y )
27 26 adantl 
 |-  ( ( X e. V /\ Y e. V ) -> ( <" Y "> ` ( 1 - ( # ` <" X "> ) ) ) = Y )
28 19 27 eqtrd 
 |-  ( ( X e. V /\ Y e. V ) -> ( ( <" X "> ++ <" Y "> ) ` 1 ) = Y )