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