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

Metamath Proof Explorer

Theorem s2s5

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

Ref Expression
Assertion s2s5 ⊢ ⟨“ ABCDEFG ”⟩ = ⟨“ AB ”⟩ ++ ⟨“ CDEFG ”⟩

Proof

Step Hyp Ref Expression
1 s1s2 ⊢ ⟨“ ABC ”⟩ = ⟨“ A ”⟩ ++ ⟨“ BC ”⟩
2 1 eqcomi ⊢ ⟨“ A ”⟩ ++ ⟨“ BC ”⟩ = ⟨“ ABC ”⟩
3 2 oveq1i ⊢ ⟨“ A ”⟩ ++ ⟨“ BC ”⟩ ++ ⟨“ DEFG ”⟩ = ⟨“ ABC ”⟩ ++ ⟨“ DEFG ”⟩
4 s1cli ⊢ ⟨“ A ”⟩ ∈ Word V
5 s4cli ⊢ ⟨“ DEFG ”⟩ ∈ Word V
6 df-s2 ⊢ ⟨“ AB ”⟩ = ⟨“ A ”⟩ ++ ⟨“ B ”⟩
7 s1s4 ⊢ ⟨“ CDEFG ”⟩ = ⟨“ C ”⟩ ++ ⟨“ DEFG ”⟩
8 4 5 6 7 cats2cat ⊢ ⟨“ AB ”⟩ ++ ⟨“ CDEFG ”⟩ = ⟨“ A ”⟩ ++ ⟨“ BC ”⟩ ++ ⟨“ DEFG ”⟩
9 s3s4 ⊢ ⟨“ ABCDEFG ”⟩ = ⟨“ ABC ”⟩ ++ ⟨“ DEFG ”⟩
10 3 8 9 3eqtr4ri ⊢ ⟨“ ABCDEFG ”⟩ = ⟨“ AB ”⟩ ++ ⟨“ CDEFG ”⟩