Step | Hyp | Ref
| Expression |
1 | | fvexd 6854 |
. . 3
โข (๐ = ๐ถ โ (Baseโ๐) โ V) |
2 | | fveq2 6839 |
. . . 4
โข (๐ = ๐ถ โ (Baseโ๐) = (Baseโ๐ถ)) |
3 | | iscat.b |
. . . 4
โข ๐ต = (Baseโ๐ถ) |
4 | 2, 3 | eqtr4di 2795 |
. . 3
โข (๐ = ๐ถ โ (Baseโ๐) = ๐ต) |
5 | | fvexd 6854 |
. . . 4
โข ((๐ = ๐ถ โง ๐ = ๐ต) โ (Hom โ๐) โ V) |
6 | | simpl 483 |
. . . . . 6
โข ((๐ = ๐ถ โง ๐ = ๐ต) โ ๐ = ๐ถ) |
7 | 6 | fveq2d 6843 |
. . . . 5
โข ((๐ = ๐ถ โง ๐ = ๐ต) โ (Hom โ๐) = (Hom โ๐ถ)) |
8 | | iscat.h |
. . . . 5
โข ๐ป = (Hom โ๐ถ) |
9 | 7, 8 | eqtr4di 2795 |
. . . 4
โข ((๐ = ๐ถ โง ๐ = ๐ต) โ (Hom โ๐) = ๐ป) |
10 | | fvexd 6854 |
. . . . 5
โข (((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โ (compโ๐) โ V) |
11 | | simpll 765 |
. . . . . . 7
โข (((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โ ๐ = ๐ถ) |
12 | 11 | fveq2d 6843 |
. . . . . 6
โข (((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โ (compโ๐) = (compโ๐ถ)) |
13 | | iscat.o |
. . . . . 6
โข ยท =
(compโ๐ถ) |
14 | 12, 13 | eqtr4di 2795 |
. . . . 5
โข (((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โ (compโ๐) = ยท ) |
15 | | simpllr 774 |
. . . . . 6
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ ๐ = ๐ต) |
16 | | simplr 767 |
. . . . . . . . 9
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ โ = ๐ป) |
17 | 16 | oveqd 7368 |
. . . . . . . 8
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ (๐ฅโ๐ฅ) = (๐ฅ๐ป๐ฅ)) |
18 | 16 | oveqd 7368 |
. . . . . . . . . . 11
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ (๐ฆโ๐ฅ) = (๐ฆ๐ป๐ฅ)) |
19 | | simpr 485 |
. . . . . . . . . . . . . 14
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ ๐ = ยท ) |
20 | 19 | oveqd 7368 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ
(โจ๐ฆ, ๐ฅโฉ๐๐ฅ) = (โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)) |
21 | 20 | oveqd 7368 |
. . . . . . . . . . . 12
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ (๐(โจ๐ฆ, ๐ฅโฉ๐๐ฅ)๐) = (๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐)) |
22 | 21 | eqeq1d 2739 |
. . . . . . . . . . 11
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ ((๐(โจ๐ฆ, ๐ฅโฉ๐๐ฅ)๐) = ๐ โ (๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐)) |
23 | 18, 22 | raleqbidv 3317 |
. . . . . . . . . 10
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ
(โ๐ โ (๐ฆโ๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ๐๐ฅ)๐) = ๐ โ โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐)) |
24 | 16 | oveqd 7368 |
. . . . . . . . . . 11
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ (๐ฅโ๐ฆ) = (๐ฅ๐ป๐ฆ)) |
25 | 19 | oveqd 7368 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ
(โจ๐ฅ, ๐ฅโฉ๐๐ฆ) = (โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)) |
26 | 25 | oveqd 7368 |
. . . . . . . . . . . 12
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ (๐(โจ๐ฅ, ๐ฅโฉ๐๐ฆ)๐) = (๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐)) |
27 | 26 | eqeq1d 2739 |
. . . . . . . . . . 11
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ ((๐(โจ๐ฅ, ๐ฅโฉ๐๐ฆ)๐) = ๐ โ (๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐)) |
28 | 24, 27 | raleqbidv 3317 |
. . . . . . . . . 10
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ
(โ๐ โ (๐ฅโ๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ๐๐ฆ)๐) = ๐ โ โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐)) |
29 | 23, 28 | anbi12d 631 |
. . . . . . . . 9
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ
((โ๐ โ (๐ฆโ๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ๐๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅโ๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ๐๐ฆ)๐) = ๐) โ (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐))) |
30 | 15, 29 | raleqbidv 3317 |
. . . . . . . 8
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ
(โ๐ฆ โ ๐ (โ๐ โ (๐ฆโ๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ๐๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅโ๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ๐๐ฆ)๐) = ๐) โ โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐))) |
31 | 17, 30 | rexeqbidv 3318 |
. . . . . . 7
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ
(โ๐ โ (๐ฅโ๐ฅ)โ๐ฆ โ ๐ (โ๐ โ (๐ฆโ๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ๐๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅโ๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ๐๐ฆ)๐) = ๐) โ โ๐ โ (๐ฅ๐ป๐ฅ)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐))) |
32 | 16 | oveqd 7368 |
. . . . . . . . . . 11
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ (๐ฆโ๐ง) = (๐ฆ๐ป๐ง)) |
33 | 19 | oveqd 7368 |
. . . . . . . . . . . . . 14
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ
(โจ๐ฅ, ๐ฆโฉ๐๐ง) = (โจ๐ฅ, ๐ฆโฉ ยท ๐ง)) |
34 | 33 | oveqd 7368 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ (๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐) = (๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)) |
35 | 16 | oveqd 7368 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ (๐ฅโ๐ง) = (๐ฅ๐ป๐ง)) |
36 | 34, 35 | eleq12d 2832 |
. . . . . . . . . . . 12
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ ((๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐) โ (๐ฅโ๐ง) โ (๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง))) |
37 | 16 | oveqd 7368 |
. . . . . . . . . . . . . 14
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ (๐งโ๐ค) = (๐ง๐ป๐ค)) |
38 | 19 | oveqd 7368 |
. . . . . . . . . . . . . . . 16
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ
(โจ๐ฅ, ๐ฆโฉ๐๐ค) = (โจ๐ฅ, ๐ฆโฉ ยท ๐ค)) |
39 | 19 | oveqd 7368 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ
(โจ๐ฆ, ๐งโฉ๐๐ค) = (โจ๐ฆ, ๐งโฉ ยท ๐ค)) |
40 | 39 | oveqd 7368 |
. . . . . . . . . . . . . . . 16
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ (๐(โจ๐ฆ, ๐งโฉ๐๐ค)๐) = (๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)) |
41 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ ๐ = ๐) |
42 | 38, 40, 41 | oveq123d 7372 |
. . . . . . . . . . . . . . 15
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ ((๐(โจ๐ฆ, ๐งโฉ๐๐ค)๐)(โจ๐ฅ, ๐ฆโฉ๐๐ค)๐) = ((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐)) |
43 | 19 | oveqd 7368 |
. . . . . . . . . . . . . . . 16
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ
(โจ๐ฅ, ๐งโฉ๐๐ค) = (โจ๐ฅ, ๐งโฉ ยท ๐ค)) |
44 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ ๐ = ๐) |
45 | 43, 44, 34 | oveq123d 7372 |
. . . . . . . . . . . . . . 15
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ (๐(โจ๐ฅ, ๐งโฉ๐๐ค)(๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐)) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐))) |
46 | 42, 45 | eqeq12d 2753 |
. . . . . . . . . . . . . 14
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ (((๐(โจ๐ฆ, ๐งโฉ๐๐ค)๐)(โจ๐ฅ, ๐ฆโฉ๐๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ๐๐ค)(๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐)) โ ((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)))) |
47 | 37, 46 | raleqbidv 3317 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ
(โ๐ โ (๐งโ๐ค)((๐(โจ๐ฆ, ๐งโฉ๐๐ค)๐)(โจ๐ฅ, ๐ฆโฉ๐๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ๐๐ค)(๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐)) โ โ๐ โ (๐ง๐ป๐ค)((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)))) |
48 | 15, 47 | raleqbidv 3317 |
. . . . . . . . . . . 12
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ
(โ๐ค โ ๐ โ๐ โ (๐งโ๐ค)((๐(โจ๐ฆ, ๐งโฉ๐๐ค)๐)(โจ๐ฅ, ๐ฆโฉ๐๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ๐๐ค)(๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐)) โ โ๐ค โ ๐ต โ๐ โ (๐ง๐ป๐ค)((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)))) |
49 | 36, 48 | anbi12d 631 |
. . . . . . . . . . 11
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ (((๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐) โ (๐ฅโ๐ง) โง โ๐ค โ ๐ โ๐ โ (๐งโ๐ค)((๐(โจ๐ฆ, ๐งโฉ๐๐ค)๐)(โจ๐ฅ, ๐ฆโฉ๐๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ๐๐ค)(๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐))) โ ((๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โง โ๐ค โ ๐ต โ๐ โ (๐ง๐ป๐ค)((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐))))) |
50 | 32, 49 | raleqbidv 3317 |
. . . . . . . . . 10
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ
(โ๐ โ (๐ฆโ๐ง)((๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐) โ (๐ฅโ๐ง) โง โ๐ค โ ๐ โ๐ โ (๐งโ๐ค)((๐(โจ๐ฆ, ๐งโฉ๐๐ค)๐)(โจ๐ฅ, ๐ฆโฉ๐๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ๐๐ค)(๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐))) โ โ๐ โ (๐ฆ๐ป๐ง)((๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โง โ๐ค โ ๐ต โ๐ โ (๐ง๐ป๐ค)((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐))))) |
51 | 24, 50 | raleqbidv 3317 |
. . . . . . . . 9
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ
(โ๐ โ (๐ฅโ๐ฆ)โ๐ โ (๐ฆโ๐ง)((๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐) โ (๐ฅโ๐ง) โง โ๐ค โ ๐ โ๐ โ (๐งโ๐ค)((๐(โจ๐ฆ, ๐งโฉ๐๐ค)๐)(โจ๐ฅ, ๐ฆโฉ๐๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ๐๐ค)(๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐))) โ โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)((๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โง โ๐ค โ ๐ต โ๐ โ (๐ง๐ป๐ค)((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐))))) |
52 | 15, 51 | raleqbidv 3317 |
. . . . . . . 8
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ
(โ๐ง โ ๐ โ๐ โ (๐ฅโ๐ฆ)โ๐ โ (๐ฆโ๐ง)((๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐) โ (๐ฅโ๐ง) โง โ๐ค โ ๐ โ๐ โ (๐งโ๐ค)((๐(โจ๐ฆ, ๐งโฉ๐๐ค)๐)(โจ๐ฅ, ๐ฆโฉ๐๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ๐๐ค)(๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐))) โ โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)((๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โง โ๐ค โ ๐ต โ๐ โ (๐ง๐ป๐ค)((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐))))) |
53 | 15, 52 | raleqbidv 3317 |
. . . . . . 7
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ
(โ๐ฆ โ ๐ โ๐ง โ ๐ โ๐ โ (๐ฅโ๐ฆ)โ๐ โ (๐ฆโ๐ง)((๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐) โ (๐ฅโ๐ง) โง โ๐ค โ ๐ โ๐ โ (๐งโ๐ค)((๐(โจ๐ฆ, ๐งโฉ๐๐ค)๐)(โจ๐ฅ, ๐ฆโฉ๐๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ๐๐ค)(๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐))) โ โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)((๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โง โ๐ค โ ๐ต โ๐ โ (๐ง๐ป๐ค)((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐))))) |
54 | 31, 53 | anbi12d 631 |
. . . . . 6
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ
((โ๐ โ (๐ฅโ๐ฅ)โ๐ฆ โ ๐ (โ๐ โ (๐ฆโ๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ๐๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅโ๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ๐๐ฆ)๐) = ๐) โง โ๐ฆ โ ๐ โ๐ง โ ๐ โ๐ โ (๐ฅโ๐ฆ)โ๐ โ (๐ฆโ๐ง)((๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐) โ (๐ฅโ๐ง) โง โ๐ค โ ๐ โ๐ โ (๐งโ๐ค)((๐(โจ๐ฆ, ๐งโฉ๐๐ค)๐)(โจ๐ฅ, ๐ฆโฉ๐๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ๐๐ค)(๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐)))) โ (โ๐ โ (๐ฅ๐ป๐ฅ)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐) โง โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)((๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โง โ๐ค โ ๐ต โ๐ โ (๐ง๐ป๐ค)((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)))))) |
55 | 15, 54 | raleqbidv 3317 |
. . . . 5
โข ((((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โง ๐ = ยท ) โ
(โ๐ฅ โ ๐ (โ๐ โ (๐ฅโ๐ฅ)โ๐ฆ โ ๐ (โ๐ โ (๐ฆโ๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ๐๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅโ๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ๐๐ฆ)๐) = ๐) โง โ๐ฆ โ ๐ โ๐ง โ ๐ โ๐ โ (๐ฅโ๐ฆ)โ๐ โ (๐ฆโ๐ง)((๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐) โ (๐ฅโ๐ง) โง โ๐ค โ ๐ โ๐ โ (๐งโ๐ค)((๐(โจ๐ฆ, ๐งโฉ๐๐ค)๐)(โจ๐ฅ, ๐ฆโฉ๐๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ๐๐ค)(๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐)))) โ โ๐ฅ โ ๐ต (โ๐ โ (๐ฅ๐ป๐ฅ)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐) โง โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)((๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โง โ๐ค โ ๐ต โ๐ โ (๐ง๐ป๐ค)((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)))))) |
56 | 10, 14, 55 | sbcied2 3784 |
. . . 4
โข (((๐ = ๐ถ โง ๐ = ๐ต) โง โ = ๐ป) โ ([(compโ๐) / ๐]โ๐ฅ โ ๐ (โ๐ โ (๐ฅโ๐ฅ)โ๐ฆ โ ๐ (โ๐ โ (๐ฆโ๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ๐๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅโ๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ๐๐ฆ)๐) = ๐) โง โ๐ฆ โ ๐ โ๐ง โ ๐ โ๐ โ (๐ฅโ๐ฆ)โ๐ โ (๐ฆโ๐ง)((๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐) โ (๐ฅโ๐ง) โง โ๐ค โ ๐ โ๐ โ (๐งโ๐ค)((๐(โจ๐ฆ, ๐งโฉ๐๐ค)๐)(โจ๐ฅ, ๐ฆโฉ๐๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ๐๐ค)(๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐)))) โ โ๐ฅ โ ๐ต (โ๐ โ (๐ฅ๐ป๐ฅ)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐) โง โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)((๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โง โ๐ค โ ๐ต โ๐ โ (๐ง๐ป๐ค)((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)))))) |
57 | 5, 9, 56 | sbcied2 3784 |
. . 3
โข ((๐ = ๐ถ โง ๐ = ๐ต) โ ([(Hom โ๐) / โ][(compโ๐) / ๐]โ๐ฅ โ ๐ (โ๐ โ (๐ฅโ๐ฅ)โ๐ฆ โ ๐ (โ๐ โ (๐ฆโ๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ๐๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅโ๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ๐๐ฆ)๐) = ๐) โง โ๐ฆ โ ๐ โ๐ง โ ๐ โ๐ โ (๐ฅโ๐ฆ)โ๐ โ (๐ฆโ๐ง)((๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐) โ (๐ฅโ๐ง) โง โ๐ค โ ๐ โ๐ โ (๐งโ๐ค)((๐(โจ๐ฆ, ๐งโฉ๐๐ค)๐)(โจ๐ฅ, ๐ฆโฉ๐๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ๐๐ค)(๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐)))) โ โ๐ฅ โ ๐ต (โ๐ โ (๐ฅ๐ป๐ฅ)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐) โง โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)((๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โง โ๐ค โ ๐ต โ๐ โ (๐ง๐ป๐ค)((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)))))) |
58 | 1, 4, 57 | sbcied2 3784 |
. 2
โข (๐ = ๐ถ โ ([(Baseโ๐) / ๐][(Hom โ๐) / โ][(compโ๐) / ๐]โ๐ฅ โ ๐ (โ๐ โ (๐ฅโ๐ฅ)โ๐ฆ โ ๐ (โ๐ โ (๐ฆโ๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ๐๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅโ๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ๐๐ฆ)๐) = ๐) โง โ๐ฆ โ ๐ โ๐ง โ ๐ โ๐ โ (๐ฅโ๐ฆ)โ๐ โ (๐ฆโ๐ง)((๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐) โ (๐ฅโ๐ง) โง โ๐ค โ ๐ โ๐ โ (๐งโ๐ค)((๐(โจ๐ฆ, ๐งโฉ๐๐ค)๐)(โจ๐ฅ, ๐ฆโฉ๐๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ๐๐ค)(๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐)))) โ โ๐ฅ โ ๐ต (โ๐ โ (๐ฅ๐ป๐ฅ)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐) โง โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)((๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โง โ๐ค โ ๐ต โ๐ โ (๐ง๐ป๐ค)((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)))))) |
59 | | df-cat 17508 |
. 2
โข Cat =
{๐ โฃ
[(Baseโ๐) /
๐][(Hom
โ๐) / โ][(compโ๐) / ๐]โ๐ฅ โ ๐ (โ๐ โ (๐ฅโ๐ฅ)โ๐ฆ โ ๐ (โ๐ โ (๐ฆโ๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ๐๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅโ๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ๐๐ฆ)๐) = ๐) โง โ๐ฆ โ ๐ โ๐ง โ ๐ โ๐ โ (๐ฅโ๐ฆ)โ๐ โ (๐ฆโ๐ง)((๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐) โ (๐ฅโ๐ง) โง โ๐ค โ ๐ โ๐ โ (๐งโ๐ค)((๐(โจ๐ฆ, ๐งโฉ๐๐ค)๐)(โจ๐ฅ, ๐ฆโฉ๐๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ๐๐ค)(๐(โจ๐ฅ, ๐ฆโฉ๐๐ง)๐))))} |
60 | 58, 59 | elab2g 3630 |
1
โข (๐ถ โ ๐ โ (๐ถ โ Cat โ โ๐ฅ โ ๐ต (โ๐ โ (๐ฅ๐ป๐ฅ)โ๐ฆ โ ๐ต (โ๐ โ (๐ฆ๐ป๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ)๐) = ๐) โง โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)((๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โง โ๐ค โ ๐ต โ๐ โ (๐ง๐ป๐ค)((๐(โจ๐ฆ, ๐งโฉ ยท ๐ค)๐)(โจ๐ฅ, ๐ฆโฉ ยท ๐ค)๐) = (๐(โจ๐ฅ, ๐งโฉ ยท ๐ค)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)))))) |