Metamath Proof Explorer

Theorem wrdlenccats1lenm1

Description: The length of a word is the length of the word concatenated with a singleton word minus 1. (Contributed by AV, 28-Jun-2018) (Revised by AV, 5-Mar-2022)

Ref Expression
Assertion wrdlenccats1lenm1 ⊢ W ∈ Word V → W ++ ⟨“ S ”⟩ − 1 = W

Proof

Step Hyp Ref Expression
1 ccatws1len ⊢ W ∈ Word V → W ++ ⟨“ S ”⟩ = W + 1
2 1 oveq1d ⊢ W ∈ Word V → W ++ ⟨“ S ”⟩ − 1 = W + 1 - 1
3 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
4 3 nn0cnd ⊢ W ∈ Word V → W ∈ ℂ
5 pncan1 ⊢ W ∈ ℂ → W + 1 - 1 = W
6 4 5 syl ⊢ W ∈ Word V → W + 1 - 1 = W
7 2 6 eqtrd ⊢ W ∈ Word V → W ++ ⟨“ S ”⟩ − 1 = W