Metamath Proof Explorer

Theorem ccats1val1OLD

Description: Obsolete version of ccats1val1 as of 20-Jan-2024. 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) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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