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