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 ) )