Metamath Proof Explorer

Theorem ccatw2s1p1

Description: Extract the symbol of the first singleton word of a word concatenated with this singleton word and another singleton word. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Proof shortened by AV, 1-May-2020) (Revised by AV, 1-May-2020) (Revised by AV, 29-Jan-2024)

Ref Expression
Assertion ccatw2s1p1 ⊢ W ∈ Word V ∧ W = N ∧ X ∈ V → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ N = X

Proof

Step Hyp Ref Expression
1 ccatws1cl ⊢ W ∈ Word V ∧ X ∈ V → W ++ ⟨“ X ”⟩ ∈ Word V
2 1 3adant2 ⊢ W ∈ Word V ∧ W = N ∧ X ∈ V → W ++ ⟨“ X ”⟩ ∈ Word V
3 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
4 fzonn0p1 ⊢ W ∈ ℕ 0 → W ∈ 0 ..^ W + 1
5 3 4 syl ⊢ W ∈ Word V → W ∈ 0 ..^ W + 1
6 5 adantr ⊢ W ∈ Word V ∧ W = N → W ∈ 0 ..^ W + 1
7 simpr ⊢ W ∈ Word V ∧ W = N → W = N
8 7 eqcomd ⊢ W ∈ Word V ∧ W = N → N = W
9 ccatws1len ⊢ W ∈ Word V → W ++ ⟨“ X ”⟩ = W + 1
10 9 adantr ⊢ W ∈ Word V ∧ W = N → W ++ ⟨“ X ”⟩ = W + 1
11 10 oveq2d ⊢ W ∈ Word V ∧ W = N → 0 ..^ W ++ ⟨“ X ”⟩ = 0 ..^ W + 1
12 6 8 11 3eltr4d ⊢ W ∈ Word V ∧ W = N → N ∈ 0 ..^ W ++ ⟨“ X ”⟩
13 12 3adant3 ⊢ W ∈ Word V ∧ W = N ∧ X ∈ V → N ∈ 0 ..^ W ++ ⟨“ X ”⟩
14 ccats1val1 ⊢ W ++ ⟨“ X ”⟩ ∈ Word V ∧ N ∈ 0 ..^ W ++ ⟨“ X ”⟩ → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ N = W ++ ⟨“ X ”⟩ ⁡ N
15 2 13 14 syl2anc ⊢ W ∈ Word V ∧ W = N ∧ X ∈ V → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ N = W ++ ⟨“ X ”⟩ ⁡ N
16 simp1 ⊢ W ∈ Word V ∧ W = N ∧ X ∈ V → W ∈ Word V
17 simp3 ⊢ W ∈ Word V ∧ W = N ∧ X ∈ V → X ∈ V
18 eqcom ⊢ W = N ↔ N = W
19 18 biimpi ⊢ W = N → N = W
20 19 3ad2ant2 ⊢ W ∈ Word V ∧ W = N ∧ X ∈ V → N = W
21 ccats1val2 ⊢ W ∈ Word V ∧ X ∈ V ∧ N = W → W ++ ⟨“ X ”⟩ ⁡ N = X
22 16 17 20 21 syl3anc ⊢ W ∈ Word V ∧ W = N ∧ X ∈ V → W ++ ⟨“ X ”⟩ ⁡ N = X
23 15 22 eqtrd ⊢ W ∈ Word V ∧ W = N ∧ X ∈ V → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ N = X