Theorem comfval

Description: Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	comfffval.o	⊢ 𝑂 = ( compf ‘ 𝐶 )
	comfffval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	comfffval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	comfffval.x	⊢ · = ( comp ‘ 𝐶 )
	comffval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	comffval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	comffval.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	comfval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
	comfval.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
Assertion	comfval	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ 𝑂 𝑍 ) 𝐹 ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		comfffval.o	⊢ 𝑂 = ( compf ‘ 𝐶 )
2		comfffval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		comfffval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
4		comfffval.x	⊢ · = ( comp ‘ 𝐶 )
5		comffval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		comffval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		comffval.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8		comfval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
9		comfval.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
10	1 2 3 4 5 6 7	comffval	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ 𝑂 𝑍 ) = ( 𝑔 ∈ ( 𝑌 𝐻 𝑍 ) , 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑓 ) ) )
11		oveq12	⊢ ( ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) → ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑓 ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) )
12	11	adantl	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑓 ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) )
13		ovexd	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ V )
14	10 12 9 8 13	ovmpod	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ 𝑂 𝑍 ) 𝐹 ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) )