Metamath Proof Explorer

Theorem ccats1pfxeqbi

Description: A word is a prefix of a word with length greater by 1 than the first word iff the second word is the first word concatenated with the last symbol of the second word. (Contributed by AV, 24-Oct-2018) (Revised by AV, 10-May-2020)

Ref Expression
Assertion ccats1pfxeqbi ⊢W∈WordV∧U∈WordV∧U=W+1→W=UprefixW↔U=W++⟨“lastS⁡U”⟩

Proof

Step Hyp Ref Expression
1 ccats1pfxeq ⊢W∈WordV∧U∈WordV∧U=W+1→W=UprefixW→U=W++⟨“lastS⁡U”⟩
2 simp1 ⊢W∈WordV∧U∈WordV∧U=W+1→W∈WordV
3 lencl ⊢W∈WordV→W∈ℕ0
4 nn0p1nn ⊢W∈ℕ0→W+1∈ℕ
5 3 4 syl ⊢W∈WordV→W+1∈ℕ
6 5 3ad2ant1 ⊢W∈WordV∧U∈WordV∧U=W+1→W+1∈ℕ
7 3simpc ⊢W∈WordV∧U∈WordV∧U=W+1→U∈WordV∧U=W+1
8 lswlgt0cl ⊢W+1∈ℕ∧U∈WordV∧U=W+1→lastS⁡U∈V
9 6 7 8 syl2anc ⊢W∈WordV∧U∈WordV∧U=W+1→lastS⁡U∈V
10 9 s1cld ⊢W∈WordV∧U∈WordV∧U=W+1→⟨“lastS⁡U”⟩∈WordV
11 eqidd ⊢W∈WordV∧U∈WordV∧U=W+1→W=W
12 pfxccatid ⊢W∈WordV∧⟨“lastS⁡U”⟩∈WordV∧W=W→W++⟨“lastS⁡U”⟩prefixW=W
13 12 eqcomd ⊢W∈WordV∧⟨“lastS⁡U”⟩∈WordV∧W=W→W=W++⟨“lastS⁡U”⟩prefixW
14 2 10 11 13 syl3anc ⊢W∈WordV∧U∈WordV∧U=W+1→W=W++⟨“lastS⁡U”⟩prefixW
15 oveq1 ⊢U=W++⟨“lastS⁡U”⟩→UprefixW=W++⟨“lastS⁡U”⟩prefixW
16 15 eqcomd ⊢U=W++⟨“lastS⁡U”⟩→W++⟨“lastS⁡U”⟩prefixW=UprefixW
17 14 16 sylan9eq ⊢W∈WordV∧U∈WordV∧U=W+1∧U=W++⟨“lastS⁡U”⟩→W=UprefixW
18 17 ex ⊢W∈WordV∧U∈WordV∧U=W+1→U=W++⟨“lastS⁡U”⟩→W=UprefixW
19 1 18 impbid ⊢W∈WordV∧U∈WordV∧U=W+1→W=UprefixW↔U=W++⟨“lastS⁡U”⟩