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 ⊢ W ∈ Word V ∧ W = N ∧ X ∈ V ∧ Y ∈ V → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ N + 1 = Y

Proof

Step Hyp Ref Expression
1 ccatws1cl ⊢ W ∈ Word V ∧ X ∈ V → W ++ ⟨“ X ”⟩ ∈ Word V
2 1 ad2ant2r ⊢ W ∈ Word V ∧ W = N ∧ X ∈ V ∧ Y ∈ V → W ++ ⟨“ X ”⟩ ∈ Word V
3 simprr ⊢ W ∈ Word V ∧ W = N ∧ X ∈ V ∧ Y ∈ V → Y ∈ V
4 ccatws1len ⊢ W ∈ Word V → W ++ ⟨“ X ”⟩ = W + 1
5 4 ad2antrr ⊢ W ∈ Word V ∧ W = N ∧ X ∈ V ∧ Y ∈ V → W ++ ⟨“ X ”⟩ = W + 1
6 oveq1 ⊢ W = N → W + 1 = N + 1
7 6 ad2antlr ⊢ W ∈ Word V ∧ W = N ∧ X ∈ V ∧ Y ∈ V → W + 1 = N + 1
8 5 7 eqtr2d ⊢ W ∈ Word V ∧ W = N ∧ X ∈ V ∧ Y ∈ V → N + 1 = W ++ ⟨“ X ”⟩
9 ccats1val2 ⊢ W ++ ⟨“ X ”⟩ ∈ Word V ∧ Y ∈ V ∧ N + 1 = W ++ ⟨“ X ”⟩ → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ N + 1 = Y
10 2 3 8 9 syl3anc ⊢ W ∈ Word V ∧ W = N ∧ X ∈ V ∧ Y ∈ V → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ N + 1 = Y