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

Metamath Proof Explorer

Theorem s3co

Description: Mapping a length 3 string by a function. (Contributed by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypotheses s2co.1 ⊢ φ → F : X ⟶ Y
s2co.2 ⊢ φ → A ∈ X
s2co.3 ⊢ φ → B ∈ X
s3co.4 ⊢ φ → C ∈ X
Assertion s3co ⊢ φ → F ∘ ⟨“ ABC ”⟩ = ⟨“ F ⁡ A F ⁡ B F ⁡ C ”⟩

Proof

Step Hyp Ref Expression
1 s2co.1 ⊢ φ → F : X ⟶ Y
2 s2co.2 ⊢ φ → A ∈ X
3 s2co.3 ⊢ φ → B ∈ X
4 s3co.4 ⊢ φ → C ∈ X
5 df-s3 ⊢ ⟨“ ABC ”⟩ = ⟨“ AB ”⟩ ++ ⟨“ C ”⟩
6 2 3 s2cld ⊢ φ → ⟨“ AB ”⟩ ∈ Word X
7 1 2 3 s2co ⊢ φ → F ∘ ⟨“ AB ”⟩ = ⟨“ F ⁡ A F ⁡ B ”⟩
8 df-s3 ⊢ ⟨“ F ⁡ A F ⁡ B F ⁡ C ”⟩ = ⟨“ F ⁡ A F ⁡ B ”⟩ ++ ⟨“ F ⁡ C ”⟩
9 5 6 4 1 7 8 cats1co ⊢ φ → F ∘ ⟨“ ABC ”⟩ = ⟨“ F ⁡ A F ⁡ B F ⁡ C ”⟩