Metamath Proof Explorer

Theorem ccat1st1st

Description: The first symbol of a word concatenated with its first symbol is the first symbol of the word. This theorem holds even if W is the empty word. (Contributed by AV, 26-Mar-2022)

Ref Expression
Assertion ccat1st1st ⊢ W ∈ Word V → W ++ ⟨“ W ⁡ 0 ”⟩ ⁡ 0 = W ⁡ 0

Proof

Step Hyp Ref Expression
1 hasheq0 ⊢ W ∈ Word V → W = 0 ↔ W = ∅
2 1 biimpa ⊢ W ∈ Word V ∧ W = 0 → W = ∅
3 s1cli ⊢ ⟨“ ∅ ”⟩ ∈ Word V
4 ccatlid ⊢ ⟨“ ∅ ”⟩ ∈ Word V → ∅ ++ ⟨“ ∅ ”⟩ = ⟨“ ∅ ”⟩
5 3 4 ax-mp ⊢ ∅ ++ ⟨“ ∅ ”⟩ = ⟨“ ∅ ”⟩
6 5 fveq1i ⊢ ∅ ++ ⟨“ ∅ ”⟩ ⁡ 0 = ⟨“ ∅ ”⟩ ⁡ 0
7 0ex ⊢ ∅ ∈ V
8 s1fv ⊢ ∅ ∈ V → ⟨“ ∅ ”⟩ ⁡ 0 = ∅
9 7 8 ax-mp ⊢ ⟨“ ∅ ”⟩ ⁡ 0 = ∅
10 6 9 eqtri ⊢ ∅ ++ ⟨“ ∅ ”⟩ ⁡ 0 = ∅
11 id ⊢ W = ∅ → W = ∅
12 fveq1 ⊢ W = ∅ → W ⁡ 0 = ∅ ⁡ 0
13 0fv ⊢ ∅ ⁡ 0 = ∅
14 12 13 eqtrdi ⊢ W = ∅ → W ⁡ 0 = ∅
15 14 s1eqd ⊢ W = ∅ → ⟨“ W ⁡ 0 ”⟩ = ⟨“ ∅ ”⟩
16 11 15 oveq12d ⊢ W = ∅ → W ++ ⟨“ W ⁡ 0 ”⟩ = ∅ ++ ⟨“ ∅ ”⟩
17 16 fveq1d ⊢ W = ∅ → W ++ ⟨“ W ⁡ 0 ”⟩ ⁡ 0 = ∅ ++ ⟨“ ∅ ”⟩ ⁡ 0
18 10 17 14 3eqtr4a ⊢ W = ∅ → W ++ ⟨“ W ⁡ 0 ”⟩ ⁡ 0 = W ⁡ 0
19 2 18 syl ⊢ W ∈ Word V ∧ W = 0 → W ++ ⟨“ W ⁡ 0 ”⟩ ⁡ 0 = W ⁡ 0
20 1 necon3bid ⊢ W ∈ Word V → W ≠ 0 ↔ W ≠ ∅
21 20 biimpa ⊢ W ∈ Word V ∧ W ≠ 0 → W ≠ ∅
22 lennncl ⊢ W ∈ Word V ∧ W ≠ ∅ → W ∈ ℕ
23 21 22 syldan ⊢ W ∈ Word V ∧ W ≠ 0 → W ∈ ℕ
24 lbfzo0 ⊢ 0 ∈ 0 ..^ W ↔ W ∈ ℕ
25 23 24 sylibr ⊢ W ∈ Word V ∧ W ≠ 0 → 0 ∈ 0 ..^ W
26 ccats1val1 ⊢ W ∈ Word V ∧ 0 ∈ 0 ..^ W → W ++ ⟨“ W ⁡ 0 ”⟩ ⁡ 0 = W ⁡ 0
27 25 26 syldan ⊢ W ∈ Word V ∧ W ≠ 0 → W ++ ⟨“ W ⁡ 0 ”⟩ ⁡ 0 = W ⁡ 0
28 19 27 pm2.61dane ⊢ W ∈ Word V → W ++ ⟨“ W ⁡ 0 ”⟩ ⁡ 0 = W ⁡ 0