This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-s8

Description: Define the length 8 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion df-s8 ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 𝐻 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ ++ ⟨“ 𝐻 ”⟩ )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ⊢ 𝐴
1 cB ⊢ 𝐵
2 cC ⊢ 𝐶
3 cD ⊢ 𝐷
4 cE ⊢ 𝐸
5 cF ⊢ 𝐹
6 cG ⊢ 𝐺
7 cH ⊢ 𝐻
8 0 1 2 3 4 5 6 7 cs8 ⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 𝐻 ”⟩
9 0 1 2 3 4 5 6 cs7 ⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩
10 cconcat ⊢ ++
11 7 cs1 ⊢ ⟨“ 𝐻 ”⟩
12 9 11 10 co ⊢ ( ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ ++ ⟨“ 𝐻 ”⟩ )
13 8 12 wceq ⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 𝐻 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ ++ ⟨“ 𝐻 ”⟩ )