Metamath Proof Explorer


Theorem lswccats1

Description: The last symbol of a word concatenated with a singleton word is the symbol of the singleton word. (Contributed by AV, 6-Aug-2018) (Proof shortened by AV, 22-Oct-2018)

Ref Expression
Assertion lswccats1
|- ( ( W e. Word V /\ S e. V ) -> ( lastS ` ( W ++ <" S "> ) ) = S )

Proof

Step Hyp Ref Expression
1 simpl
 |-  ( ( W e. Word V /\ S e. V ) -> W e. Word V )
2 s1cl
 |-  ( S e. V -> <" S "> e. Word V )
3 2 adantl
 |-  ( ( W e. Word V /\ S e. V ) -> <" S "> e. Word V )
4 s1nz
 |-  <" S "> =/= (/)
5 4 a1i
 |-  ( ( W e. Word V /\ S e. V ) -> <" S "> =/= (/) )
6 lswccatn0lsw
 |-  ( ( W e. Word V /\ <" S "> e. Word V /\ <" S "> =/= (/) ) -> ( lastS ` ( W ++ <" S "> ) ) = ( lastS ` <" S "> ) )
7 1 3 5 6 syl3anc
 |-  ( ( W e. Word V /\ S e. V ) -> ( lastS ` ( W ++ <" S "> ) ) = ( lastS ` <" S "> ) )
8 lsws1
 |-  ( S e. V -> ( lastS ` <" S "> ) = S )
9 8 adantl
 |-  ( ( W e. Word V /\ S e. V ) -> ( lastS ` <" S "> ) = S )
10 7 9 eqtrd
 |-  ( ( W e. Word V /\ S e. V ) -> ( lastS ` ( W ++ <" S "> ) ) = S )