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

Metamath Proof Explorer

Theorem s5s2

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

Ref Expression
Assertion s5s2 ⊢ ⟨“ ABCDEFG ”⟩ = ⟨“ ABCDE ”⟩ ++ ⟨“ FG ”⟩

Proof

Step Hyp Ref Expression
1 s4s2 ⊢ ⟨“ ABCDEF ”⟩ = ⟨“ ABCD ”⟩ ++ ⟨“ EF ”⟩
2 1 eqcomi ⊢ ⟨“ ABCD ”⟩ ++ ⟨“ EF ”⟩ = ⟨“ ABCDEF ”⟩
3 2 oveq1i ⊢ ⟨“ ABCD ”⟩ ++ ⟨“ EF ”⟩ ++ ⟨“ G ”⟩ = ⟨“ ABCDEF ”⟩ ++ ⟨“ G ”⟩
4 s4cli ⊢ ⟨“ ABCD ”⟩ ∈ Word V
5 s1cli ⊢ ⟨“ G ”⟩ ∈ Word V
6 df-s5 ⊢ ⟨“ ABCDE ”⟩ = ⟨“ ABCD ”⟩ ++ ⟨“ E ”⟩
7 df-s2 ⊢ ⟨“ FG ”⟩ = ⟨“ F ”⟩ ++ ⟨“ G ”⟩
8 4 5 6 7 cats2cat ⊢ ⟨“ ABCDE ”⟩ ++ ⟨“ FG ”⟩ = ⟨“ ABCD ”⟩ ++ ⟨“ EF ”⟩ ++ ⟨“ G ”⟩
9 df-s7 ⊢ ⟨“ ABCDEFG ”⟩ = ⟨“ ABCDEF ”⟩ ++ ⟨“ G ”⟩
10 3 8 9 3eqtr4ri ⊢ ⟨“ ABCDEFG ”⟩ = ⟨“ ABCDE ”⟩ ++ ⟨“ FG ”⟩