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

Metamath Proof Explorer

Theorem ringcco

Description: Composition in the category of unital rings. (Contributed by AV, 14-Feb-2020) (Revised by AV, 8-Mar-2020)

Ref Expression
Hypotheses ringcco.c ⊢ 𝐶 = ( RingCat ‘ 𝑈 )
ringcco.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
ringcco.o ⊢ · = ( comp ‘ 𝐶 )
ringcco.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
ringcco.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
ringcco.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
ringcco.f ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) )
ringcco.g ⊢ ( 𝜑 → 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑍 ) )
Assertion ringcco ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 𝐺 ∘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 ringcco.c ⊢ 𝐶 = ( RingCat ‘ 𝑈 )
2 ringcco.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3 ringcco.o ⊢ · = ( comp ‘ 𝐶 )
4 ringcco.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
5 ringcco.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
6 ringcco.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
7 ringcco.f ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) )
8 ringcco.g ⊢ ( 𝜑 → 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑍 ) )
9 1 2 3 ringccofval ⊢ ( 𝜑 → · = ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) )
10 9 oveqd ⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) = ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) 𝑍 ) )
11 10 oveqd ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) 𝑍 ) 𝐹 ) )
12 eqid ⊢ ( ExtStrCat ‘ 𝑈 ) = ( ExtStrCat ‘ 𝑈 )
13 eqid ⊢ ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) = ( comp ‘ ( ExtStrCat ‘ 𝑈 ) )
14 eqid ⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
15 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
16 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
17 12 2 13 4 5 6 14 15 16 7 8 estrcco ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) 𝑍 ) 𝐹 ) = ( 𝐺 ∘ 𝐹 ) )
18 11 17 eqtrd ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 𝐺 ∘ 𝐹 ) )