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 ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑊 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( lastS ‘ ( 𝐹 ∘ 𝑊 ) ) = ( 𝐹 ‘ ( lastS ‘ 𝑊 ) ) )

Proof

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