Metamath Proof Explorer


Theorem s1s7

Description: Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016)

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

Proof

Step Hyp Ref Expression
1 df-s7 ⟨“ 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 𝐻 ”⟩ = ( ⟨“ 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ ++ ⟨“ 𝐻 ”⟩ )
2 s1cli ⟨“ 𝐴 ”⟩ ∈ Word V
3 s6cli ⟨“ 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ ∈ Word V
4 df-s8 ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 𝐻 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ ++ ⟨“ 𝐻 ”⟩ )
5 s1s6 ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ )
6 1 2 3 4 5 cats1cat ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 𝐻 ”⟩ = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 𝐻 ”⟩ )