Metamath Proof Explorer

Theorem ccatws1ls

Description: The last symbol of the concatenation of a word with a singleton word is the symbol of the singleton word. (Contributed by AV, 29-Sep-2018) (Proof shortened by AV, 14-Oct-2018)

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

Proof

Step	Hyp	Ref	Expression
1		eqidd	\|- ( ( W e. Word V /\ X e. V ) -> ( # ` W ) = ( # ` W ) )
2		ccats1val2	\|- ( ( W e. Word V /\ X e. V /\ ( # ` W ) = ( # ` W ) ) -> ( ( W ++ <" X "> ) ` ( # ` W ) ) = X )
3	1 2	mpd3an3	\|- ( ( W e. Word V /\ X e. V ) -> ( ( W ++ <" X "> ) ` ( # ` W ) ) = X )

Step

Hyp

Ref

Expression

eqidd

 |-  ( ( W e. Word V /\ X e. V ) -> ( # ` W ) = ( # ` W ) )

ccats1val2

 |-  ( ( W e. Word V /\ X e. V /\ ( # ` W ) = ( # ` W ) ) -> ( ( W ++ <" X "> ) ` ( # ` W ) ) = X )

1 2

mpd3an3

 |-  ( ( W e. Word V /\ X e. V ) -> ( ( W ++ <" X "> ) ` ( # ` W ) ) = X )