evlf2val

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

	Ref	Expression
Hypotheses	evlfval.e	⊢ 𝐸 = ( 𝐶 eval_F 𝐷 )
	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	⊢ 𝐿 = ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑌 ⟩ )
	evlf2val.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) )
	evlf2val.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
Assertion	evlf2val	⊢ ( 𝜑 → ( 𝐴 𝐿 𝐾 ) = ( ( 𝐴 ‘ 𝑌 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlfval.e	⊢ 𝐸 = ( 𝐶 eval_F 𝐷 )
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	⊢ 𝐿 = ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑌 ⟩ )
13		evlf2val.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) )
14		evlf2val.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
15	1 2 3 4 5 6 7 8 9 10 11 12	evlf2	⊢ ( 𝜑 → 𝐿 = ( 𝑎 ∈ ( 𝐹 𝑁 𝐺 ) , 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝑎 ‘ 𝑌 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝑔 ) ) ) )
16		simprl	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑔 = 𝐾 ) ) → 𝑎 = 𝐴 )
17	16	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑔 = 𝐾 ) ) → ( 𝑎 ‘ 𝑌 ) = ( 𝐴 ‘ 𝑌 ) )
18		simprr	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑔 = 𝐾 ) ) → 𝑔 = 𝐾 )
19	18	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑔 = 𝐾 ) ) → ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝑔 ) = ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) )
20	17 19	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑔 = 𝐾 ) ) → ( ( 𝑎 ‘ 𝑌 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝑔 ) ) = ( ( 𝐴 ‘ 𝑌 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) ) )
21		ovexd	⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑌 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) ) ∈ V )
22	15 20 13 14 21	ovmpod	⊢ ( 𝜑 → ( 𝐴 𝐿 𝐾 ) = ( ( 𝐴 ‘ 𝑌 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) ) )

Metamath Proof Explorer

Theorem evlf2val

Proof