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

Metamath Proof Explorer

Theorem rngcco

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

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

Proof

Step Hyp Ref Expression
1 rngcco.c ⊢ 𝐶 = ( RngCat ‘ 𝑈 )
2 rngcco.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3 rngcco.o ⊢ · = ( comp ‘ 𝐶 )
4 rngcco.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
5 rngcco.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
6 rngcco.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
7 rngcco.f ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) )
8 rngcco.g ⊢ ( 𝜑 → 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑍 ) )
9 1 2 3 rngccofval ⊢ ( 𝜑 → · = ( 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 ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 𝐺 ∘ 𝐹 ) )