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 ( 𝜑𝐹 : 𝑋𝑌 )
s2co.2 ( 𝜑𝐴𝑋 )
s2co.3 ( 𝜑𝐵𝑋 )
s3co.4 ( 𝜑𝐶𝑋 )
Assertion s3co ( 𝜑 → ( 𝐹 ∘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = ⟨“ ( 𝐹𝐴 ) ( 𝐹𝐵 ) ( 𝐹𝐶 ) ”⟩ )

Proof

Step Hyp Ref Expression
1 s2co.1 ( 𝜑𝐹 : 𝑋𝑌 )
2 s2co.2 ( 𝜑𝐴𝑋 )
3 s2co.3 ( 𝜑𝐵𝑋 )
4 s3co.4 ( 𝜑𝐶𝑋 )
5 df-s3 ⟨“ 𝐴 𝐵 𝐶 ”⟩ = ( ⟨“ 𝐴 𝐵 ”⟩ ++ ⟨“ 𝐶 ”⟩ )
6 2 3 s2cld ( 𝜑 → ⟨“ 𝐴 𝐵 ”⟩ ∈ Word 𝑋 )
7 1 2 3 s2co ( 𝜑 → ( 𝐹 ∘ ⟨“ 𝐴 𝐵 ”⟩ ) = ⟨“ ( 𝐹𝐴 ) ( 𝐹𝐵 ) ”⟩ )
8 df-s3 ⟨“ ( 𝐹𝐴 ) ( 𝐹𝐵 ) ( 𝐹𝐶 ) ”⟩ = ( ⟨“ ( 𝐹𝐴 ) ( 𝐹𝐵 ) ”⟩ ++ ⟨“ ( 𝐹𝐶 ) ”⟩ )
9 5 6 4 1 7 8 cats1co ( 𝜑 → ( 𝐹 ∘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = ⟨“ ( 𝐹𝐴 ) ( 𝐹𝐵 ) ( 𝐹𝐶 ) ”⟩ )