Metamath Proof Explorer

Theorem hof2val

Description: The morphism part of the Hom functor, for morphisms <. f , g >. : <. X , Y >. --> <. Z , W >. (which since the first argument is contravariant means morphisms f : Z --> X and g : Y --> W ), yields a function (a morphism of SetCat ) mapping h : X --> Y to g o. h o. f : Z --> W . (Contributed by Mario Carneiro, 15-Jan-2017)

Ref Expression
Hypotheses hofval.m ⊢ 𝑀 = ( HomF ‘ 𝐶 )
hofval.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
hof1.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
hof1.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
hof1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
hof1.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
hof2.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
hof2.w ⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
hof2.o ⊢ · = ( comp ‘ 𝐶 )
hof2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑍 𝐻 𝑋 ) )
hof2.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑊 ) )
Assertion hof2val ( 𝜑 → ( 𝐹 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝑀 ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝐺 ) = ( ℎ ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) ℎ ) ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 hofval.m ⊢ 𝑀 = ( HomF ‘ 𝐶 )
2 hofval.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
3 hof1.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
4 hof1.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
5 hof1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 hof1.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 hof2.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8 hof2.w ⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
9 hof2.o ⊢ · = ( comp ‘ 𝐶 )
10 hof2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑍 𝐻 𝑋 ) )
11 hof2.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑊 ) )
12 1 2 3 4 5 6 7 8 9 hof2fval ⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝑀 ) ⟨ 𝑍 , 𝑊 ⟩ ) = ( 𝑓 ∈ ( 𝑍 𝐻 𝑋 ) , 𝑔 ∈ ( 𝑌 𝐻 𝑊 ) ↦ ( ℎ ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) ℎ ) ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) 𝑓 ) ) ) )
13 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ ℎ ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑔 = 𝐺 )
14 13 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ ℎ ∈ ( 𝑋 𝐻 𝑌 ) ) → ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) ℎ ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) ℎ ) )
15 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ ℎ ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑓 = 𝐹 )
16 14 15 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ ℎ ∈ ( 𝑋 𝐻 𝑌 ) ) → ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) ℎ ) ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) 𝑓 ) = ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) ℎ ) ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) 𝐹 ) )
17 16 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( ℎ ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) ℎ ) ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) 𝑓 ) ) = ( ℎ ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) ℎ ) ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) 𝐹 ) ) )
18 ovex ⊢ ( 𝑋 𝐻 𝑌 ) ∈ V
19 18 mptex ⊢ ( ℎ ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) ℎ ) ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) 𝐹 ) ) ∈ V
20 19 a1i ⊢ ( 𝜑 → ( ℎ ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) ℎ ) ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) 𝐹 ) ) ∈ V )
21 12 17 10 11 20 ovmpod ⊢ ( 𝜑 → ( 𝐹 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝑀 ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝐺 ) = ( ℎ ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) ℎ ) ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) 𝐹 ) ) )