Metamath Proof Explorer


Theorem evlf2val

Description: Value of the evaluation natural transformation at an object. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses evlfval.e 𝐸 = ( 𝐶 evalF 𝐷 )
evlfval.c ( 𝜑𝐶 ∈ Cat )
evlfval.d ( 𝜑𝐷 ∈ Cat )
evlfval.b 𝐵 = ( Base ‘ 𝐶 )
evlfval.h 𝐻 = ( Hom ‘ 𝐶 )
evlfval.o · = ( comp ‘ 𝐷 )
evlfval.n 𝑁 = ( 𝐶 Nat 𝐷 )
evlf2.f ( 𝜑𝐹 ∈ ( 𝐶 Func 𝐷 ) )
evlf2.g ( 𝜑𝐺 ∈ ( 𝐶 Func 𝐷 ) )
evlf2.x ( 𝜑𝑋𝐵 )
evlf2.y ( 𝜑𝑌𝐵 )
evlf2.l 𝐿 = ( ⟨ 𝐹 , 𝑋 ⟩ ( 2nd𝐸 ) ⟨ 𝐺 , 𝑌 ⟩ )
evlf2val.a ( 𝜑𝐴 ∈ ( 𝐹 𝑁 𝐺 ) )
evlf2val.k ( 𝜑𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
Assertion evlf2val ( 𝜑 → ( 𝐴 𝐿 𝐾 ) = ( ( 𝐴𝑌 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑋 ) , ( ( 1st𝐹 ) ‘ 𝑌 ) ⟩ · ( ( 1st𝐺 ) ‘ 𝑌 ) ) ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 evlfval.e 𝐸 = ( 𝐶 evalF 𝐷 )
2 evlfval.c ( 𝜑𝐶 ∈ Cat )
3 evlfval.d ( 𝜑𝐷 ∈ Cat )
4 evlfval.b 𝐵 = ( Base ‘ 𝐶 )
5 evlfval.h 𝐻 = ( Hom ‘ 𝐶 )
6 evlfval.o · = ( comp ‘ 𝐷 )
7 evlfval.n 𝑁 = ( 𝐶 Nat 𝐷 )
8 evlf2.f ( 𝜑𝐹 ∈ ( 𝐶 Func 𝐷 ) )
9 evlf2.g ( 𝜑𝐺 ∈ ( 𝐶 Func 𝐷 ) )
10 evlf2.x ( 𝜑𝑋𝐵 )
11 evlf2.y ( 𝜑𝑌𝐵 )
12 evlf2.l 𝐿 = ( ⟨ 𝐹 , 𝑋 ⟩ ( 2nd𝐸 ) ⟨ 𝐺 , 𝑌 ⟩ )
13 evlf2val.a ( 𝜑𝐴 ∈ ( 𝐹 𝑁 𝐺 ) )
14 evlf2val.k ( 𝜑𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
15 1 2 3 4 5 6 7 8 9 10 11 12 evlf2 ( 𝜑𝐿 = ( 𝑎 ∈ ( 𝐹 𝑁 𝐺 ) , 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝑎𝑌 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑋 ) , ( ( 1st𝐹 ) ‘ 𝑌 ) ⟩ · ( ( 1st𝐺 ) ‘ 𝑌 ) ) ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ 𝑔 ) ) ) )
16 simprl ( ( 𝜑 ∧ ( 𝑎 = 𝐴𝑔 = 𝐾 ) ) → 𝑎 = 𝐴 )
17 16 fveq1d ( ( 𝜑 ∧ ( 𝑎 = 𝐴𝑔 = 𝐾 ) ) → ( 𝑎𝑌 ) = ( 𝐴𝑌 ) )
18 simprr ( ( 𝜑 ∧ ( 𝑎 = 𝐴𝑔 = 𝐾 ) ) → 𝑔 = 𝐾 )
19 18 fveq2d ( ( 𝜑 ∧ ( 𝑎 = 𝐴𝑔 = 𝐾 ) ) → ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ 𝑔 ) = ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ 𝐾 ) )
20 17 19 oveq12d ( ( 𝜑 ∧ ( 𝑎 = 𝐴𝑔 = 𝐾 ) ) → ( ( 𝑎𝑌 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑋 ) , ( ( 1st𝐹 ) ‘ 𝑌 ) ⟩ · ( ( 1st𝐺 ) ‘ 𝑌 ) ) ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ 𝑔 ) ) = ( ( 𝐴𝑌 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑋 ) , ( ( 1st𝐹 ) ‘ 𝑌 ) ⟩ · ( ( 1st𝐺 ) ‘ 𝑌 ) ) ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ 𝐾 ) ) )
21 ovexd ( 𝜑 → ( ( 𝐴𝑌 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑋 ) , ( ( 1st𝐹 ) ‘ 𝑌 ) ⟩ · ( ( 1st𝐺 ) ‘ 𝑌 ) ) ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ 𝐾 ) ) ∈ V )
22 15 20 13 14 21 ovmpod ( 𝜑 → ( 𝐴 𝐿 𝐾 ) = ( ( 𝐴𝑌 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑋 ) , ( ( 1st𝐹 ) ‘ 𝑌 ) ⟩ · ( ( 1st𝐺 ) ‘ 𝑌 ) ) ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ 𝐾 ) ) )