Metamath Proof Explorer

Theorem ccat2s1fvwALT

Description: Alternate proof of ccat2s1fvw using words of length 2, see df-s2 . A symbol of the concatenation of a word with two single symbols corresponding to the symbol of the word. (Contributed by AV, 22-Sep-2018) (Proof shortened by Mario Carneiro/AV, 21-Oct-2018) (Revised by AV, 28-Jan-2024) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion ccat2s1fvwALT ⊢ W ∈ Word V ∧ I ∈ ℕ 0 ∧ I < W → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ I = W ⁡ I

Proof

Step Hyp Ref Expression
1 ccatw2s1ccatws2 ⊢ W ∈ Word V → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = W ++ ⟨“ XY ”⟩
2 1 fveq1d ⊢ W ∈ Word V → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ I = W ++ ⟨“ XY ”⟩ ⁡ I
3 2 3ad2ant1 ⊢ W ∈ Word V ∧ I ∈ ℕ 0 ∧ I < W → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ I = W ++ ⟨“ XY ”⟩ ⁡ I
4 simp1 ⊢ W ∈ Word V ∧ I ∈ ℕ 0 ∧ I < W → W ∈ Word V
5 s2cli ⊢ ⟨“ XY ”⟩ ∈ Word V
6 5 a1i ⊢ W ∈ Word V ∧ I ∈ ℕ 0 ∧ I < W → ⟨“ XY ”⟩ ∈ Word V
7 simp2 ⊢ W ∈ Word V ∧ I ∈ ℕ 0 ∧ I < W → I ∈ ℕ 0
8 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
9 8 nn0zd ⊢ W ∈ Word V → W ∈ ℤ
10 9 3ad2ant1 ⊢ W ∈ Word V ∧ I ∈ ℕ 0 ∧ I < W → W ∈ ℤ
11 simp3 ⊢ W ∈ Word V ∧ I ∈ ℕ 0 ∧ I < W → I < W
12 elfzo0z ⊢ I ∈ 0 ..^ W ↔ I ∈ ℕ 0 ∧ W ∈ ℤ ∧ I < W
13 7 10 11 12 syl3anbrc ⊢ W ∈ Word V ∧ I ∈ ℕ 0 ∧ I < W → I ∈ 0 ..^ W
14 ccatval1 ⊢ W ∈ Word V ∧ ⟨“ XY ”⟩ ∈ Word V ∧ I ∈ 0 ..^ W → W ++ ⟨“ XY ”⟩ ⁡ I = W ⁡ I
15 4 6 13 14 syl3anc ⊢ W ∈ Word V ∧ I ∈ ℕ 0 ∧ I < W → W ++ ⟨“ XY ”⟩ ⁡ I = W ⁡ I
16 3 15 eqtrd ⊢ W ∈ Word V ∧ I ∈ ℕ 0 ∧ I < W → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ I = W ⁡ I