evlf1

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

	Ref	Expression
Hypotheses	evlf1.e	\|- E = ( C evalF D )
	evlf1.c	\|- ( ph -> C e. Cat )
	evlf1.d	\|- ( ph -> D e. Cat )
	evlf1.b	\|- B = ( Base ` C )
	evlf1.f	\|- ( ph -> F e. ( C Func D ) )
	evlf1.x	\|- ( ph -> X e. B )
Assertion	evlf1	\|- ( ph -> ( F ( 1st ` E ) X ) = ( ( 1st ` F ) ` X ) )

Proof

Step	Hyp	Ref	Expression
1		evlf1.e	\|- E = ( C evalF D )
2		evlf1.c	\|- ( ph -> C e. Cat )
3		evlf1.d	\|- ( ph -> D e. Cat )
4		evlf1.b	\|- B = ( Base ` C )
5		evlf1.f	\|- ( ph -> F e. ( C Func D ) )
6		evlf1.x	\|- ( ph -> X e. B )
7		eqid	\|- ( Hom ` C ) = ( Hom ` C )
8		eqid	\|- ( comp ` D ) = ( comp ` D )
9		eqid	\|- ( C Nat D ) = ( C Nat D )
10	1 2 3 4 7 8 9	evlfval	\|- ( ph -> E = <. ( f e. ( C Func D ) , x e. B \|-> ( ( 1st ` f ) ` x ) ) , ( x e. ( ( C Func D ) X. B ) , y e. ( ( C Func D ) X. B ) \|-> [_ ( 1st ` x ) / m ]_ [_ ( 1st ` y ) / n ]_ ( a e. ( m ( C Nat D ) n ) , g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) \|-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. ( comp ` D ) ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) ) ) >. )
11		ovex	\|- ( C Func D ) e. _V
12	4	fvexi	\|- B e. _V
13	11 12	mpoex	\|- ( f e. ( C Func D ) , x e. B \|-> ( ( 1st ` f ) ` x ) ) e. _V
14	11 12	xpex	\|- ( ( C Func D ) X. B ) e. _V
15	14 14	mpoex	\|- ( x e. ( ( C Func D ) X. B ) , y e. ( ( C Func D ) X. B ) \|-> [_ ( 1st ` x ) / m ]_ [_ ( 1st ` y ) / n ]_ ( a e. ( m ( C Nat D ) n ) , g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) \|-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. ( comp ` D ) ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) ) ) e. _V
16	13 15	op1std	\|- ( E = <. ( f e. ( C Func D ) , x e. B \|-> ( ( 1st ` f ) ` x ) ) , ( x e. ( ( C Func D ) X. B ) , y e. ( ( C Func D ) X. B ) \|-> [_ ( 1st ` x ) / m ]_ [_ ( 1st ` y ) / n ]_ ( a e. ( m ( C Nat D ) n ) , g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) \|-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. ( comp ` D ) ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) ) ) >. -> ( 1st ` E ) = ( f e. ( C Func D ) , x e. B \|-> ( ( 1st ` f ) ` x ) ) )
17	10 16	syl	\|- ( ph -> ( 1st ` E ) = ( f e. ( C Func D ) , x e. B \|-> ( ( 1st ` f ) ` x ) ) )
18		simprl	\|- ( ( ph /\ ( f = F /\ x = X ) ) -> f = F )
19	18	fveq2d	\|- ( ( ph /\ ( f = F /\ x = X ) ) -> ( 1st ` f ) = ( 1st ` F ) )
20		simprr	\|- ( ( ph /\ ( f = F /\ x = X ) ) -> x = X )
21	19 20	fveq12d	\|- ( ( ph /\ ( f = F /\ x = X ) ) -> ( ( 1st ` f ) ` x ) = ( ( 1st ` F ) ` X ) )
22		fvexd	\|- ( ph -> ( ( 1st ` F ) ` X ) e. _V )
23	17 21 5 6 22	ovmpod	\|- ( ph -> ( F ( 1st ` E ) X ) = ( ( 1st ` F ) ` X ) )

Metamath Proof Explorer

Theorem evlf1

Proof