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∈WordA∧W≠∅∧F:A⟶B→lastS⁡F∘W=F⁡lastS⁡W

Proof

Step Hyp Ref Expression
1 ffun ⊢F:A⟶B→Fun⁡F
2 1 anim1i ⊢F:A⟶B∧W∈WordA→Fun⁡F∧W∈WordA
3 2 ancoms ⊢W∈WordA∧F:A⟶B→Fun⁡F∧W∈WordA
4 3 3adant2 ⊢W∈WordA∧W≠∅∧F:A⟶B→Fun⁡F∧W∈WordA
5 cofunexg ⊢Fun⁡F∧W∈WordA→F∘W∈V
6 lsw ⊢F∘W∈V→lastS⁡F∘W=F∘W⁡F∘W−1
7 4 5 6 3syl ⊢W∈WordA∧W≠∅∧F:A⟶B→lastS⁡F∘W=F∘W⁡F∘W−1
8 lenco ⊢W∈WordA∧F:A⟶B→F∘W=W
9 8 3adant2 ⊢W∈WordA∧W≠∅∧F:A⟶B→F∘W=W
10 9 fvoveq1d ⊢W∈WordA∧W≠∅∧F:A⟶B→F∘W⁡F∘W−1=F∘W⁡W−1
11 wrdf ⊢W∈WordA→W:0..^W⟶A
12 11 adantr ⊢W∈WordA∧W≠∅→W:0..^W⟶A
13 lennncl ⊢W∈WordA∧W≠∅→W∈ℕ
14 fzo0end ⊢W∈ℕ→W−1∈0..^W
15 13 14 syl ⊢W∈WordA∧W≠∅→W−1∈0..^W
16 12 15 jca ⊢W∈WordA∧W≠∅→W:0..^W⟶A∧W−1∈0..^W
17 16 3adant3 ⊢W∈WordA∧W≠∅∧F:A⟶B→W:0..^W⟶A∧W−1∈0..^W
18 fvco3 ⊢W:0..^W⟶A∧W−1∈0..^W→F∘W⁡W−1=F⁡W⁡W−1
19 17 18 syl ⊢W∈WordA∧W≠∅∧F:A⟶B→F∘W⁡W−1=F⁡W⁡W−1
20 lsw ⊢W∈WordA→lastS⁡W=W⁡W−1
21 20 3ad2ant1 ⊢W∈WordA∧W≠∅∧F:A⟶B→lastS⁡W=W⁡W−1
22 21 eqcomd ⊢W∈WordA∧W≠∅∧F:A⟶B→W⁡W−1=lastS⁡W
23 22 fveq2d ⊢W∈WordA∧W≠∅∧F:A⟶B→F⁡W⁡W−1=F⁡lastS⁡W
24 19 23 eqtrd ⊢W∈WordA∧W≠∅∧F:A⟶B→F∘W⁡W−1=F⁡lastS⁡W
25 7 10 24 3eqtrd ⊢W∈WordA∧W≠∅∧F:A⟶B→lastS⁡F∘W=F⁡lastS⁡W