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

Metamath Proof Explorer

Theorem ccatw2s1p2

Description: Extract the second of two single symbols concatenated with a word. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Proof shortened by AV, 1-May-2020)

Ref Expression
Assertion ccatw2s1p2 ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 + 1 ) ) = 𝑌 )

Proof

Step Hyp Ref Expression
1 ccatws1cl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 )
2 1 ad2ant2r ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 )
3 simprr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → 𝑌 ∈ 𝑉 )
4 ccatws1len ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
5 4 ad2antrr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
6 oveq1 ⊢ ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( ( ♯ ‘ 𝑊 ) + 1 ) = ( 𝑁 + 1 ) )
7 6 ad2antlr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ♯ ‘ 𝑊 ) + 1 ) = ( 𝑁 + 1 ) )
8 5 7 eqtr2d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑁 + 1 ) = ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) )
9 ccats1val2 ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ ( 𝑁 + 1 ) = ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 + 1 ) ) = 𝑌 )
10 2 3 8 9 syl3anc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 + 1 ) ) = 𝑌 )