Metamath Proof Explorer

Theorem ccats1pfxeq

Description: The last symbol of a word concatenated with the word with the last symbol removed results in the word itself. (Contributed by Alexander van der Vekens, 24-Oct-2018) (Revised by AV, 9-May-2020)

Ref Expression
Assertion ccats1pfxeq ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → W = U prefix W → U = W ++ ⟨“ lastS ⁡ U ”⟩

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ W = U prefix W → W ++ ⟨“ lastS ⁡ U ”⟩ = U prefix W ++ ⟨“ lastS ⁡ U ”⟩
2 1 adantl ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 ∧ W = U prefix W → W ++ ⟨“ lastS ⁡ U ”⟩ = U prefix W ++ ⟨“ lastS ⁡ U ”⟩
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 6 eqcomd ⊢ W ∈ Word V → W = W + 1 - 1
8 7 3ad2ant1 ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → W = W + 1 - 1
9 oveq1 ⊢ U = W + 1 → U − 1 = W + 1 - 1
10 9 eqcomd ⊢ U = W + 1 → W + 1 - 1 = U − 1
11 10 3ad2ant3 ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → W + 1 - 1 = U − 1
12 8 11 eqtrd ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → W = U − 1
13 12 oveq2d ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → U prefix W = U prefix U − 1
14 13 oveq1d ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → U prefix W ++ ⟨“ lastS ⁡ U ”⟩ = U prefix U − 1 ++ ⟨“ lastS ⁡ U ”⟩
15 simp2 ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → U ∈ Word V
16 nn0p1gt0 ⊢ W ∈ ℕ 0 → 0 < W + 1
17 3 16 syl ⊢ W ∈ Word V → 0 < W + 1
18 17 3ad2ant1 ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → 0 < W + 1
19 breq2 ⊢ U = W + 1 → 0 < U ↔ 0 < W + 1
20 19 3ad2ant3 ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → 0 < U ↔ 0 < W + 1
21 18 20 mpbird ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → 0 < U
22 hashneq0 ⊢ U ∈ Word V → 0 < U ↔ U ≠ ∅
23 22 3ad2ant2 ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → 0 < U ↔ U ≠ ∅
24 21 23 mpbid ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → U ≠ ∅
25 pfxlswccat ⊢ U ∈ Word V ∧ U ≠ ∅ → U prefix U − 1 ++ ⟨“ lastS ⁡ U ”⟩ = U
26 15 24 25 syl2anc ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → U prefix U − 1 ++ ⟨“ lastS ⁡ U ”⟩ = U
27 14 26 eqtrd ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → U prefix W ++ ⟨“ lastS ⁡ U ”⟩ = U
28 27 adantr ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 ∧ W = U prefix W → U prefix W ++ ⟨“ lastS ⁡ U ”⟩ = U
29 2 28 eqtr2d ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 ∧ W = U prefix W → U = W ++ ⟨“ lastS ⁡ U ”⟩
30 29 ex ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → W = U prefix W → U = W ++ ⟨“ lastS ⁡ U ”⟩