# 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 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {U}\in \mathrm{Word}{V}\wedge \left|{U}\right|=\left|{W}\right|+1\right)\to \left({W}={U}\mathrm{prefix}\left|{W}\right|\to {U}={W}\mathrm{++}⟨“\mathrm{lastS}\left({U}\right)”⟩\right)$

### Proof

Step Hyp Ref Expression
1 oveq1 ${⊢}{W}={U}\mathrm{prefix}\left|{W}\right|\to {W}\mathrm{++}⟨“\mathrm{lastS}\left({U}\right)”⟩=\left({U}\mathrm{prefix}\left|{W}\right|\right)\mathrm{++}⟨“\mathrm{lastS}\left({U}\right)”⟩$
2 1 adantl ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge {U}\in \mathrm{Word}{V}\wedge \left|{U}\right|=\left|{W}\right|+1\right)\wedge {W}={U}\mathrm{prefix}\left|{W}\right|\right)\to {W}\mathrm{++}⟨“\mathrm{lastS}\left({U}\right)”⟩=\left({U}\mathrm{prefix}\left|{W}\right|\right)\mathrm{++}⟨“\mathrm{lastS}\left({U}\right)”⟩$
3 lencl ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|\in {ℕ}_{0}$
4 3 nn0cnd ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|\in ℂ$
5 pncan1 ${⊢}\left|{W}\right|\in ℂ\to \left|{W}\right|+1-1=\left|{W}\right|$
6 4 5 syl ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|+1-1=\left|{W}\right|$
7 6 eqcomd ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|=\left|{W}\right|+1-1$
8 7 3ad2ant1 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {U}\in \mathrm{Word}{V}\wedge \left|{U}\right|=\left|{W}\right|+1\right)\to \left|{W}\right|=\left|{W}\right|+1-1$
9 oveq1 ${⊢}\left|{U}\right|=\left|{W}\right|+1\to \left|{U}\right|-1=\left|{W}\right|+1-1$
10 9 eqcomd ${⊢}\left|{U}\right|=\left|{W}\right|+1\to \left|{W}\right|+1-1=\left|{U}\right|-1$
11 10 3ad2ant3 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {U}\in \mathrm{Word}{V}\wedge \left|{U}\right|=\left|{W}\right|+1\right)\to \left|{W}\right|+1-1=\left|{U}\right|-1$
12 8 11 eqtrd ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {U}\in \mathrm{Word}{V}\wedge \left|{U}\right|=\left|{W}\right|+1\right)\to \left|{W}\right|=\left|{U}\right|-1$
13 12 oveq2d ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {U}\in \mathrm{Word}{V}\wedge \left|{U}\right|=\left|{W}\right|+1\right)\to {U}\mathrm{prefix}\left|{W}\right|={U}\mathrm{prefix}\left(\left|{U}\right|-1\right)$
14 13 oveq1d ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {U}\in \mathrm{Word}{V}\wedge \left|{U}\right|=\left|{W}\right|+1\right)\to \left({U}\mathrm{prefix}\left|{W}\right|\right)\mathrm{++}⟨“\mathrm{lastS}\left({U}\right)”⟩=\left({U}\mathrm{prefix}\left(\left|{U}\right|-1\right)\right)\mathrm{++}⟨“\mathrm{lastS}\left({U}\right)”⟩$
15 simp2 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {U}\in \mathrm{Word}{V}\wedge \left|{U}\right|=\left|{W}\right|+1\right)\to {U}\in \mathrm{Word}{V}$
16 nn0p1gt0 ${⊢}\left|{W}\right|\in {ℕ}_{0}\to 0<\left|{W}\right|+1$
17 3 16 syl ${⊢}{W}\in \mathrm{Word}{V}\to 0<\left|{W}\right|+1$
18 17 3ad2ant1 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {U}\in \mathrm{Word}{V}\wedge \left|{U}\right|=\left|{W}\right|+1\right)\to 0<\left|{W}\right|+1$
19 breq2 ${⊢}\left|{U}\right|=\left|{W}\right|+1\to \left(0<\left|{U}\right|↔0<\left|{W}\right|+1\right)$
20 19 3ad2ant3 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {U}\in \mathrm{Word}{V}\wedge \left|{U}\right|=\left|{W}\right|+1\right)\to \left(0<\left|{U}\right|↔0<\left|{W}\right|+1\right)$
21 18 20 mpbird ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {U}\in \mathrm{Word}{V}\wedge \left|{U}\right|=\left|{W}\right|+1\right)\to 0<\left|{U}\right|$
22 hashneq0 ${⊢}{U}\in \mathrm{Word}{V}\to \left(0<\left|{U}\right|↔{U}\ne \varnothing \right)$
23 22 3ad2ant2 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {U}\in \mathrm{Word}{V}\wedge \left|{U}\right|=\left|{W}\right|+1\right)\to \left(0<\left|{U}\right|↔{U}\ne \varnothing \right)$
24 21 23 mpbid ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {U}\in \mathrm{Word}{V}\wedge \left|{U}\right|=\left|{W}\right|+1\right)\to {U}\ne \varnothing$
25 pfxlswccat ${⊢}\left({U}\in \mathrm{Word}{V}\wedge {U}\ne \varnothing \right)\to \left({U}\mathrm{prefix}\left(\left|{U}\right|-1\right)\right)\mathrm{++}⟨“\mathrm{lastS}\left({U}\right)”⟩={U}$
26 15 24 25 syl2anc ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {U}\in \mathrm{Word}{V}\wedge \left|{U}\right|=\left|{W}\right|+1\right)\to \left({U}\mathrm{prefix}\left(\left|{U}\right|-1\right)\right)\mathrm{++}⟨“\mathrm{lastS}\left({U}\right)”⟩={U}$
27 14 26 eqtrd ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {U}\in \mathrm{Word}{V}\wedge \left|{U}\right|=\left|{W}\right|+1\right)\to \left({U}\mathrm{prefix}\left|{W}\right|\right)\mathrm{++}⟨“\mathrm{lastS}\left({U}\right)”⟩={U}$
28 27 adantr ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge {U}\in \mathrm{Word}{V}\wedge \left|{U}\right|=\left|{W}\right|+1\right)\wedge {W}={U}\mathrm{prefix}\left|{W}\right|\right)\to \left({U}\mathrm{prefix}\left|{W}\right|\right)\mathrm{++}⟨“\mathrm{lastS}\left({U}\right)”⟩={U}$
29 2 28 eqtr2d ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge {U}\in \mathrm{Word}{V}\wedge \left|{U}\right|=\left|{W}\right|+1\right)\wedge {W}={U}\mathrm{prefix}\left|{W}\right|\right)\to {U}={W}\mathrm{++}⟨“\mathrm{lastS}\left({U}\right)”⟩$
30 29 ex ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {U}\in \mathrm{Word}{V}\wedge \left|{U}\right|=\left|{W}\right|+1\right)\to \left({W}={U}\mathrm{prefix}\left|{W}\right|\to {U}={W}\mathrm{++}⟨“\mathrm{lastS}\left({U}\right)”⟩\right)$