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

Theorem catass 17637
Description: Associativity of composition in a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
catcocl.b ๐ต = (Baseโ€˜๐ถ)
catcocl.h ๐ป = (Hom โ€˜๐ถ)
catcocl.o ยท = (compโ€˜๐ถ)
catcocl.c (๐œ‘ โ†’ ๐ถ โˆˆ Cat)
catcocl.x (๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต)
catcocl.y (๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ต)
catcocl.z (๐œ‘ โ†’ ๐‘ โˆˆ ๐ต)
catcocl.f (๐œ‘ โ†’ ๐น โˆˆ (๐‘‹๐ป๐‘Œ))
catcocl.g (๐œ‘ โ†’ ๐บ โˆˆ (๐‘Œ๐ป๐‘))
catass.w (๐œ‘ โ†’ ๐‘Š โˆˆ ๐ต)
catass.g (๐œ‘ โ†’ ๐พ โˆˆ (๐‘๐ป๐‘Š))
Assertion
Ref Expression
catass (๐œ‘ โ†’ ((๐พ(โŸจ๐‘Œ, ๐‘โŸฉ ยท ๐‘Š)๐บ)(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘Š)๐น) = (๐พ(โŸจ๐‘‹, ๐‘โŸฉ ยท ๐‘Š)(๐บ(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น)))

Proof of Theorem catass
Dummy variables ๐‘“ ๐‘” ๐‘˜ ๐‘ค ๐‘ฅ ๐‘ฆ ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 catcocl.c . . 3 (๐œ‘ โ†’ ๐ถ โˆˆ Cat)
2 catcocl.b . . . . 5 ๐ต = (Baseโ€˜๐ถ)
3 catcocl.h . . . . 5 ๐ป = (Hom โ€˜๐ถ)
4 catcocl.o . . . . 5 ยท = (compโ€˜๐ถ)
52, 3, 4iscat 17623 . . . 4 (๐ถ โˆˆ Cat โ†’ (๐ถ โˆˆ Cat โ†” โˆ€๐‘ฅ โˆˆ ๐ต (โˆƒ๐‘” โˆˆ (๐‘ฅ๐ป๐‘ฅ)โˆ€๐‘ฆ โˆˆ ๐ต (โˆ€๐‘“ โˆˆ (๐‘ฆ๐ป๐‘ฅ)(๐‘”(โŸจ๐‘ฆ, ๐‘ฅโŸฉ ยท ๐‘ฅ)๐‘“) = ๐‘“ โˆง โˆ€๐‘“ โˆˆ (๐‘ฅ๐ป๐‘ฆ)(๐‘“(โŸจ๐‘ฅ, ๐‘ฅโŸฉ ยท ๐‘ฆ)๐‘”) = ๐‘“) โˆง โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘“ โˆˆ (๐‘ฅ๐ป๐‘ฆ)โˆ€๐‘” โˆˆ (๐‘ฆ๐ป๐‘ง)((๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ฅ๐ป๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต โˆ€๐‘˜ โˆˆ (๐‘ง๐ป๐‘ค)((๐‘˜(โŸจ๐‘ฆ, ๐‘งโŸฉ ยท ๐‘ค)๐‘”)(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ค)๐‘“) = (๐‘˜(โŸจ๐‘ฅ, ๐‘งโŸฉ ยท ๐‘ค)(๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“))))))
65ibi 267 . . 3 (๐ถ โˆˆ Cat โ†’ โˆ€๐‘ฅ โˆˆ ๐ต (โˆƒ๐‘” โˆˆ (๐‘ฅ๐ป๐‘ฅ)โˆ€๐‘ฆ โˆˆ ๐ต (โˆ€๐‘“ โˆˆ (๐‘ฆ๐ป๐‘ฅ)(๐‘”(โŸจ๐‘ฆ, ๐‘ฅโŸฉ ยท ๐‘ฅ)๐‘“) = ๐‘“ โˆง โˆ€๐‘“ โˆˆ (๐‘ฅ๐ป๐‘ฆ)(๐‘“(โŸจ๐‘ฅ, ๐‘ฅโŸฉ ยท ๐‘ฆ)๐‘”) = ๐‘“) โˆง โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘“ โˆˆ (๐‘ฅ๐ป๐‘ฆ)โˆ€๐‘” โˆˆ (๐‘ฆ๐ป๐‘ง)((๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ฅ๐ป๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต โˆ€๐‘˜ โˆˆ (๐‘ง๐ป๐‘ค)((๐‘˜(โŸจ๐‘ฆ, ๐‘งโŸฉ ยท ๐‘ค)๐‘”)(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ค)๐‘“) = (๐‘˜(โŸจ๐‘ฅ, ๐‘งโŸฉ ยท ๐‘ค)(๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“)))))
71, 6syl 17 . 2 (๐œ‘ โ†’ โˆ€๐‘ฅ โˆˆ ๐ต (โˆƒ๐‘” โˆˆ (๐‘ฅ๐ป๐‘ฅ)โˆ€๐‘ฆ โˆˆ ๐ต (โˆ€๐‘“ โˆˆ (๐‘ฆ๐ป๐‘ฅ)(๐‘”(โŸจ๐‘ฆ, ๐‘ฅโŸฉ ยท ๐‘ฅ)๐‘“) = ๐‘“ โˆง โˆ€๐‘“ โˆˆ (๐‘ฅ๐ป๐‘ฆ)(๐‘“(โŸจ๐‘ฅ, ๐‘ฅโŸฉ ยท ๐‘ฆ)๐‘”) = ๐‘“) โˆง โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘“ โˆˆ (๐‘ฅ๐ป๐‘ฆ)โˆ€๐‘” โˆˆ (๐‘ฆ๐ป๐‘ง)((๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ฅ๐ป๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต โˆ€๐‘˜ โˆˆ (๐‘ง๐ป๐‘ค)((๐‘˜(โŸจ๐‘ฆ, ๐‘งโŸฉ ยท ๐‘ค)๐‘”)(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ค)๐‘“) = (๐‘˜(โŸจ๐‘ฅ, ๐‘งโŸฉ ยท ๐‘ค)(๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“)))))
8 catcocl.x . . 3 (๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต)
9 catcocl.y . . . . . 6 (๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ต)
109adantr 480 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โ†’ ๐‘Œ โˆˆ ๐ต)
11 catcocl.z . . . . . . 7 (๐œ‘ โ†’ ๐‘ โˆˆ ๐ต)
1211ad2antrr 723 . . . . . 6 (((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โ†’ ๐‘ โˆˆ ๐ต)
13 catcocl.f . . . . . . . . 9 (๐œ‘ โ†’ ๐น โˆˆ (๐‘‹๐ป๐‘Œ))
1413ad3antrrr 727 . . . . . . . 8 ((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โ†’ ๐น โˆˆ (๐‘‹๐ป๐‘Œ))
15 simpllr 773 . . . . . . . . 9 ((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โ†’ ๐‘ฅ = ๐‘‹)
16 simplr 766 . . . . . . . . 9 ((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โ†’ ๐‘ฆ = ๐‘Œ)
1715, 16oveq12d 7422 . . . . . . . 8 ((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โ†’ (๐‘ฅ๐ป๐‘ฆ) = (๐‘‹๐ป๐‘Œ))
1814, 17eleqtrrd 2830 . . . . . . 7 ((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โ†’ ๐น โˆˆ (๐‘ฅ๐ป๐‘ฆ))
19 catcocl.g . . . . . . . . . 10 (๐œ‘ โ†’ ๐บ โˆˆ (๐‘Œ๐ป๐‘))
2019ad4antr 729 . . . . . . . . 9 (((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โ†’ ๐บ โˆˆ (๐‘Œ๐ป๐‘))
21 simpllr 773 . . . . . . . . . 10 (((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โ†’ ๐‘ฆ = ๐‘Œ)
22 simplr 766 . . . . . . . . . 10 (((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โ†’ ๐‘ง = ๐‘)
2321, 22oveq12d 7422 . . . . . . . . 9 (((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โ†’ (๐‘ฆ๐ป๐‘ง) = (๐‘Œ๐ป๐‘))
2420, 23eleqtrrd 2830 . . . . . . . 8 (((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โ†’ ๐บ โˆˆ (๐‘ฆ๐ป๐‘ง))
25 catass.w . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘Š โˆˆ ๐ต)
2625ad5antr 731 . . . . . . . . . 10 ((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โ†’ ๐‘Š โˆˆ ๐ต)
27 catass.g . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐พ โˆˆ (๐‘๐ป๐‘Š))
2827ad6antr 733 . . . . . . . . . . . 12 (((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โ†’ ๐พ โˆˆ (๐‘๐ป๐‘Š))
29 simp-4r 781 . . . . . . . . . . . . 13 (((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โ†’ ๐‘ง = ๐‘)
30 simpr 484 . . . . . . . . . . . . 13 (((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โ†’ ๐‘ค = ๐‘Š)
3129, 30oveq12d 7422 . . . . . . . . . . . 12 (((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โ†’ (๐‘ง๐ป๐‘ค) = (๐‘๐ป๐‘Š))
3228, 31eleqtrrd 2830 . . . . . . . . . . 11 (((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โ†’ ๐พ โˆˆ (๐‘ง๐ป๐‘ค))
33 simp-7r 787 . . . . . . . . . . . . . . 15 ((((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โˆง ๐‘˜ = ๐พ) โ†’ ๐‘ฅ = ๐‘‹)
34 simp-6r 785 . . . . . . . . . . . . . . 15 ((((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โˆง ๐‘˜ = ๐พ) โ†’ ๐‘ฆ = ๐‘Œ)
3533, 34opeq12d 4876 . . . . . . . . . . . . . 14 ((((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โˆง ๐‘˜ = ๐พ) โ†’ โŸจ๐‘ฅ, ๐‘ฆโŸฉ = โŸจ๐‘‹, ๐‘ŒโŸฉ)
36 simplr 766 . . . . . . . . . . . . . 14 ((((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โˆง ๐‘˜ = ๐พ) โ†’ ๐‘ค = ๐‘Š)
3735, 36oveq12d 7422 . . . . . . . . . . . . 13 ((((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โˆง ๐‘˜ = ๐พ) โ†’ (โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ค) = (โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘Š))
38 simp-5r 783 . . . . . . . . . . . . . . . 16 ((((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โˆง ๐‘˜ = ๐พ) โ†’ ๐‘ง = ๐‘)
3934, 38opeq12d 4876 . . . . . . . . . . . . . . 15 ((((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โˆง ๐‘˜ = ๐พ) โ†’ โŸจ๐‘ฆ, ๐‘งโŸฉ = โŸจ๐‘Œ, ๐‘โŸฉ)
4039, 36oveq12d 7422 . . . . . . . . . . . . . 14 ((((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โˆง ๐‘˜ = ๐พ) โ†’ (โŸจ๐‘ฆ, ๐‘งโŸฉ ยท ๐‘ค) = (โŸจ๐‘Œ, ๐‘โŸฉ ยท ๐‘Š))
41 simpr 484 . . . . . . . . . . . . . 14 ((((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โˆง ๐‘˜ = ๐พ) โ†’ ๐‘˜ = ๐พ)
42 simpllr 773 . . . . . . . . . . . . . 14 ((((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โˆง ๐‘˜ = ๐พ) โ†’ ๐‘” = ๐บ)
4340, 41, 42oveq123d 7425 . . . . . . . . . . . . 13 ((((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โˆง ๐‘˜ = ๐พ) โ†’ (๐‘˜(โŸจ๐‘ฆ, ๐‘งโŸฉ ยท ๐‘ค)๐‘”) = (๐พ(โŸจ๐‘Œ, ๐‘โŸฉ ยท ๐‘Š)๐บ))
44 simp-4r 781 . . . . . . . . . . . . 13 ((((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โˆง ๐‘˜ = ๐พ) โ†’ ๐‘“ = ๐น)
4537, 43, 44oveq123d 7425 . . . . . . . . . . . 12 ((((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โˆง ๐‘˜ = ๐พ) โ†’ ((๐‘˜(โŸจ๐‘ฆ, ๐‘งโŸฉ ยท ๐‘ค)๐‘”)(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ค)๐‘“) = ((๐พ(โŸจ๐‘Œ, ๐‘โŸฉ ยท ๐‘Š)๐บ)(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘Š)๐น))
4633, 38opeq12d 4876 . . . . . . . . . . . . . 14 ((((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โˆง ๐‘˜ = ๐พ) โ†’ โŸจ๐‘ฅ, ๐‘งโŸฉ = โŸจ๐‘‹, ๐‘โŸฉ)
4746, 36oveq12d 7422 . . . . . . . . . . . . 13 ((((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โˆง ๐‘˜ = ๐พ) โ†’ (โŸจ๐‘ฅ, ๐‘งโŸฉ ยท ๐‘ค) = (โŸจ๐‘‹, ๐‘โŸฉ ยท ๐‘Š))
4835, 38oveq12d 7422 . . . . . . . . . . . . . 14 ((((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โˆง ๐‘˜ = ๐พ) โ†’ (โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง) = (โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘))
4948, 42, 44oveq123d 7425 . . . . . . . . . . . . 13 ((((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โˆง ๐‘˜ = ๐พ) โ†’ (๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) = (๐บ(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น))
5047, 41, 49oveq123d 7425 . . . . . . . . . . . 12 ((((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โˆง ๐‘˜ = ๐พ) โ†’ (๐‘˜(โŸจ๐‘ฅ, ๐‘งโŸฉ ยท ๐‘ค)(๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“)) = (๐พ(โŸจ๐‘‹, ๐‘โŸฉ ยท ๐‘Š)(๐บ(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น)))
5145, 50eqeq12d 2742 . . . . . . . . . . 11 ((((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โˆง ๐‘˜ = ๐พ) โ†’ (((๐‘˜(โŸจ๐‘ฆ, ๐‘งโŸฉ ยท ๐‘ค)๐‘”)(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ค)๐‘“) = (๐‘˜(โŸจ๐‘ฅ, ๐‘งโŸฉ ยท ๐‘ค)(๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“)) โ†” ((๐พ(โŸจ๐‘Œ, ๐‘โŸฉ ยท ๐‘Š)๐บ)(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘Š)๐น) = (๐พ(โŸจ๐‘‹, ๐‘โŸฉ ยท ๐‘Š)(๐บ(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น))))
5232, 51rspcdv 3598 . . . . . . . . . 10 (((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โˆง ๐‘ค = ๐‘Š) โ†’ (โˆ€๐‘˜ โˆˆ (๐‘ง๐ป๐‘ค)((๐‘˜(โŸจ๐‘ฆ, ๐‘งโŸฉ ยท ๐‘ค)๐‘”)(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ค)๐‘“) = (๐‘˜(โŸจ๐‘ฅ, ๐‘งโŸฉ ยท ๐‘ค)(๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“)) โ†’ ((๐พ(โŸจ๐‘Œ, ๐‘โŸฉ ยท ๐‘Š)๐บ)(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘Š)๐น) = (๐พ(โŸจ๐‘‹, ๐‘โŸฉ ยท ๐‘Š)(๐บ(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น))))
5326, 52rspcimdv 3596 . . . . . . . . 9 ((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โ†’ (โˆ€๐‘ค โˆˆ ๐ต โˆ€๐‘˜ โˆˆ (๐‘ง๐ป๐‘ค)((๐‘˜(โŸจ๐‘ฆ, ๐‘งโŸฉ ยท ๐‘ค)๐‘”)(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ค)๐‘“) = (๐‘˜(โŸจ๐‘ฅ, ๐‘งโŸฉ ยท ๐‘ค)(๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“)) โ†’ ((๐พ(โŸจ๐‘Œ, ๐‘โŸฉ ยท ๐‘Š)๐บ)(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘Š)๐น) = (๐พ(โŸจ๐‘‹, ๐‘โŸฉ ยท ๐‘Š)(๐บ(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น))))
5453adantld 490 . . . . . . . 8 ((((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โˆง ๐‘” = ๐บ) โ†’ (((๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ฅ๐ป๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต โˆ€๐‘˜ โˆˆ (๐‘ง๐ป๐‘ค)((๐‘˜(โŸจ๐‘ฆ, ๐‘งโŸฉ ยท ๐‘ค)๐‘”)(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ค)๐‘“) = (๐‘˜(โŸจ๐‘ฅ, ๐‘งโŸฉ ยท ๐‘ค)(๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“))) โ†’ ((๐พ(โŸจ๐‘Œ, ๐‘โŸฉ ยท ๐‘Š)๐บ)(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘Š)๐น) = (๐พ(โŸจ๐‘‹, ๐‘โŸฉ ยท ๐‘Š)(๐บ(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น))))
5524, 54rspcimdv 3596 . . . . . . 7 (((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โˆง ๐‘“ = ๐น) โ†’ (โˆ€๐‘” โˆˆ (๐‘ฆ๐ป๐‘ง)((๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ฅ๐ป๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต โˆ€๐‘˜ โˆˆ (๐‘ง๐ป๐‘ค)((๐‘˜(โŸจ๐‘ฆ, ๐‘งโŸฉ ยท ๐‘ค)๐‘”)(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ค)๐‘“) = (๐‘˜(โŸจ๐‘ฅ, ๐‘งโŸฉ ยท ๐‘ค)(๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“))) โ†’ ((๐พ(โŸจ๐‘Œ, ๐‘โŸฉ ยท ๐‘Š)๐บ)(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘Š)๐น) = (๐พ(โŸจ๐‘‹, ๐‘โŸฉ ยท ๐‘Š)(๐บ(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น))))
5618, 55rspcimdv 3596 . . . . . 6 ((((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โˆง ๐‘ง = ๐‘) โ†’ (โˆ€๐‘“ โˆˆ (๐‘ฅ๐ป๐‘ฆ)โˆ€๐‘” โˆˆ (๐‘ฆ๐ป๐‘ง)((๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ฅ๐ป๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต โˆ€๐‘˜ โˆˆ (๐‘ง๐ป๐‘ค)((๐‘˜(โŸจ๐‘ฆ, ๐‘งโŸฉ ยท ๐‘ค)๐‘”)(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ค)๐‘“) = (๐‘˜(โŸจ๐‘ฅ, ๐‘งโŸฉ ยท ๐‘ค)(๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“))) โ†’ ((๐พ(โŸจ๐‘Œ, ๐‘โŸฉ ยท ๐‘Š)๐บ)(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘Š)๐น) = (๐พ(โŸจ๐‘‹, ๐‘โŸฉ ยท ๐‘Š)(๐บ(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น))))
5712, 56rspcimdv 3596 . . . . 5 (((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โˆง ๐‘ฆ = ๐‘Œ) โ†’ (โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘“ โˆˆ (๐‘ฅ๐ป๐‘ฆ)โˆ€๐‘” โˆˆ (๐‘ฆ๐ป๐‘ง)((๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ฅ๐ป๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต โˆ€๐‘˜ โˆˆ (๐‘ง๐ป๐‘ค)((๐‘˜(โŸจ๐‘ฆ, ๐‘งโŸฉ ยท ๐‘ค)๐‘”)(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ค)๐‘“) = (๐‘˜(โŸจ๐‘ฅ, ๐‘งโŸฉ ยท ๐‘ค)(๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“))) โ†’ ((๐พ(โŸจ๐‘Œ, ๐‘โŸฉ ยท ๐‘Š)๐บ)(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘Š)๐น) = (๐พ(โŸจ๐‘‹, ๐‘โŸฉ ยท ๐‘Š)(๐บ(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น))))
5810, 57rspcimdv 3596 . . . 4 ((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โ†’ (โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘“ โˆˆ (๐‘ฅ๐ป๐‘ฆ)โˆ€๐‘” โˆˆ (๐‘ฆ๐ป๐‘ง)((๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ฅ๐ป๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต โˆ€๐‘˜ โˆˆ (๐‘ง๐ป๐‘ค)((๐‘˜(โŸจ๐‘ฆ, ๐‘งโŸฉ ยท ๐‘ค)๐‘”)(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ค)๐‘“) = (๐‘˜(โŸจ๐‘ฅ, ๐‘งโŸฉ ยท ๐‘ค)(๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“))) โ†’ ((๐พ(โŸจ๐‘Œ, ๐‘โŸฉ ยท ๐‘Š)๐บ)(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘Š)๐น) = (๐พ(โŸจ๐‘‹, ๐‘โŸฉ ยท ๐‘Š)(๐บ(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น))))
5958adantld 490 . . 3 ((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โ†’ ((โˆƒ๐‘” โˆˆ (๐‘ฅ๐ป๐‘ฅ)โˆ€๐‘ฆ โˆˆ ๐ต (โˆ€๐‘“ โˆˆ (๐‘ฆ๐ป๐‘ฅ)(๐‘”(โŸจ๐‘ฆ, ๐‘ฅโŸฉ ยท ๐‘ฅ)๐‘“) = ๐‘“ โˆง โˆ€๐‘“ โˆˆ (๐‘ฅ๐ป๐‘ฆ)(๐‘“(โŸจ๐‘ฅ, ๐‘ฅโŸฉ ยท ๐‘ฆ)๐‘”) = ๐‘“) โˆง โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘“ โˆˆ (๐‘ฅ๐ป๐‘ฆ)โˆ€๐‘” โˆˆ (๐‘ฆ๐ป๐‘ง)((๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ฅ๐ป๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต โˆ€๐‘˜ โˆˆ (๐‘ง๐ป๐‘ค)((๐‘˜(โŸจ๐‘ฆ, ๐‘งโŸฉ ยท ๐‘ค)๐‘”)(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ค)๐‘“) = (๐‘˜(โŸจ๐‘ฅ, ๐‘งโŸฉ ยท ๐‘ค)(๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“)))) โ†’ ((๐พ(โŸจ๐‘Œ, ๐‘โŸฉ ยท ๐‘Š)๐บ)(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘Š)๐น) = (๐พ(โŸจ๐‘‹, ๐‘โŸฉ ยท ๐‘Š)(๐บ(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น))))
608, 59rspcimdv 3596 . 2 (๐œ‘ โ†’ (โˆ€๐‘ฅ โˆˆ ๐ต (โˆƒ๐‘” โˆˆ (๐‘ฅ๐ป๐‘ฅ)โˆ€๐‘ฆ โˆˆ ๐ต (โˆ€๐‘“ โˆˆ (๐‘ฆ๐ป๐‘ฅ)(๐‘”(โŸจ๐‘ฆ, ๐‘ฅโŸฉ ยท ๐‘ฅ)๐‘“) = ๐‘“ โˆง โˆ€๐‘“ โˆˆ (๐‘ฅ๐ป๐‘ฆ)(๐‘“(โŸจ๐‘ฅ, ๐‘ฅโŸฉ ยท ๐‘ฆ)๐‘”) = ๐‘“) โˆง โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘“ โˆˆ (๐‘ฅ๐ป๐‘ฆ)โˆ€๐‘” โˆˆ (๐‘ฆ๐ป๐‘ง)((๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ฅ๐ป๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต โˆ€๐‘˜ โˆˆ (๐‘ง๐ป๐‘ค)((๐‘˜(โŸจ๐‘ฆ, ๐‘งโŸฉ ยท ๐‘ค)๐‘”)(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ค)๐‘“) = (๐‘˜(โŸจ๐‘ฅ, ๐‘งโŸฉ ยท ๐‘ค)(๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“)))) โ†’ ((๐พ(โŸจ๐‘Œ, ๐‘โŸฉ ยท ๐‘Š)๐บ)(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘Š)๐น) = (๐พ(โŸจ๐‘‹, ๐‘โŸฉ ยท ๐‘Š)(๐บ(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น))))
617, 60mpd 15 1 (๐œ‘ โ†’ ((๐พ(โŸจ๐‘Œ, ๐‘โŸฉ ยท ๐‘Š)๐บ)(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘Š)๐น) = (๐พ(โŸจ๐‘‹, ๐‘โŸฉ ยท ๐‘Š)(๐บ(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 395   = wceq 1533   โˆˆ wcel 2098  โˆ€wral 3055  โˆƒwrex 3064  โŸจcop 4629  โ€˜cfv 6536  (class class class)co 7404  Basecbs 17151  Hom chom 17215  compcco 17216  Catccat 17615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697  ax-nul 5299
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-ne 2935  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-sbc 3773  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-iota 6488  df-fv 6544  df-ov 7407  df-cat 17619
This theorem is referenced by:  oppccatid  17672  sectcan  17709  sectco  17710  sectmon  17736  monsect  17737  rcaninv  17748  subccatid  17803  fuccocl  17927  fucass  17931  invfuc  17937  arwass  18034  xpccatid  18150  evlfcllem  18184  hofcllem  18221  bj-endmnd  36706  endmndlem  47890
  Copyright terms: Public domain W3C validator