Metamath Proof Explorer

Theorem lswco

Description: Mapping of (nonempty) words commutes with the "last symbol" operation. This theorem would not hold if W = (/) , ( F(/) ) =/= (/) and (/) e. A , because then ( lastS( F o. W ) ) = ( lastS(/) ) = (/) =/= ( F(/) ) = ( F ( lastSW ) ) . (Contributed by AV, 11-Nov-2018)

Ref Expression
Assertion lswco 
|- ( ( W e. Word A /\ W =/= (/) /\ F : A --> B ) -> ( lastS ` ( F o. W ) ) = ( F ` ( lastS ` W ) ) )

Proof

Step Hyp Ref Expression
1 ffun 
 |-  ( F : A --> B -> Fun F )
2 1 anim1i 
 |-  ( ( F : A --> B /\ W e. Word A ) -> ( Fun F /\ W e. Word A ) )
3 2 ancoms 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( Fun F /\ W e. Word A ) )
4 3 3adant2 
 |-  ( ( W e. Word A /\ W =/= (/) /\ F : A --> B ) -> ( Fun F /\ W e. Word A ) )
5 cofunexg 
 |-  ( ( Fun F /\ W e. Word A ) -> ( F o. W ) e. _V )
6 lsw 
 |-  ( ( F o. W ) e. _V -> ( lastS ` ( F o. W ) ) = ( ( F o. W ) ` ( ( # ` ( F o. W ) ) - 1 ) ) )
7 4 5 6 3syl 
 |-  ( ( W e. Word A /\ W =/= (/) /\ F : A --> B ) -> ( lastS ` ( F o. W ) ) = ( ( F o. W ) ` ( ( # ` ( F o. W ) ) - 1 ) ) )
8 lenco 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( # ` ( F o. W ) ) = ( # ` W ) )
9 8 3adant2 
 |-  ( ( W e. Word A /\ W =/= (/) /\ F : A --> B ) -> ( # ` ( F o. W ) ) = ( # ` W ) )
10 9 fvoveq1d 
 |-  ( ( W e. Word A /\ W =/= (/) /\ F : A --> B ) -> ( ( F o. W ) ` ( ( # ` ( F o. W ) ) - 1 ) ) = ( ( F o. W ) ` ( ( # ` W ) - 1 ) ) )
11 wrdf 
 |-  ( W e. Word A -> W : ( 0 ..^ ( # ` W ) ) --> A )
12 11 adantr 
 |-  ( ( W e. Word A /\ W =/= (/) ) -> W : ( 0 ..^ ( # ` W ) ) --> A )
13 lennncl 
 |-  ( ( W e. Word A /\ W =/= (/) ) -> ( # ` W ) e. NN )
14 fzo0end 
 |-  ( ( # ` W ) e. NN -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
15 13 14 syl 
 |-  ( ( W e. Word A /\ W =/= (/) ) -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
16 12 15 jca 
 |-  ( ( W e. Word A /\ W =/= (/) ) -> ( W : ( 0 ..^ ( # ` W ) ) --> A /\ ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) ) )
17 16 3adant3 
 |-  ( ( W e. Word A /\ W =/= (/) /\ F : A --> B ) -> ( W : ( 0 ..^ ( # ` W ) ) --> A /\ ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) ) )
18 fvco3 
 |-  ( ( W : ( 0 ..^ ( # ` W ) ) --> A /\ ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) ) -> ( ( F o. W ) ` ( ( # ` W ) - 1 ) ) = ( F ` ( W ` ( ( # ` W ) - 1 ) ) ) )
19 17 18 syl 
 |-  ( ( W e. Word A /\ W =/= (/) /\ F : A --> B ) -> ( ( F o. W ) ` ( ( # ` W ) - 1 ) ) = ( F ` ( W ` ( ( # ` W ) - 1 ) ) ) )
20 lsw 
 |-  ( W e. Word A -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
21 20 3ad2ant1 
 |-  ( ( W e. Word A /\ W =/= (/) /\ F : A --> B ) -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
22 21 eqcomd 
 |-  ( ( W e. Word A /\ W =/= (/) /\ F : A --> B ) -> ( W ` ( ( # ` W ) - 1 ) ) = ( lastS ` W ) )
23 22 fveq2d 
 |-  ( ( W e. Word A /\ W =/= (/) /\ F : A --> B ) -> ( F ` ( W ` ( ( # ` W ) - 1 ) ) ) = ( F ` ( lastS ` W ) ) )
24 19 23 eqtrd 
 |-  ( ( W e. Word A /\ W =/= (/) /\ F : A --> B ) -> ( ( F o. W ) ` ( ( # ` W ) - 1 ) ) = ( F ` ( lastS ` W ) ) )
25 7 10 24 3eqtrd 
 |-  ( ( W e. Word A /\ W =/= (/) /\ F : A --> B ) -> ( lastS ` ( F o. W ) ) = ( F ` ( lastS ` W ) ) )