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∈WordV∧I∈0..^W→W++⟨“S”⟩⁡I=W⁡I

Proof

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