Metamath Proof Explorer

Theorem ccats1val1OLD

Description: Obsolete version of ccats1val1 as of 20-Jan-2024. Value of a symbol in the left half of a word concatenated with a single symbol. (Contributed by Alexander van der Vekens, 5-Aug-2018) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	ccats1val1OLD	\|- ( ( W e. Word V /\ S e. V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" S "> ) ` I ) = ( W ` I ) )

Proof

Step	Hyp	Ref	Expression
1		s1cl	\|- ( S e. V -> <" S "> e. Word V )
2		ccatval1OLD	\|- ( ( W e. Word V /\ <" S "> e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" S "> ) ` I ) = ( W ` I ) )
3	1 2	syl3an2	\|- ( ( W e. Word V /\ S e. V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" S "> ) ` I ) = ( W ` I ) )

Step

Hyp

Ref

Expression

s1cl

 |-  ( S e. V -> <" S "> e. Word V )

ccatval1OLD

 |-  ( ( W e. Word V /\ <" S "> e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" S "> ) ` I ) = ( W ` I ) )

1 2

syl3an2

 |-  ( ( W e. Word V /\ S e. V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" S "> ) ` I ) = ( W ` I ) )