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 ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌· 𝑍 ) 𝐹 ) = ( 𝐺𝐹 ) )