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

Metamath Proof Explorer

Theorem ccatws1ls

Description: The last symbol of the concatenation of a word with a singleton word is the symbol of the singleton word. (Contributed by AV, 29-Sep-2018) (Proof shortened by AV, 14-Oct-2018)

		Ref	Expression
	Assertion	ccatws1ls	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		eqidd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) )
2		ccats1val2	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) = 𝑋 )
3	1 2	mpd3an3	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) = 𝑋 )