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 ∈ Word A ∧ 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 ∈ Word A → Fun ⁡ F ∧ W ∈ Word A
3 2 ancoms ⊢ W ∈ Word A ∧ F : A ⟶ B → Fun ⁡ F ∧ W ∈ Word A
4 3 3adant2 ⊢ W ∈ Word A ∧ W ≠ ∅ ∧ F : A ⟶ B → Fun ⁡ F ∧ W ∈ Word A
5 cofunexg ⊢ Fun ⁡ F ∧ W ∈ Word A → F ∘ W ∈ V
6 lsw ⊢ F ∘ W ∈ V → lastS ⁡ F ∘ W = F ∘ W ⁡ F ∘ W − 1
7 4 5 6 3syl ⊢ W ∈ Word A ∧ W ≠ ∅ ∧ F : A ⟶ B → lastS ⁡ F ∘ W = F ∘ W ⁡ F ∘ W − 1
8 lenco ⊢ W ∈ Word A ∧ F : A ⟶ B → F ∘ W = W
9 8 3adant2 ⊢ W ∈ Word A ∧ W ≠ ∅ ∧ F : A ⟶ B → F ∘ W = W
10 9 fvoveq1d ⊢ W ∈ Word A ∧ W ≠ ∅ ∧ F : A ⟶ B → F ∘ W ⁡ F ∘ W − 1 = F ∘ W ⁡ W − 1
11 wrdf ⊢ W ∈ Word A → W : 0 ..^ W ⟶ A
12 11 adantr ⊢ W ∈ Word A ∧ W ≠ ∅ → W : 0 ..^ W ⟶ A
13 lennncl ⊢ W ∈ Word A ∧ W ≠ ∅ → W ∈ ℕ
14 fzo0end ⊢ W ∈ ℕ → W − 1 ∈ 0 ..^ W
15 13 14 syl ⊢ W ∈ Word A ∧ W ≠ ∅ → W − 1 ∈ 0 ..^ W
16 12 15 jca ⊢ W ∈ Word A ∧ W ≠ ∅ → W : 0 ..^ W ⟶ A ∧ W − 1 ∈ 0 ..^ W
17 16 3adant3 ⊢ W ∈ Word A ∧ 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 ∈ Word A ∧ W ≠ ∅ ∧ F : A ⟶ B → F ∘ W ⁡ W − 1 = F ⁡ W ⁡ W − 1
20 lsw ⊢ W ∈ Word A → lastS ⁡ W = W ⁡ W − 1
21 20 3ad2ant1 ⊢ W ∈ Word A ∧ W ≠ ∅ ∧ F : A ⟶ B → lastS ⁡ W = W ⁡ W − 1
22 21 eqcomd ⊢ W ∈ Word A ∧ W ≠ ∅ ∧ F : A ⟶ B → W ⁡ W − 1 = lastS ⁡ W
23 22 fveq2d ⊢ W ∈ Word A ∧ W ≠ ∅ ∧ F : A ⟶ B → F ⁡ W ⁡ W − 1 = F ⁡ lastS ⁡ W
24 19 23 eqtrd ⊢ W ∈ Word A ∧ W ≠ ∅ ∧ F : A ⟶ B → F ∘ W ⁡ W − 1 = F ⁡ lastS ⁡ W
25 7 10 24 3eqtrd ⊢ W ∈ Word A ∧ W ≠ ∅ ∧ F : A ⟶ B → lastS ⁡ F ∘ W = F ⁡ lastS ⁡ W