This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )

Proof

Step Hyp Ref Expression
1 hasheq0 ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) = 0 ↔ 𝑊 = ∅ ) )
2 1 biimpa ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 0 ) → 𝑊 = ∅ )
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 ⊢ ( 𝑊 = ∅ → 𝑊 = ∅ )
12 fveq1 ⊢ ( 𝑊 = ∅ → ( 𝑊 ‘ 0 ) = ( ∅ ‘ 0 ) )
13 0fv ⊢ ( ∅ ‘ 0 ) = ∅
14 12 13 eqtrdi ⊢ ( 𝑊 = ∅ → ( 𝑊 ‘ 0 ) = ∅ )
15 14 s1eqd ⊢ ( 𝑊 = ∅ → ⟨“ ( 𝑊 ‘ 0 ) ”⟩ = ⟨“ ∅ ”⟩ )
16 11 15 oveq12d ⊢ ( 𝑊 = ∅ → ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) = ( ∅ ++ ⟨“ ∅ ”⟩ ) )
17 16 fveq1d ⊢ ( 𝑊 = ∅ → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 0 ) = ( ( ∅ ++ ⟨“ ∅ ”⟩ ) ‘ 0 ) )
18 10 17 14 3eqtr4a ⊢ ( 𝑊 = ∅ → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
19 2 18 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 0 ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
20 1 necon3bid ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) ≠ 0 ↔ 𝑊 ≠ ∅ ) )
21 20 biimpa ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → 𝑊 ≠ ∅ )
22 lennncl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
23 21 22 syldan ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
24 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ )
25 23 24 sylibr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
26 ccats1val1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
27 25 26 syldan ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
28 19 27 pm2.61dane ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )