MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  evlf2 Structured version   Visualization version   GIF version

Theorem evlf2 18210
Description: Value of the evaluation functor at a morphism. (Contributed by Mario Carneiro, 12-Jan-2017.)
Hypotheses
Ref Expression
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 โ€˜๐ธ)โŸจ๐บ, ๐‘ŒโŸฉ)
Assertion
Ref Expression
evlf2 (๐œ‘ โ†’ ๐ฟ = (๐‘Ž โˆˆ (๐น๐‘๐บ), ๐‘” โˆˆ (๐‘‹๐ป๐‘Œ) โ†ฆ ((๐‘Žโ€˜๐‘Œ)(โŸจ((1st โ€˜๐น)โ€˜๐‘‹), ((1st โ€˜๐น)โ€˜๐‘Œ)โŸฉ ยท ((1st โ€˜๐บ)โ€˜๐‘Œ))((๐‘‹(2nd โ€˜๐น)๐‘Œ)โ€˜๐‘”))))
Distinct variable groups:   ๐‘”,๐‘Ž,๐ถ   ๐ท,๐‘Ž,๐‘”   ๐‘”,๐ป   ๐น,๐‘Ž,๐‘”   ๐‘,๐‘Ž,๐‘”   ๐บ,๐‘Ž,๐‘”   ๐œ‘,๐‘Ž,๐‘”   ยท ,๐‘Ž,๐‘”   ๐‘‹,๐‘Ž,๐‘”   ๐‘Œ,๐‘Ž,๐‘”
Allowed substitution hints:   ๐ต(๐‘”,๐‘Ž)   ๐ธ(๐‘”,๐‘Ž)   ๐ป(๐‘Ž)   ๐ฟ(๐‘”,๐‘Ž)

Proof of Theorem evlf2
Dummy variables ๐‘“ ๐‘š ๐‘› ๐‘ฅ ๐‘ฆ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 evlf2.l . 2 ๐ฟ = (โŸจ๐น, ๐‘‹โŸฉ(2nd โ€˜๐ธ)โŸจ๐บ, ๐‘ŒโŸฉ)
2 evlfval.e . . . . 5 ๐ธ = (๐ถ evalF ๐ท)
3 evlfval.c . . . . 5 (๐œ‘ โ†’ ๐ถ โˆˆ Cat)
4 evlfval.d . . . . 5 (๐œ‘ โ†’ ๐ท โˆˆ Cat)
5 evlfval.b . . . . 5 ๐ต = (Baseโ€˜๐ถ)
6 evlfval.h . . . . 5 ๐ป = (Hom โ€˜๐ถ)
7 evlfval.o . . . . 5 ยท = (compโ€˜๐ท)
8 evlfval.n . . . . 5 ๐‘ = (๐ถ Nat ๐ท)
92, 3, 4, 5, 6, 7, 8evlfval 18209 . . . 4 (๐œ‘ โ†’ ๐ธ = โŸจ(๐‘“ โˆˆ (๐ถ Func ๐ท), ๐‘ฅ โˆˆ ๐ต โ†ฆ ((1st โ€˜๐‘“)โ€˜๐‘ฅ)), (๐‘ฅ โˆˆ ((๐ถ Func ๐ท) ร— ๐ต), ๐‘ฆ โˆˆ ((๐ถ Func ๐ท) ร— ๐ต) โ†ฆ โฆ‹(1st โ€˜๐‘ฅ) / ๐‘šโฆŒโฆ‹(1st โ€˜๐‘ฆ) / ๐‘›โฆŒ(๐‘Ž โˆˆ (๐‘š๐‘๐‘›), ๐‘” โˆˆ ((2nd โ€˜๐‘ฅ)๐ป(2nd โ€˜๐‘ฆ)) โ†ฆ ((๐‘Žโ€˜(2nd โ€˜๐‘ฆ))(โŸจ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฅ)), ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฆ))โŸฉ ยท ((1st โ€˜๐‘›)โ€˜(2nd โ€˜๐‘ฆ)))(((2nd โ€˜๐‘ฅ)(2nd โ€˜๐‘š)(2nd โ€˜๐‘ฆ))โ€˜๐‘”))))โŸฉ)
10 ovex 7453 . . . . . 6 (๐ถ Func ๐ท) โˆˆ V
115fvexi 6911 . . . . . 6 ๐ต โˆˆ V
1210, 11mpoex 8084 . . . . 5 (๐‘“ โˆˆ (๐ถ Func ๐ท), ๐‘ฅ โˆˆ ๐ต โ†ฆ ((1st โ€˜๐‘“)โ€˜๐‘ฅ)) โˆˆ V
1310, 11xpex 7755 . . . . . 6 ((๐ถ Func ๐ท) ร— ๐ต) โˆˆ V
1413, 13mpoex 8084 . . . . 5 (๐‘ฅ โˆˆ ((๐ถ Func ๐ท) ร— ๐ต), ๐‘ฆ โˆˆ ((๐ถ Func ๐ท) ร— ๐ต) โ†ฆ โฆ‹(1st โ€˜๐‘ฅ) / ๐‘šโฆŒโฆ‹(1st โ€˜๐‘ฆ) / ๐‘›โฆŒ(๐‘Ž โˆˆ (๐‘š๐‘๐‘›), ๐‘” โˆˆ ((2nd โ€˜๐‘ฅ)๐ป(2nd โ€˜๐‘ฆ)) โ†ฆ ((๐‘Žโ€˜(2nd โ€˜๐‘ฆ))(โŸจ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฅ)), ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฆ))โŸฉ ยท ((1st โ€˜๐‘›)โ€˜(2nd โ€˜๐‘ฆ)))(((2nd โ€˜๐‘ฅ)(2nd โ€˜๐‘š)(2nd โ€˜๐‘ฆ))โ€˜๐‘”)))) โˆˆ V
1512, 14op2ndd 8004 . . . 4 (๐ธ = โŸจ(๐‘“ โˆˆ (๐ถ Func ๐ท), ๐‘ฅ โˆˆ ๐ต โ†ฆ ((1st โ€˜๐‘“)โ€˜๐‘ฅ)), (๐‘ฅ โˆˆ ((๐ถ Func ๐ท) ร— ๐ต), ๐‘ฆ โˆˆ ((๐ถ Func ๐ท) ร— ๐ต) โ†ฆ โฆ‹(1st โ€˜๐‘ฅ) / ๐‘šโฆŒโฆ‹(1st โ€˜๐‘ฆ) / ๐‘›โฆŒ(๐‘Ž โˆˆ (๐‘š๐‘๐‘›), ๐‘” โˆˆ ((2nd โ€˜๐‘ฅ)๐ป(2nd โ€˜๐‘ฆ)) โ†ฆ ((๐‘Žโ€˜(2nd โ€˜๐‘ฆ))(โŸจ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฅ)), ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฆ))โŸฉ ยท ((1st โ€˜๐‘›)โ€˜(2nd โ€˜๐‘ฆ)))(((2nd โ€˜๐‘ฅ)(2nd โ€˜๐‘š)(2nd โ€˜๐‘ฆ))โ€˜๐‘”))))โŸฉ โ†’ (2nd โ€˜๐ธ) = (๐‘ฅ โˆˆ ((๐ถ Func ๐ท) ร— ๐ต), ๐‘ฆ โˆˆ ((๐ถ Func ๐ท) ร— ๐ต) โ†ฆ โฆ‹(1st โ€˜๐‘ฅ) / ๐‘šโฆŒโฆ‹(1st โ€˜๐‘ฆ) / ๐‘›โฆŒ(๐‘Ž โˆˆ (๐‘š๐‘๐‘›), ๐‘” โˆˆ ((2nd โ€˜๐‘ฅ)๐ป(2nd โ€˜๐‘ฆ)) โ†ฆ ((๐‘Žโ€˜(2nd โ€˜๐‘ฆ))(โŸจ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฅ)), ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฆ))โŸฉ ยท ((1st โ€˜๐‘›)โ€˜(2nd โ€˜๐‘ฆ)))(((2nd โ€˜๐‘ฅ)(2nd โ€˜๐‘š)(2nd โ€˜๐‘ฆ))โ€˜๐‘”)))))
169, 15syl 17 . . 3 (๐œ‘ โ†’ (2nd โ€˜๐ธ) = (๐‘ฅ โˆˆ ((๐ถ Func ๐ท) ร— ๐ต), ๐‘ฆ โˆˆ ((๐ถ Func ๐ท) ร— ๐ต) โ†ฆ โฆ‹(1st โ€˜๐‘ฅ) / ๐‘šโฆŒโฆ‹(1st โ€˜๐‘ฆ) / ๐‘›โฆŒ(๐‘Ž โˆˆ (๐‘š๐‘๐‘›), ๐‘” โˆˆ ((2nd โ€˜๐‘ฅ)๐ป(2nd โ€˜๐‘ฆ)) โ†ฆ ((๐‘Žโ€˜(2nd โ€˜๐‘ฆ))(โŸจ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฅ)), ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฆ))โŸฉ ยท ((1st โ€˜๐‘›)โ€˜(2nd โ€˜๐‘ฆ)))(((2nd โ€˜๐‘ฅ)(2nd โ€˜๐‘š)(2nd โ€˜๐‘ฆ))โ€˜๐‘”)))))
17 fvexd 6912 . . . 4 ((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โ†’ (1st โ€˜๐‘ฅ) โˆˆ V)
18 simprl 770 . . . . . 6 ((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โ†’ ๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ)
1918fveq2d 6901 . . . . 5 ((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โ†’ (1st โ€˜๐‘ฅ) = (1st โ€˜โŸจ๐น, ๐‘‹โŸฉ))
20 evlf2.f . . . . . . 7 (๐œ‘ โ†’ ๐น โˆˆ (๐ถ Func ๐ท))
21 evlf2.x . . . . . . 7 (๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต)
22 op1stg 8005 . . . . . . 7 ((๐น โˆˆ (๐ถ Func ๐ท) โˆง ๐‘‹ โˆˆ ๐ต) โ†’ (1st โ€˜โŸจ๐น, ๐‘‹โŸฉ) = ๐น)
2320, 21, 22syl2anc 583 . . . . . 6 (๐œ‘ โ†’ (1st โ€˜โŸจ๐น, ๐‘‹โŸฉ) = ๐น)
2423adantr 480 . . . . 5 ((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โ†’ (1st โ€˜โŸจ๐น, ๐‘‹โŸฉ) = ๐น)
2519, 24eqtrd 2768 . . . 4 ((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โ†’ (1st โ€˜๐‘ฅ) = ๐น)
26 fvexd 6912 . . . . 5 (((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โ†’ (1st โ€˜๐‘ฆ) โˆˆ V)
27 simplrr 777 . . . . . . 7 (((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โ†’ ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)
2827fveq2d 6901 . . . . . 6 (((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โ†’ (1st โ€˜๐‘ฆ) = (1st โ€˜โŸจ๐บ, ๐‘ŒโŸฉ))
29 evlf2.g . . . . . . . 8 (๐œ‘ โ†’ ๐บ โˆˆ (๐ถ Func ๐ท))
30 evlf2.y . . . . . . . 8 (๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ต)
31 op1stg 8005 . . . . . . . 8 ((๐บ โˆˆ (๐ถ Func ๐ท) โˆง ๐‘Œ โˆˆ ๐ต) โ†’ (1st โ€˜โŸจ๐บ, ๐‘ŒโŸฉ) = ๐บ)
3229, 30, 31syl2anc 583 . . . . . . 7 (๐œ‘ โ†’ (1st โ€˜โŸจ๐บ, ๐‘ŒโŸฉ) = ๐บ)
3332ad2antrr 725 . . . . . 6 (((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โ†’ (1st โ€˜โŸจ๐บ, ๐‘ŒโŸฉ) = ๐บ)
3428, 33eqtrd 2768 . . . . 5 (((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โ†’ (1st โ€˜๐‘ฆ) = ๐บ)
35 simplr 768 . . . . . . 7 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ ๐‘š = ๐น)
36 simpr 484 . . . . . . 7 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ ๐‘› = ๐บ)
3735, 36oveq12d 7438 . . . . . 6 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ (๐‘š๐‘๐‘›) = (๐น๐‘๐บ))
3818ad2antrr 725 . . . . . . . . 9 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ ๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ)
3938fveq2d 6901 . . . . . . . 8 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ (2nd โ€˜๐‘ฅ) = (2nd โ€˜โŸจ๐น, ๐‘‹โŸฉ))
40 op2ndg 8006 . . . . . . . . . 10 ((๐น โˆˆ (๐ถ Func ๐ท) โˆง ๐‘‹ โˆˆ ๐ต) โ†’ (2nd โ€˜โŸจ๐น, ๐‘‹โŸฉ) = ๐‘‹)
4120, 21, 40syl2anc 583 . . . . . . . . 9 (๐œ‘ โ†’ (2nd โ€˜โŸจ๐น, ๐‘‹โŸฉ) = ๐‘‹)
4241ad3antrrr 729 . . . . . . . 8 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ (2nd โ€˜โŸจ๐น, ๐‘‹โŸฉ) = ๐‘‹)
4339, 42eqtrd 2768 . . . . . . 7 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ (2nd โ€˜๐‘ฅ) = ๐‘‹)
4427adantr 480 . . . . . . . . 9 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)
4544fveq2d 6901 . . . . . . . 8 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ (2nd โ€˜๐‘ฆ) = (2nd โ€˜โŸจ๐บ, ๐‘ŒโŸฉ))
46 op2ndg 8006 . . . . . . . . . 10 ((๐บ โˆˆ (๐ถ Func ๐ท) โˆง ๐‘Œ โˆˆ ๐ต) โ†’ (2nd โ€˜โŸจ๐บ, ๐‘ŒโŸฉ) = ๐‘Œ)
4729, 30, 46syl2anc 583 . . . . . . . . 9 (๐œ‘ โ†’ (2nd โ€˜โŸจ๐บ, ๐‘ŒโŸฉ) = ๐‘Œ)
4847ad3antrrr 729 . . . . . . . 8 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ (2nd โ€˜โŸจ๐บ, ๐‘ŒโŸฉ) = ๐‘Œ)
4945, 48eqtrd 2768 . . . . . . 7 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ (2nd โ€˜๐‘ฆ) = ๐‘Œ)
5043, 49oveq12d 7438 . . . . . 6 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ ((2nd โ€˜๐‘ฅ)๐ป(2nd โ€˜๐‘ฆ)) = (๐‘‹๐ป๐‘Œ))
5135fveq2d 6901 . . . . . . . . . 10 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ (1st โ€˜๐‘š) = (1st โ€˜๐น))
5251, 43fveq12d 6904 . . . . . . . . 9 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฅ)) = ((1st โ€˜๐น)โ€˜๐‘‹))
5351, 49fveq12d 6904 . . . . . . . . 9 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฆ)) = ((1st โ€˜๐น)โ€˜๐‘Œ))
5452, 53opeq12d 4882 . . . . . . . 8 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ โŸจ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฅ)), ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฆ))โŸฉ = โŸจ((1st โ€˜๐น)โ€˜๐‘‹), ((1st โ€˜๐น)โ€˜๐‘Œ)โŸฉ)
5536fveq2d 6901 . . . . . . . . 9 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ (1st โ€˜๐‘›) = (1st โ€˜๐บ))
5655, 49fveq12d 6904 . . . . . . . 8 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ ((1st โ€˜๐‘›)โ€˜(2nd โ€˜๐‘ฆ)) = ((1st โ€˜๐บ)โ€˜๐‘Œ))
5754, 56oveq12d 7438 . . . . . . 7 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ (โŸจ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฅ)), ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฆ))โŸฉ ยท ((1st โ€˜๐‘›)โ€˜(2nd โ€˜๐‘ฆ))) = (โŸจ((1st โ€˜๐น)โ€˜๐‘‹), ((1st โ€˜๐น)โ€˜๐‘Œ)โŸฉ ยท ((1st โ€˜๐บ)โ€˜๐‘Œ)))
5849fveq2d 6901 . . . . . . 7 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ (๐‘Žโ€˜(2nd โ€˜๐‘ฆ)) = (๐‘Žโ€˜๐‘Œ))
5935fveq2d 6901 . . . . . . . . 9 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ (2nd โ€˜๐‘š) = (2nd โ€˜๐น))
6059, 43, 49oveq123d 7441 . . . . . . . 8 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ ((2nd โ€˜๐‘ฅ)(2nd โ€˜๐‘š)(2nd โ€˜๐‘ฆ)) = (๐‘‹(2nd โ€˜๐น)๐‘Œ))
6160fveq1d 6899 . . . . . . 7 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ (((2nd โ€˜๐‘ฅ)(2nd โ€˜๐‘š)(2nd โ€˜๐‘ฆ))โ€˜๐‘”) = ((๐‘‹(2nd โ€˜๐น)๐‘Œ)โ€˜๐‘”))
6257, 58, 61oveq123d 7441 . . . . . 6 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ ((๐‘Žโ€˜(2nd โ€˜๐‘ฆ))(โŸจ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฅ)), ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฆ))โŸฉ ยท ((1st โ€˜๐‘›)โ€˜(2nd โ€˜๐‘ฆ)))(((2nd โ€˜๐‘ฅ)(2nd โ€˜๐‘š)(2nd โ€˜๐‘ฆ))โ€˜๐‘”)) = ((๐‘Žโ€˜๐‘Œ)(โŸจ((1st โ€˜๐น)โ€˜๐‘‹), ((1st โ€˜๐น)โ€˜๐‘Œ)โŸฉ ยท ((1st โ€˜๐บ)โ€˜๐‘Œ))((๐‘‹(2nd โ€˜๐น)๐‘Œ)โ€˜๐‘”)))
6337, 50, 62mpoeq123dv 7495 . . . . 5 ((((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โˆง ๐‘› = ๐บ) โ†’ (๐‘Ž โˆˆ (๐‘š๐‘๐‘›), ๐‘” โˆˆ ((2nd โ€˜๐‘ฅ)๐ป(2nd โ€˜๐‘ฆ)) โ†ฆ ((๐‘Žโ€˜(2nd โ€˜๐‘ฆ))(โŸจ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฅ)), ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฆ))โŸฉ ยท ((1st โ€˜๐‘›)โ€˜(2nd โ€˜๐‘ฆ)))(((2nd โ€˜๐‘ฅ)(2nd โ€˜๐‘š)(2nd โ€˜๐‘ฆ))โ€˜๐‘”))) = (๐‘Ž โˆˆ (๐น๐‘๐บ), ๐‘” โˆˆ (๐‘‹๐ป๐‘Œ) โ†ฆ ((๐‘Žโ€˜๐‘Œ)(โŸจ((1st โ€˜๐น)โ€˜๐‘‹), ((1st โ€˜๐น)โ€˜๐‘Œ)โŸฉ ยท ((1st โ€˜๐บ)โ€˜๐‘Œ))((๐‘‹(2nd โ€˜๐น)๐‘Œ)โ€˜๐‘”))))
6426, 34, 63csbied2 3932 . . . 4 (((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โˆง ๐‘š = ๐น) โ†’ โฆ‹(1st โ€˜๐‘ฆ) / ๐‘›โฆŒ(๐‘Ž โˆˆ (๐‘š๐‘๐‘›), ๐‘” โˆˆ ((2nd โ€˜๐‘ฅ)๐ป(2nd โ€˜๐‘ฆ)) โ†ฆ ((๐‘Žโ€˜(2nd โ€˜๐‘ฆ))(โŸจ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฅ)), ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฆ))โŸฉ ยท ((1st โ€˜๐‘›)โ€˜(2nd โ€˜๐‘ฆ)))(((2nd โ€˜๐‘ฅ)(2nd โ€˜๐‘š)(2nd โ€˜๐‘ฆ))โ€˜๐‘”))) = (๐‘Ž โˆˆ (๐น๐‘๐บ), ๐‘” โˆˆ (๐‘‹๐ป๐‘Œ) โ†ฆ ((๐‘Žโ€˜๐‘Œ)(โŸจ((1st โ€˜๐น)โ€˜๐‘‹), ((1st โ€˜๐น)โ€˜๐‘Œ)โŸฉ ยท ((1st โ€˜๐บ)โ€˜๐‘Œ))((๐‘‹(2nd โ€˜๐น)๐‘Œ)โ€˜๐‘”))))
6517, 25, 64csbied2 3932 . . 3 ((๐œ‘ โˆง (๐‘ฅ = โŸจ๐น, ๐‘‹โŸฉ โˆง ๐‘ฆ = โŸจ๐บ, ๐‘ŒโŸฉ)) โ†’ โฆ‹(1st โ€˜๐‘ฅ) / ๐‘šโฆŒโฆ‹(1st โ€˜๐‘ฆ) / ๐‘›โฆŒ(๐‘Ž โˆˆ (๐‘š๐‘๐‘›), ๐‘” โˆˆ ((2nd โ€˜๐‘ฅ)๐ป(2nd โ€˜๐‘ฆ)) โ†ฆ ((๐‘Žโ€˜(2nd โ€˜๐‘ฆ))(โŸจ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฅ)), ((1st โ€˜๐‘š)โ€˜(2nd โ€˜๐‘ฆ))โŸฉ ยท ((1st โ€˜๐‘›)โ€˜(2nd โ€˜๐‘ฆ)))(((2nd โ€˜๐‘ฅ)(2nd โ€˜๐‘š)(2nd โ€˜๐‘ฆ))โ€˜๐‘”))) = (๐‘Ž โˆˆ (๐น๐‘๐บ), ๐‘” โˆˆ (๐‘‹๐ป๐‘Œ) โ†ฆ ((๐‘Žโ€˜๐‘Œ)(โŸจ((1st โ€˜๐น)โ€˜๐‘‹), ((1st โ€˜๐น)โ€˜๐‘Œ)โŸฉ ยท ((1st โ€˜๐บ)โ€˜๐‘Œ))((๐‘‹(2nd โ€˜๐น)๐‘Œ)โ€˜๐‘”))))
6620, 21opelxpd 5717 . . 3 (๐œ‘ โ†’ โŸจ๐น, ๐‘‹โŸฉ โˆˆ ((๐ถ Func ๐ท) ร— ๐ต))
6729, 30opelxpd 5717 . . 3 (๐œ‘ โ†’ โŸจ๐บ, ๐‘ŒโŸฉ โˆˆ ((๐ถ Func ๐ท) ร— ๐ต))
68 ovex 7453 . . . . 5 (๐น๐‘๐บ) โˆˆ V
69 ovex 7453 . . . . 5 (๐‘‹๐ป๐‘Œ) โˆˆ V
7068, 69mpoex 8084 . . . 4 (๐‘Ž โˆˆ (๐น๐‘๐บ), ๐‘” โˆˆ (๐‘‹๐ป๐‘Œ) โ†ฆ ((๐‘Žโ€˜๐‘Œ)(โŸจ((1st โ€˜๐น)โ€˜๐‘‹), ((1st โ€˜๐น)โ€˜๐‘Œ)โŸฉ ยท ((1st โ€˜๐บ)โ€˜๐‘Œ))((๐‘‹(2nd โ€˜๐น)๐‘Œ)โ€˜๐‘”))) โˆˆ V
7170a1i 11 . . 3 (๐œ‘ โ†’ (๐‘Ž โˆˆ (๐น๐‘๐บ), ๐‘” โˆˆ (๐‘‹๐ป๐‘Œ) โ†ฆ ((๐‘Žโ€˜๐‘Œ)(โŸจ((1st โ€˜๐น)โ€˜๐‘‹), ((1st โ€˜๐น)โ€˜๐‘Œ)โŸฉ ยท ((1st โ€˜๐บ)โ€˜๐‘Œ))((๐‘‹(2nd โ€˜๐น)๐‘Œ)โ€˜๐‘”))) โˆˆ V)
7216, 65, 66, 67, 71ovmpod 7573 . 2 (๐œ‘ โ†’ (โŸจ๐น, ๐‘‹โŸฉ(2nd โ€˜๐ธ)โŸจ๐บ, ๐‘ŒโŸฉ) = (๐‘Ž โˆˆ (๐น๐‘๐บ), ๐‘” โˆˆ (๐‘‹๐ป๐‘Œ) โ†ฆ ((๐‘Žโ€˜๐‘Œ)(โŸจ((1st โ€˜๐น)โ€˜๐‘‹), ((1st โ€˜๐น)โ€˜๐‘Œ)โŸฉ ยท ((1st โ€˜๐บ)โ€˜๐‘Œ))((๐‘‹(2nd โ€˜๐น)๐‘Œ)โ€˜๐‘”))))
731, 72eqtrid 2780 1 (๐œ‘ โ†’ ๐ฟ = (๐‘Ž โˆˆ (๐น๐‘๐บ), ๐‘” โˆˆ (๐‘‹๐ป๐‘Œ) โ†ฆ ((๐‘Žโ€˜๐‘Œ)(โŸจ((1st โ€˜๐น)โ€˜๐‘‹), ((1st โ€˜๐น)โ€˜๐‘Œ)โŸฉ ยท ((1st โ€˜๐บ)โ€˜๐‘Œ))((๐‘‹(2nd โ€˜๐น)๐‘Œ)โ€˜๐‘”))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 395   = wceq 1534   โˆˆ wcel 2099  Vcvv 3471  โฆ‹csb 3892  โŸจcop 4635   ร— cxp 5676  โ€˜cfv 6548  (class class class)co 7420   โˆˆ cmpo 7422  1st c1st 7991  2nd c2nd 7992  Basecbs 17180  Hom chom 17244  compcco 17245  Catccat 17644   Func cfunc 17840   Nat cnat 17931   evalF cevlf 18201
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-ov 7423  df-oprab 7424  df-mpo 7425  df-1st 7993  df-2nd 7994  df-evlf 18205
This theorem is referenced by:  evlf2val  18211  evlfcl  18214
  Copyright terms: Public domain W3C validator