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∈WordV→W++⟨“W⁡0”⟩⁡0=W⁡0

Proof

Step Hyp Ref Expression
1 hasheq0 ⊢W∈WordV→W=0↔W=∅
2 1 biimpa ⊢W∈WordV∧W=0→W=∅
3 s1cli ⊢⟨“∅”⟩∈WordV
4 ccatlid ⊢⟨“∅”⟩∈WordV→∅++⟨“∅”⟩=⟨“∅”⟩
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∈WordV∧W=0→W++⟨“W⁡0”⟩⁡0=W⁡0
20 1 necon3bid ⊢W∈WordV→W≠0↔W≠∅
21 20 biimpa ⊢W∈WordV∧W≠0→W≠∅
22 lennncl ⊢W∈WordV∧W≠∅→W∈ℕ
23 21 22 syldan ⊢W∈WordV∧W≠0→W∈ℕ
24 lbfzo0 ⊢0∈0..^W↔W∈ℕ
25 23 24 sylibr ⊢W∈WordV∧W≠0→0∈0..^W
26 ccats1val1 ⊢W∈WordV∧0∈0..^W→W++⟨“W⁡0”⟩⁡0=W⁡0
27 25 26 syldan ⊢W∈WordV∧W≠0→W++⟨“W⁡0”⟩⁡0=W⁡0
28 19 27 pm2.61dane ⊢W∈WordV→W++⟨“W⁡0”⟩⁡0=W⁡0