Metamath Proof Explorer


Theorem natfval

Description: Value of the function giving natural transformations between two categories. (Contributed by Mario Carneiro, 6-Jan-2017) (Proof shortened by AV, 1-Mar-2024)

Ref Expression
Hypotheses natfval.1 N = C Nat D
natfval.b B = Base C
natfval.h H = Hom C
natfval.j J = Hom D
natfval.o · ˙ = comp D
Assertion natfval N = f C Func D , g C Func D 1 st f / r 1 st g / s a x B r x J s x | x B y B h x H y a y r x r y · ˙ s y x 2 nd f y h = x 2 nd g y h r x s x · ˙ s y a x

Proof

Step Hyp Ref Expression
1 natfval.1 N = C Nat D
2 natfval.b B = Base C
3 natfval.h H = Hom C
4 natfval.j J = Hom D
5 natfval.o · ˙ = comp D
6 oveq12 t = C u = D t Func u = C Func D
7 simpl t = C u = D t = C
8 7 fveq2d t = C u = D Base t = Base C
9 8 2 eqtr4di t = C u = D Base t = B
10 9 ixpeq1d t = C u = D x Base t r x Hom u s x = x B r x Hom u s x
11 simpr t = C u = D u = D
12 11 fveq2d t = C u = D Hom u = Hom D
13 12 4 eqtr4di t = C u = D Hom u = J
14 13 oveqd t = C u = D r x Hom u s x = r x J s x
15 14 ixpeq2dv t = C u = D x B r x Hom u s x = x B r x J s x
16 10 15 eqtrd t = C u = D x Base t r x Hom u s x = x B r x J s x
17 7 fveq2d t = C u = D Hom t = Hom C
18 17 3 eqtr4di t = C u = D Hom t = H
19 18 oveqd t = C u = D x Hom t y = x H y
20 11 fveq2d t = C u = D comp u = comp D
21 20 5 eqtr4di t = C u = D comp u = · ˙
22 21 oveqd t = C u = D r x r y comp u s y = r x r y · ˙ s y
23 22 oveqd t = C u = D a y r x r y comp u s y x 2 nd f y h = a y r x r y · ˙ s y x 2 nd f y h
24 21 oveqd t = C u = D r x s x comp u s y = r x s x · ˙ s y
25 24 oveqd t = C u = D x 2 nd g y h r x s x comp u s y a x = x 2 nd g y h r x s x · ˙ s y a x
26 23 25 eqeq12d t = C u = D a y r x r y comp u s y x 2 nd f y h = x 2 nd g y h r x s x comp u s y a x a y r x r y · ˙ s y x 2 nd f y h = x 2 nd g y h r x s x · ˙ s y a x
27 19 26 raleqbidv t = C u = D h x Hom t y a y r x r y comp u s y x 2 nd f y h = x 2 nd g y h r x s x comp u s y a x h x H y a y r x r y · ˙ s y x 2 nd f y h = x 2 nd g y h r x s x · ˙ s y a x
28 9 27 raleqbidv t = C u = D y Base t h x Hom t y a y r x r y comp u s y x 2 nd f y h = x 2 nd g y h r x s x comp u s y a x y B h x H y a y r x r y · ˙ s y x 2 nd f y h = x 2 nd g y h r x s x · ˙ s y a x
29 9 28 raleqbidv t = C u = D x Base t y Base t h x Hom t y a y r x r y comp u s y x 2 nd f y h = x 2 nd g y h r x s x comp u s y a x x B y B h x H y a y r x r y · ˙ s y x 2 nd f y h = x 2 nd g y h r x s x · ˙ s y a x
30 16 29 rabeqbidv t = C u = D a x Base t r x Hom u s x | x Base t y Base t h x Hom t y a y r x r y comp u s y x 2 nd f y h = x 2 nd g y h r x s x comp u s y a x = a x B r x J s x | x B y B h x H y a y r x r y · ˙ s y x 2 nd f y h = x 2 nd g y h r x s x · ˙ s y a x
31 30 csbeq2dv t = C u = D 1 st g / s a x Base t r x Hom u s x | x Base t y Base t h x Hom t y a y r x r y comp u s y x 2 nd f y h = x 2 nd g y h r x s x comp u s y a x = 1 st g / s a x B r x J s x | x B y B h x H y a y r x r y · ˙ s y x 2 nd f y h = x 2 nd g y h r x s x · ˙ s y a x
32 31 csbeq2dv t = C u = D 1 st f / r 1 st g / s a x Base t r x Hom u s x | x Base t y Base t h x Hom t y a y r x r y comp u s y x 2 nd f y h = x 2 nd g y h r x s x comp u s y a x = 1 st f / r 1 st g / s a x B r x J s x | x B y B h x H y a y r x r y · ˙ s y x 2 nd f y h = x 2 nd g y h r x s x · ˙ s y a x
33 6 6 32 mpoeq123dv t = C u = D f t Func u , g t Func u 1 st f / r 1 st g / s a x Base t r x Hom u s x | x Base t y Base t h x Hom t y a y r x r y comp u s y x 2 nd f y h = x 2 nd g y h r x s x comp u s y a x = f C Func D , g C Func D 1 st f / r 1 st g / s a x B r x J s x | x B y B h x H y a y r x r y · ˙ s y x 2 nd f y h = x 2 nd g y h r x s x · ˙ s y a x
34 df-nat Nat = t Cat , u Cat f t Func u , g t Func u 1 st f / r 1 st g / s a x Base t r x Hom u s x | x Base t y Base t h x Hom t y a y r x r y comp u s y x 2 nd f y h = x 2 nd g y h r x s x comp u s y a x
35 ovex C Func D V
36 35 35 mpoex f C Func D , g C Func D 1 st f / r 1 st g / s a x B r x J s x | x B y B h x H y a y r x r y · ˙ s y x 2 nd f y h = x 2 nd g y h r x s x · ˙ s y a x V
37 33 34 36 ovmpoa C Cat D Cat C Nat D = f C Func D , g C Func D 1 st f / r 1 st g / s a x B r x J s x | x B y B h x H y a y r x r y · ˙ s y x 2 nd f y h = x 2 nd g y h r x s x · ˙ s y a x
38 34 mpondm0 ¬ C Cat D Cat C Nat D =
39 funcrcl f C Func D C Cat D Cat
40 39 con3i ¬ C Cat D Cat ¬ f C Func D
41 40 eq0rdv ¬ C Cat D Cat C Func D =
42 41 olcd ¬ C Cat D Cat C Func D = C Func D =
43 0mpo0 C Func D = C Func D = f C Func D , g C Func D 1 st f / r 1 st g / s a x B r x J s x | x B y B h x H y a y r x r y · ˙ s y x 2 nd f y h = x 2 nd g y h r x s x · ˙ s y a x =
44 42 43 syl ¬ C Cat D Cat f C Func D , g C Func D 1 st f / r 1 st g / s a x B r x J s x | x B y B h x H y a y r x r y · ˙ s y x 2 nd f y h = x 2 nd g y h r x s x · ˙ s y a x =
45 38 44 eqtr4d ¬ C Cat D Cat C Nat D = f C Func D , g C Func D 1 st f / r 1 st g / s a x B r x J s x | x B y B h x H y a y r x r y · ˙ s y x 2 nd f y h = x 2 nd g y h r x s x · ˙ s y a x
46 37 45 pm2.61i C Nat D = f C Func D , g C Func D 1 st f / r 1 st g / s a x B r x J s x | x B y B h x H y a y r x r y · ˙ s y x 2 nd f y h = x 2 nd g y h r x s x · ˙ s y a x
47 1 46 eqtri N = f C Func D , g C Func D 1 st f / r 1 st g / s a x B r x J s x | x B y B h x H y a y r x r y · ˙ s y x 2 nd f y h = x 2 nd g y h r x s x · ˙ s y a x