Metamath Proof Explorer


Theorem lswccatn0lsw

Description: The last symbol of a word concatenated with a nonempty word is the last symbol of the nonempty word. (Contributed by AV, 22-Oct-2018) (Proof shortened by AV, 1-May-2020)

Ref Expression
Assertion lswccatn0lsw
|- ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> ( lastS ` ( A ++ B ) ) = ( lastS ` B ) )

Proof

Step Hyp Ref Expression
1 ccatlen
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( # ` ( A ++ B ) ) = ( ( # ` A ) + ( # ` B ) ) )
2 1 oveq1d
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( # ` ( A ++ B ) ) - 1 ) = ( ( ( # ` A ) + ( # ` B ) ) - 1 ) )
3 2 3adant3
 |-  ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> ( ( # ` ( A ++ B ) ) - 1 ) = ( ( ( # ` A ) + ( # ` B ) ) - 1 ) )
4 lencl
 |-  ( A e. Word V -> ( # ` A ) e. NN0 )
5 4 nn0zd
 |-  ( A e. Word V -> ( # ` A ) e. ZZ )
6 lennncl
 |-  ( ( B e. Word V /\ B =/= (/) ) -> ( # ` B ) e. NN )
7 simpl
 |-  ( ( ( # ` A ) e. ZZ /\ ( # ` B ) e. NN ) -> ( # ` A ) e. ZZ )
8 nnz
 |-  ( ( # ` B ) e. NN -> ( # ` B ) e. ZZ )
9 zaddcl
 |-  ( ( ( # ` A ) e. ZZ /\ ( # ` B ) e. ZZ ) -> ( ( # ` A ) + ( # ` B ) ) e. ZZ )
10 8 9 sylan2
 |-  ( ( ( # ` A ) e. ZZ /\ ( # ` B ) e. NN ) -> ( ( # ` A ) + ( # ` B ) ) e. ZZ )
11 zre
 |-  ( ( # ` A ) e. ZZ -> ( # ` A ) e. RR )
12 nnrp
 |-  ( ( # ` B ) e. NN -> ( # ` B ) e. RR+ )
13 ltaddrp
 |-  ( ( ( # ` A ) e. RR /\ ( # ` B ) e. RR+ ) -> ( # ` A ) < ( ( # ` A ) + ( # ` B ) ) )
14 11 12 13 syl2an
 |-  ( ( ( # ` A ) e. ZZ /\ ( # ` B ) e. NN ) -> ( # ` A ) < ( ( # ` A ) + ( # ` B ) ) )
15 7 10 14 3jca
 |-  ( ( ( # ` A ) e. ZZ /\ ( # ` B ) e. NN ) -> ( ( # ` A ) e. ZZ /\ ( ( # ` A ) + ( # ` B ) ) e. ZZ /\ ( # ` A ) < ( ( # ` A ) + ( # ` B ) ) ) )
16 5 6 15 syl2an
 |-  ( ( A e. Word V /\ ( B e. Word V /\ B =/= (/) ) ) -> ( ( # ` A ) e. ZZ /\ ( ( # ` A ) + ( # ` B ) ) e. ZZ /\ ( # ` A ) < ( ( # ` A ) + ( # ` B ) ) ) )
17 16 3impb
 |-  ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> ( ( # ` A ) e. ZZ /\ ( ( # ` A ) + ( # ` B ) ) e. ZZ /\ ( # ` A ) < ( ( # ` A ) + ( # ` B ) ) ) )
18 fzolb
 |-  ( ( # ` A ) e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) <-> ( ( # ` A ) e. ZZ /\ ( ( # ` A ) + ( # ` B ) ) e. ZZ /\ ( # ` A ) < ( ( # ` A ) + ( # ` B ) ) ) )
19 17 18 sylibr
 |-  ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> ( # ` A ) e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) )
20 fzoend
 |-  ( ( # ` A ) e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) -> ( ( ( # ` A ) + ( # ` B ) ) - 1 ) e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) )
21 19 20 syl
 |-  ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> ( ( ( # ` A ) + ( # ` B ) ) - 1 ) e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) )
22 3 21 eqeltrd
 |-  ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> ( ( # ` ( A ++ B ) ) - 1 ) e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) )
23 ccatval2
 |-  ( ( A e. Word V /\ B e. Word V /\ ( ( # ` ( A ++ B ) ) - 1 ) e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) ) -> ( ( A ++ B ) ` ( ( # ` ( A ++ B ) ) - 1 ) ) = ( B ` ( ( ( # ` ( A ++ B ) ) - 1 ) - ( # ` A ) ) ) )
24 22 23 syld3an3
 |-  ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> ( ( A ++ B ) ` ( ( # ` ( A ++ B ) ) - 1 ) ) = ( B ` ( ( ( # ` ( A ++ B ) ) - 1 ) - ( # ` A ) ) ) )
25 2 oveq1d
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( ( # ` ( A ++ B ) ) - 1 ) - ( # ` A ) ) = ( ( ( ( # ` A ) + ( # ` B ) ) - 1 ) - ( # ` A ) ) )
26 4 nn0cnd
 |-  ( A e. Word V -> ( # ` A ) e. CC )
27 lencl
 |-  ( B e. Word V -> ( # ` B ) e. NN0 )
28 27 nn0cnd
 |-  ( B e. Word V -> ( # ` B ) e. CC )
29 addcl
 |-  ( ( ( # ` A ) e. CC /\ ( # ` B ) e. CC ) -> ( ( # ` A ) + ( # ` B ) ) e. CC )
30 1cnd
 |-  ( ( ( # ` A ) e. CC /\ ( # ` B ) e. CC ) -> 1 e. CC )
31 simpl
 |-  ( ( ( # ` A ) e. CC /\ ( # ` B ) e. CC ) -> ( # ` A ) e. CC )
32 29 30 31 sub32d
 |-  ( ( ( # ` A ) e. CC /\ ( # ` B ) e. CC ) -> ( ( ( ( # ` A ) + ( # ` B ) ) - 1 ) - ( # ` A ) ) = ( ( ( ( # ` A ) + ( # ` B ) ) - ( # ` A ) ) - 1 ) )
33 pncan2
 |-  ( ( ( # ` A ) e. CC /\ ( # ` B ) e. CC ) -> ( ( ( # ` A ) + ( # ` B ) ) - ( # ` A ) ) = ( # ` B ) )
34 33 oveq1d
 |-  ( ( ( # ` A ) e. CC /\ ( # ` B ) e. CC ) -> ( ( ( ( # ` A ) + ( # ` B ) ) - ( # ` A ) ) - 1 ) = ( ( # ` B ) - 1 ) )
35 32 34 eqtrd
 |-  ( ( ( # ` A ) e. CC /\ ( # ` B ) e. CC ) -> ( ( ( ( # ` A ) + ( # ` B ) ) - 1 ) - ( # ` A ) ) = ( ( # ` B ) - 1 ) )
36 26 28 35 syl2an
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( ( ( # ` A ) + ( # ` B ) ) - 1 ) - ( # ` A ) ) = ( ( # ` B ) - 1 ) )
37 25 36 eqtrd
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( ( # ` ( A ++ B ) ) - 1 ) - ( # ` A ) ) = ( ( # ` B ) - 1 ) )
38 37 3adant3
 |-  ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> ( ( ( # ` ( A ++ B ) ) - 1 ) - ( # ` A ) ) = ( ( # ` B ) - 1 ) )
39 38 fveq2d
 |-  ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> ( B ` ( ( ( # ` ( A ++ B ) ) - 1 ) - ( # ` A ) ) ) = ( B ` ( ( # ` B ) - 1 ) ) )
40 24 39 eqtrd
 |-  ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> ( ( A ++ B ) ` ( ( # ` ( A ++ B ) ) - 1 ) ) = ( B ` ( ( # ` B ) - 1 ) ) )
41 ovex
 |-  ( A ++ B ) e. _V
42 lsw
 |-  ( ( A ++ B ) e. _V -> ( lastS ` ( A ++ B ) ) = ( ( A ++ B ) ` ( ( # ` ( A ++ B ) ) - 1 ) ) )
43 41 42 mp1i
 |-  ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> ( lastS ` ( A ++ B ) ) = ( ( A ++ B ) ` ( ( # ` ( A ++ B ) ) - 1 ) ) )
44 lsw
 |-  ( B e. Word V -> ( lastS ` B ) = ( B ` ( ( # ` B ) - 1 ) ) )
45 44 3ad2ant2
 |-  ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> ( lastS ` B ) = ( B ` ( ( # ` B ) - 1 ) ) )
46 40 43 45 3eqtr4d
 |-  ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> ( lastS ` ( A ++ B ) ) = ( lastS ` B ) )