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

Metamath Proof Explorer

Theorem cats1co

Description: Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016)

Ref Expression
Hypotheses cats1cld.1 ⊢ 𝑇 = ( 𝑆 ++ ⟨“ 𝑋 ”⟩ )
cats1cld.2 ⊢ ( 𝜑 → 𝑆 ∈ Word 𝐴 )
cats1cld.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
cats1co.4 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
cats1co.5 ⊢ ( 𝜑 → ( 𝐹 ∘ 𝑆 ) = 𝑈 )
cats1co.6 ⊢ 𝑉 = ( 𝑈 ++ ⟨“ ( 𝐹 ‘ 𝑋 ) ”⟩ )
Assertion cats1co ( 𝜑 → ( 𝐹 ∘ 𝑇 ) = 𝑉 )

Proof

Step Hyp Ref Expression
1 cats1cld.1 ⊢ 𝑇 = ( 𝑆 ++ ⟨“ 𝑋 ”⟩ )
2 cats1cld.2 ⊢ ( 𝜑 → 𝑆 ∈ Word 𝐴 )
3 cats1cld.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
4 cats1co.4 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
5 cats1co.5 ⊢ ( 𝜑 → ( 𝐹 ∘ 𝑆 ) = 𝑈 )
6 cats1co.6 ⊢ 𝑉 = ( 𝑈 ++ ⟨“ ( 𝐹 ‘ 𝑋 ) ”⟩ )
7 3 s1cld ⊢ ( 𝜑 → ⟨“ 𝑋 ”⟩ ∈ Word 𝐴 )
8 ccatco ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) ) = ( ( 𝐹 ∘ 𝑆 ) ++ ( 𝐹 ∘ ⟨“ 𝑋 ”⟩ ) ) )
9 2 7 4 8 syl3anc ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) ) = ( ( 𝐹 ∘ 𝑆 ) ++ ( 𝐹 ∘ ⟨“ 𝑋 ”⟩ ) ) )
10 s1co ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ⟨“ 𝑋 ”⟩ ) = ⟨“ ( 𝐹 ‘ 𝑋 ) ”⟩ )
11 3 4 10 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∘ ⟨“ 𝑋 ”⟩ ) = ⟨“ ( 𝐹 ‘ 𝑋 ) ”⟩ )
12 5 11 oveq12d ⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝑆 ) ++ ( 𝐹 ∘ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑈 ++ ⟨“ ( 𝐹 ‘ 𝑋 ) ”⟩ ) )
13 9 12 eqtrd ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑈 ++ ⟨“ ( 𝐹 ‘ 𝑋 ) ”⟩ ) )
14 1 coeq2i ⊢ ( 𝐹 ∘ 𝑇 ) = ( 𝐹 ∘ ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) )
15 13 14 6 3eqtr4g ⊢ ( 𝜑 → ( 𝐹 ∘ 𝑇 ) = 𝑉 )