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