Metamath Proof Explorer

Theorem ccats1val1

Description: Value of a symbol in the left half of a word concatenated with a single symbol. (Contributed by Alexander van der Vekens, 5-Aug-2018) (Revised by JJ, 20-Jan-2024)

Ref Expression
Assertion ccats1val1 ⊢ W ∈ Word V ∧ I ∈ 0 ..^ W → W ++ ⟨“ S ”⟩ ⁡ I = W ⁡ I

Proof

Step Hyp Ref Expression
1 s1cli ⊢ ⟨“ S ”⟩ ∈ Word V
2 ccatval1 ⊢ W ∈ Word V ∧ ⟨“ S ”⟩ ∈ Word V ∧ I ∈ 0 ..^ W → W ++ ⟨“ S ”⟩ ⁡ I = W ⁡ I
3 1 2 mp3an2 ⊢ W ∈ Word V ∧ I ∈ 0 ..^ W → W ++ ⟨“ S ”⟩ ⁡ I = W ⁡ I