Metamath Proof Explorer

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