Metamath Proof Explorer

Theorem ccat2s1fvwOLD

Description: Obsolete version of ccat2s1fvw as of 28-Jan-2024. 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) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ccatw2s1assOLD 
 |-  ( ( W e. Word V /\ X e. V /\ Y e. V ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) = ( W ++ ( <" X "> ++ <" Y "> ) ) )
2 1 3expb 
 |-  ( ( W e. Word V /\ ( X e. V /\ Y e. V ) ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) = ( W ++ ( <" X "> ++ <" Y "> ) ) )
3 2 3ad2antl1 
 |-  ( ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) /\ ( X e. V /\ Y e. V ) ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) = ( W ++ ( <" X "> ++ <" Y "> ) ) )
4 3 fveq1d 
 |-  ( ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` I ) = ( ( W ++ ( <" X "> ++ <" Y "> ) ) ` I ) )
5 simpl1 
 |-  ( ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) /\ ( X e. V /\ Y e. V ) ) -> W e. Word V )
6 ccat2s1cl 
 |-  ( ( X e. V /\ Y e. V ) -> ( <" X "> ++ <" Y "> ) e. Word V )
7 6 adantl 
 |-  ( ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) /\ ( X e. V /\ Y e. V ) ) -> ( <" 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 26 adantr 
 |-  ( ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) /\ ( X e. V /\ Y e. V ) ) -> I e. ( 0 ..^ ( # ` W ) ) )
28 ccatval1 
 |-  ( ( W e. Word V /\ ( <" X "> ++ <" Y "> ) e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ ( <" X "> ++ <" Y "> ) ) ` I ) = ( W ` I ) )
29 5 7 27 28 syl3anc 
 |-  ( ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) /\ ( X e. V /\ Y e. V ) ) -> ( ( W ++ ( <" X "> ++ <" Y "> ) ) ` I ) = ( W ` I ) )
30 4 29 eqtrd 
 |-  ( ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` I ) = ( W ` I ) )