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 ⊢ ⟨“ ABCDEFG ”⟩ = ⟨“ ABC ”⟩ ++ ⟨“ DEFG ”⟩

Proof

Step Hyp Ref Expression
1 s2s2 ⊢ ⟨“ ABCD ”⟩ = ⟨“ AB ”⟩ ++ ⟨“ CD ”⟩
2 1 eqcomi ⊢ ⟨“ AB ”⟩ ++ ⟨“ CD ”⟩ = ⟨“ ABCD ”⟩
3 2 oveq1i ⊢ ⟨“ AB ”⟩ ++ ⟨“ CD ”⟩ ++ ⟨“ EFG ”⟩ = ⟨“ ABCD ”⟩ ++ ⟨“ EFG ”⟩
4 s2cli ⊢ ⟨“ AB ”⟩ ∈ Word V
5 s3cli ⊢ ⟨“ EFG ”⟩ ∈ Word V
6 df-s3 ⊢ ⟨“ ABC ”⟩ = ⟨“ AB ”⟩ ++ ⟨“ C ”⟩
7 s1s3 ⊢ ⟨“ DEFG ”⟩ = ⟨“ D ”⟩ ++ ⟨“ EFG ”⟩
8 4 5 6 7 cats2cat ⊢ ⟨“ ABC ”⟩ ++ ⟨“ DEFG ”⟩ = ⟨“ AB ”⟩ ++ ⟨“ CD ”⟩ ++ ⟨“ EFG ”⟩
9 s4s3 ⊢ ⟨“ ABCDEFG ”⟩ = ⟨“ ABCD ”⟩ ++ ⟨“ EFG ”⟩
10 3 8 9 3eqtr4ri ⊢ ⟨“ ABCDEFG ”⟩ = ⟨“ ABC ”⟩ ++ ⟨“ DEFG ”⟩