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 ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → W = U prefix W ↔ U = W ++ ⟨“ lastS ⁡ U ”⟩

Proof

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