This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )