Metamath Proof Explorer

Theorem ccat2s1fvw

Description: Extract a symbol of a word from the concatenation of the word with two single symbols. (Contributed by AV, 22-Sep-2018) (Revised by AV, 13-Jan-2020) (Proof shortened by AV, 1-May-2020) (Revised by AV, 28-Jan-2024)

Ref Expression
Assertion ccat2s1fvw 
|- ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` I ) = ( W ` I ) )

Proof

Step Hyp Ref Expression
1 ccatw2s1ass 
 |-  ( W e. Word V -> ( ( W ++ <" X "> ) ++ <" Y "> ) = ( W ++ ( <" X "> ++ <" Y "> ) ) )
2 1 3ad2ant1 
 |-  ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) = ( W ++ ( <" X "> ++ <" Y "> ) ) )
3 2 fveq1d 
 |-  ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` I ) = ( ( W ++ ( <" X "> ++ <" Y "> ) ) ` I ) )
4 simp1 
 |-  ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> W e. Word V )
5 s1cli 
 |-  <" X "> e. Word _V
6 ccatws1clv 
 |-  ( <" X "> e. Word _V -> ( <" X "> ++ <" Y "> ) e. Word _V )
7 5 6 mp1i 
 |-  ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> ( <" X "> ++ <" Y "> ) e. Word _V )
8 simp2 
 |-  ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> I e. NN0 )
9 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
10 9 3ad2ant1 
 |-  ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> ( # ` W ) e. NN0 )
11 nn0ge0 
 |-  ( I e. NN0 -> 0 <_ I )
12 11 adantl 
 |-  ( ( W e. Word V /\ I e. NN0 ) -> 0 <_ I )
13 0red 
 |-  ( ( W e. Word V /\ I e. NN0 ) -> 0 e. RR )
14 nn0re 
 |-  ( I e. NN0 -> I e. RR )
15 14 adantl 
 |-  ( ( W e. Word V /\ I e. NN0 ) -> I e. RR )
16 9 nn0red 
 |-  ( W e. Word V -> ( # ` W ) e. RR )
17 16 adantr 
 |-  ( ( W e. Word V /\ I e. NN0 ) -> ( # ` W ) e. RR )
18 lelttr 
 |-  ( ( 0 e. RR /\ I e. RR /\ ( # ` W ) e. RR ) -> ( ( 0 <_ I /\ I < ( # ` W ) ) -> 0 < ( # ` W ) ) )
19 13 15 17 18 syl3anc 
 |-  ( ( W e. Word V /\ I e. NN0 ) -> ( ( 0 <_ I /\ I < ( # ` W ) ) -> 0 < ( # ` W ) ) )
20 12 19 mpand 
 |-  ( ( W e. Word V /\ I e. NN0 ) -> ( I < ( # ` W ) -> 0 < ( # ` W ) ) )
21 20 3impia 
 |-  ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> 0 < ( # ` W ) )
22 elnnnn0b 
 |-  ( ( # ` W ) e. NN <-> ( ( # ` W ) e. NN0 /\ 0 < ( # ` W ) ) )
23 10 21 22 sylanbrc 
 |-  ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> ( # ` W ) e. NN )
24 simp3 
 |-  ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> I < ( # ` W ) )
25 elfzo0 
 |-  ( I e. ( 0 ..^ ( # ` W ) ) <-> ( I e. NN0 /\ ( # ` W ) e. NN /\ I < ( # ` W ) ) )
26 8 23 24 25 syl3anbrc 
 |-  ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> I e. ( 0 ..^ ( # ` W ) ) )
27 ccatval1 
 |-  ( ( W e. Word V /\ ( <" X "> ++ <" Y "> ) e. Word _V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ ( <" X "> ++ <" Y "> ) ) ` I ) = ( W ` I ) )
28 4 7 26 27 syl3anc 
 |-  ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> ( ( W ++ ( <" X "> ++ <" Y "> ) ) ` I ) = ( W ` I ) )
29 3 28 eqtrd 
 |-  ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` I ) = ( W ` I ) )