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

Metamath Proof Explorer

Theorem s3s4

Description: Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021)

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

Proof

Step Hyp Ref Expression
1 s2s2 ⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ = ( ⟨“ 𝐴 𝐵 ”⟩ ++ ⟨“ 𝐶 𝐷 ”⟩ )
2 1 eqcomi ⊢ ( ⟨“ 𝐴 𝐵 ”⟩ ++ ⟨“ 𝐶 𝐷 ”⟩ ) = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩
3 2 oveq1i ⊢ ( ( ⟨“ 𝐴 𝐵 ”⟩ ++ ⟨“ 𝐶 𝐷 ”⟩ ) ++ ⟨“ 𝐸 𝐹 𝐺 ”⟩ ) = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ++ ⟨“ 𝐸 𝐹 𝐺 ”⟩ )
4 s2cli ⊢ ⟨“ 𝐴 𝐵 ”⟩ ∈ Word V
5 s3cli ⊢ ⟨“ 𝐸 𝐹 𝐺 ”⟩ ∈ Word V
6 df-s3 ⊢ ⟨“ 𝐴 𝐵 𝐶 ”⟩ = ( ⟨“ 𝐴 𝐵 ”⟩ ++ ⟨“ 𝐶 ”⟩ )
7 s1s3 ⊢ ⟨“ 𝐷 𝐸 𝐹 𝐺 ”⟩ = ( ⟨“ 𝐷 ”⟩ ++ ⟨“ 𝐸 𝐹 𝐺 ”⟩ )
8 4 5 6 7 cats2cat ⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 𝐸 𝐹 𝐺 ”⟩ ) = ( ( ⟨“ 𝐴 𝐵 ”⟩ ++ ⟨“ 𝐶 𝐷 ”⟩ ) ++ ⟨“ 𝐸 𝐹 𝐺 ”⟩ )
9 s4s3 ⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ++ ⟨“ 𝐸 𝐹 𝐺 ”⟩ )
10 3 8 9 3eqtr4ri ⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 𝐸 𝐹 𝐺 ”⟩ )