Theorem comffval

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	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
Assertion	comffval	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ 𝑂 𝑍 ) = ( 𝑔 ∈ ( 𝑌 𝐻 𝑍 ) , 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑓 ) ) )

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	1 2 3 4	comfffval	⊢ 𝑂 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 · 𝑧 ) 𝑓 ) ) )
9	8	a1i	⊢ ( 𝜑 → 𝑂 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 · 𝑧 ) 𝑓 ) ) ) )
10		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ )
11	10	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2nd ‘ 𝑥 ) = ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
12		op2ndg	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
13	5 6 12	syl2anc	⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
14	13	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
15	11 14	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2nd ‘ 𝑥 ) = 𝑌 )
16		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → 𝑧 = 𝑍 )
17	15 16	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( ( 2nd ‘ 𝑥 ) 𝐻 𝑧 ) = ( 𝑌 𝐻 𝑍 ) )
18	10	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
19		df-ov	⊢ ( 𝑋 𝐻 𝑌 ) = ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
20	18 19	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 𝐻 ‘ 𝑥 ) = ( 𝑋 𝐻 𝑌 ) )
21	10 16	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 𝑥 · 𝑧 ) = ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) )
22	21	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 𝑔 ( 𝑥 · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑓 ) )
23	17 20 22	mpoeq123dv	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) 𝐻 𝑧 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 · 𝑧 ) 𝑓 ) ) = ( 𝑔 ∈ ( 𝑌 𝐻 𝑍 ) , 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑓 ) ) )
24	5 6	opelxpd	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
25		ovex	⊢ ( 𝑌 𝐻 𝑍 ) ∈ V
26		ovex	⊢ ( 𝑋 𝐻 𝑌 ) ∈ V
27	25 26	mpoex	⊢ ( 𝑔 ∈ ( 𝑌 𝐻 𝑍 ) , 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑓 ) ) ∈ V
28	27	a1i	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝑌 𝐻 𝑍 ) , 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑓 ) ) ∈ V )
29	9 23 24 7 28	ovmpod	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ 𝑂 𝑍 ) = ( 𝑔 ∈ ( 𝑌 𝐻 𝑍 ) , 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑓 ) ) )