Theorem ccat2s1fvwALT

Description: Alternate proof of ccat2s1fvw 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) (Revised by AV, 28-Jan-2024) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ccatw2s1ccatws2	|- ( W e. Word V -> ( ( W ++ <" X "> ) ++ <" Y "> ) = ( W ++ <" X Y "> ) )
2	1	fveq1d	|- ( W e. Word V -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` I ) = ( ( W ++ <" X Y "> ) ` I ) )
3	2	3ad2ant1	|- ( ( 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		s2cli	|- <" X Y "> e. Word _V
6	5	a1i	|- ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> <" X Y "> e. Word _V )
7		simp2	|- ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> I e. NN0 )
8		lencl	|- ( W e. Word V -> ( # ` W ) e. NN0 )
9	8	nn0zd	|- ( W e. Word V -> ( # ` W ) e. ZZ )
10	9	3ad2ant1	|- ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> ( # ` W ) e. ZZ )
11		simp3	|- ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> I < ( # ` W ) )
12		elfzo0z	|- ( I e. ( 0 ..^ ( # ` W ) ) <-> ( I e. NN0 /\ ( # ` W ) e. ZZ /\ I < ( # ` W ) ) )
13	7 10 11 12	syl3anbrc	|- ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> I e. ( 0 ..^ ( # ` W ) ) )
14		ccatval1	|- ( ( W e. Word V /\ <" X Y "> e. Word _V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" X Y "> ) ` I ) = ( W ` I ) )
15	4 6 13 14	syl3anc	|- ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> ( ( W ++ <" X Y "> ) ` I ) = ( W ` I ) )
16	3 15	eqtrd	|- ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` I ) = ( W ` I ) )