Metamath Proof Explorer


Theorem ccat2s1fvwALTOLD

Description: Obsolete version of ccat2s1fvwALT as of 28-Jan-2024. Alternate proof of ccat2s1fvwOLD using words of length 2, see df-s2 . A symbol of the concatenation of a word with two single symbols corresponding to the symbol of the word. (Contributed by AV, 22-Sep-2018) (Proof shortened by Mario Carneiro/AV, 21-Oct-2018) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion ccat2s1fvwALTOLD
|- ( ( ( 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 simp1
 |-  ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> W e. Word V )
2 1 anim1i
 |-  ( ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) /\ ( X e. V /\ Y e. V ) ) -> ( W e. Word V /\ ( X e. V /\ Y e. V ) ) )
3 3anass
 |-  ( ( W e. Word V /\ X e. V /\ Y e. V ) <-> ( W e. Word V /\ ( X e. V /\ Y e. V ) ) )
4 2 3 sylibr
 |-  ( ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) /\ ( X e. V /\ Y e. V ) ) -> ( W e. Word V /\ X e. V /\ Y e. V ) )
5 ccatw2s1ccatws2OLD
 |-  ( ( W e. Word V /\ X e. V /\ Y e. V ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) = ( W ++ <" X Y "> ) )
6 5 fveq1d
 |-  ( ( W e. Word V /\ X e. V /\ Y e. V ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` I ) = ( ( W ++ <" X Y "> ) ` I ) )
7 4 6 syl
 |-  ( ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` I ) = ( ( W ++ <" X Y "> ) ` I ) )
8 1 adantr
 |-  ( ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) /\ ( X e. V /\ Y e. V ) ) -> W e. Word V )
9 s2cl
 |-  ( ( X e. V /\ Y e. V ) -> <" X Y "> e. Word V )
10 9 adantl
 |-  ( ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) /\ ( X e. V /\ Y e. V ) ) -> <" X Y "> e. Word V )
11 simp2
 |-  ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> I e. NN0 )
12 lencl
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
13 12 nn0zd
 |-  ( W e. Word V -> ( # ` W ) e. ZZ )
14 13 3ad2ant1
 |-  ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> ( # ` W ) e. ZZ )
15 simp3
 |-  ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> I < ( # ` W ) )
16 elfzo0z
 |-  ( I e. ( 0 ..^ ( # ` W ) ) <-> ( I e. NN0 /\ ( # ` W ) e. ZZ /\ I < ( # ` W ) ) )
17 11 14 15 16 syl3anbrc
 |-  ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> I e. ( 0 ..^ ( # ` W ) ) )
18 17 adantr
 |-  ( ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) /\ ( X e. V /\ Y e. V ) ) -> I e. ( 0 ..^ ( # ` W ) ) )
19 ccatval1
 |-  ( ( W e. Word V /\ <" X Y "> e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" X Y "> ) ` I ) = ( W ` I ) )
20 8 10 18 19 syl3anc
 |-  ( ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) /\ ( X e. V /\ Y e. V ) ) -> ( ( W ++ <" X Y "> ) ` I ) = ( W ` I ) )
21 7 20 eqtrd
 |-  ( ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` I ) = ( W ` I ) )