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∈WordV∧U∈WordV∧U=W+1→W=UprefixW→U=W++⟨“lastS⁡U”⟩

Proof

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