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