Theorem comfffval2

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

	Ref	Expression
Hypotheses	comfffval2.o	⊢ 𝑂 = ( compf ‘ 𝐶 )
	comfffval2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	comfffval2.h	⊢ 𝐻 = ( Homf ‘ 𝐶 )
	comfffval2.x	⊢ · = ( comp ‘ 𝐶 )
Assertion	comfffval2	⊢ 𝑂 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) 𝐻 𝑦 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 · 𝑦 ) 𝑓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		comfffval2.o	⊢ 𝑂 = ( compf ‘ 𝐶 )
2		comfffval2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		comfffval2.h	⊢ 𝐻 = ( Homf ‘ 𝐶 )
4		comfffval2.x	⊢ · = ( comp ‘ 𝐶 )
5		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
6	1 2 5 4	comfffval	⊢ 𝑂 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 · 𝑦 ) 𝑓 ) ) )
7		xp2nd	⊢ ( 𝑥 ∈ ( 𝐵 × 𝐵 ) → ( 2nd ‘ 𝑥 ) ∈ 𝐵 )
8	7	adantr	⊢ ( ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 2nd ‘ 𝑥 ) ∈ 𝐵 )
9		simpr	⊢ ( ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
10	3 2 5 8 9	homfval	⊢ ( ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 2nd ‘ 𝑥 ) 𝐻 𝑦 ) = ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) 𝑦 ) )
11		xp1st	⊢ ( 𝑥 ∈ ( 𝐵 × 𝐵 ) → ( 1st ‘ 𝑥 ) ∈ 𝐵 )
12	11	adantr	⊢ ( ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 1st ‘ 𝑥 ) ∈ 𝐵 )
13	3 2 5 12 8	homfval	⊢ ( ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 1st ‘ 𝑥 ) 𝐻 ( 2nd ‘ 𝑥 ) ) = ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2nd ‘ 𝑥 ) ) )
14		df-ov	⊢ ( ( 1st ‘ 𝑥 ) 𝐻 ( 2nd ‘ 𝑥 ) ) = ( 𝐻 ‘ ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ )
15		df-ov	⊢ ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2nd ‘ 𝑥 ) ) = ( ( Hom ‘ 𝐶 ) ‘ ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ )
16	13 14 15	3eqtr3g	⊢ ( ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐻 ‘ ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ) = ( ( Hom ‘ 𝐶 ) ‘ ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ) )
17		1st2nd2	⊢ ( 𝑥 ∈ ( 𝐵 × 𝐵 ) → 𝑥 = ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ )
18	17	adantr	⊢ ( ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑥 = ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ )
19	18	fveq2d	⊢ ( ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ) )
20	18	fveq2d	⊢ ( ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) = ( ( Hom ‘ 𝐶 ) ‘ ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ) )
21	16 19 20	3eqtr4d	⊢ ( ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐻 ‘ 𝑥 ) = ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) )
22		eqidd	⊢ ( ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑔 ( 𝑥 · 𝑦 ) 𝑓 ) = ( 𝑔 ( 𝑥 · 𝑦 ) 𝑓 ) )
23	10 21 22	mpoeq123dv	⊢ ( ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) 𝐻 𝑦 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 · 𝑦 ) 𝑓 ) ) = ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 · 𝑦 ) 𝑓 ) ) )
24	23	mpoeq3ia	⊢ ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) 𝐻 𝑦 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 · 𝑦 ) 𝑓 ) ) ) = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 · 𝑦 ) 𝑓 ) ) )
25	6 24	eqtr4i	⊢ 𝑂 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) 𝐻 𝑦 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 · 𝑦 ) 𝑓 ) ) )