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 ) )