Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . 5
โข
(Baseโ๐ถ) =
(Baseโ๐ถ) |
2 | | eqid 2733 |
. . . . 5
โข (Hom
โ๐ถ) = (Hom
โ๐ถ) |
3 | | eqid 2733 |
. . . . 5
โข
(compโ๐ถ) =
(compโ๐ถ) |
4 | | arwlid.f |
. . . . . 6
โข (๐ โ ๐น โ (๐๐ป๐)) |
5 | | arwlid.h |
. . . . . . 7
โข ๐ป =
(Homaโ๐ถ) |
6 | 5 | homarcl 17978 |
. . . . . 6
โข (๐น โ (๐๐ป๐) โ ๐ถ โ Cat) |
7 | 4, 6 | syl 17 |
. . . . 5
โข (๐ โ ๐ถ โ Cat) |
8 | 5, 1 | homarcl2 17985 |
. . . . . . 7
โข (๐น โ (๐๐ป๐) โ (๐ โ (Baseโ๐ถ) โง ๐ โ (Baseโ๐ถ))) |
9 | 4, 8 | syl 17 |
. . . . . 6
โข (๐ โ (๐ โ (Baseโ๐ถ) โง ๐ โ (Baseโ๐ถ))) |
10 | 9 | simpld 496 |
. . . . 5
โข (๐ โ ๐ โ (Baseโ๐ถ)) |
11 | 9 | simprd 497 |
. . . . 5
โข (๐ โ ๐ โ (Baseโ๐ถ)) |
12 | | arwass.k |
. . . . . . 7
โข (๐ โ ๐พ โ (๐๐ป๐)) |
13 | 5, 1 | homarcl2 17985 |
. . . . . . 7
โข (๐พ โ (๐๐ป๐) โ (๐ โ (Baseโ๐ถ) โง ๐ โ (Baseโ๐ถ))) |
14 | 12, 13 | syl 17 |
. . . . . 6
โข (๐ โ (๐ โ (Baseโ๐ถ) โง ๐ โ (Baseโ๐ถ))) |
15 | 14 | simpld 496 |
. . . . 5
โข (๐ โ ๐ โ (Baseโ๐ถ)) |
16 | 5, 2 | homahom 17989 |
. . . . . 6
โข (๐น โ (๐๐ป๐) โ (2nd โ๐น) โ (๐(Hom โ๐ถ)๐)) |
17 | 4, 16 | syl 17 |
. . . . 5
โข (๐ โ (2nd
โ๐น) โ (๐(Hom โ๐ถ)๐)) |
18 | | arwass.g |
. . . . . 6
โข (๐ โ ๐บ โ (๐๐ป๐)) |
19 | 5, 2 | homahom 17989 |
. . . . . 6
โข (๐บ โ (๐๐ป๐) โ (2nd โ๐บ) โ (๐(Hom โ๐ถ)๐)) |
20 | 18, 19 | syl 17 |
. . . . 5
โข (๐ โ (2nd
โ๐บ) โ (๐(Hom โ๐ถ)๐)) |
21 | 14 | simprd 497 |
. . . . 5
โข (๐ โ ๐ โ (Baseโ๐ถ)) |
22 | 5, 2 | homahom 17989 |
. . . . . 6
โข (๐พ โ (๐๐ป๐) โ (2nd โ๐พ) โ (๐(Hom โ๐ถ)๐)) |
23 | 12, 22 | syl 17 |
. . . . 5
โข (๐ โ (2nd
โ๐พ) โ (๐(Hom โ๐ถ)๐)) |
24 | 1, 2, 3, 7, 10, 11, 15, 17, 20, 21, 23 | catass 17630 |
. . . 4
โข (๐ โ (((2nd
โ๐พ)(โจ๐, ๐โฉ(compโ๐ถ)๐)(2nd โ๐บ))(โจ๐, ๐โฉ(compโ๐ถ)๐)(2nd โ๐น)) = ((2nd โ๐พ)(โจ๐, ๐โฉ(compโ๐ถ)๐)((2nd โ๐บ)(โจ๐, ๐โฉ(compโ๐ถ)๐)(2nd โ๐น)))) |
25 | | arwlid.o |
. . . . . 6
โข ยท =
(compaโ๐ถ) |
26 | 25, 5, 18, 12, 3 | coa2 18019 |
. . . . 5
โข (๐ โ (2nd
โ(๐พ ยท ๐บ)) = ((2nd
โ๐พ)(โจ๐, ๐โฉ(compโ๐ถ)๐)(2nd โ๐บ))) |
27 | 26 | oveq1d 7424 |
. . . 4
โข (๐ โ ((2nd
โ(๐พ ยท ๐บ))(โจ๐, ๐โฉ(compโ๐ถ)๐)(2nd โ๐น)) = (((2nd โ๐พ)(โจ๐, ๐โฉ(compโ๐ถ)๐)(2nd โ๐บ))(โจ๐, ๐โฉ(compโ๐ถ)๐)(2nd โ๐น))) |
28 | 25, 5, 4, 18, 3 | coa2 18019 |
. . . . 5
โข (๐ โ (2nd
โ(๐บ ยท ๐น)) = ((2nd
โ๐บ)(โจ๐, ๐โฉ(compโ๐ถ)๐)(2nd โ๐น))) |
29 | 28 | oveq2d 7425 |
. . . 4
โข (๐ โ ((2nd
โ๐พ)(โจ๐, ๐โฉ(compโ๐ถ)๐)(2nd โ(๐บ ยท ๐น))) = ((2nd โ๐พ)(โจ๐, ๐โฉ(compโ๐ถ)๐)((2nd โ๐บ)(โจ๐, ๐โฉ(compโ๐ถ)๐)(2nd โ๐น)))) |
30 | 24, 27, 29 | 3eqtr4d 2783 |
. . 3
โข (๐ โ ((2nd
โ(๐พ ยท ๐บ))(โจ๐, ๐โฉ(compโ๐ถ)๐)(2nd โ๐น)) = ((2nd โ๐พ)(โจ๐, ๐โฉ(compโ๐ถ)๐)(2nd โ(๐บ ยท ๐น)))) |
31 | 30 | oteq3d 4888 |
. 2
โข (๐ โ โจ๐, ๐, ((2nd โ(๐พ ยท ๐บ))(โจ๐, ๐โฉ(compโ๐ถ)๐)(2nd โ๐น))โฉ = โจ๐, ๐, ((2nd โ๐พ)(โจ๐, ๐โฉ(compโ๐ถ)๐)(2nd โ(๐บ ยท ๐น)))โฉ) |
32 | 25, 5, 18, 12 | coahom 18020 |
. . 3
โข (๐ โ (๐พ ยท ๐บ) โ (๐๐ป๐)) |
33 | 25, 5, 4, 32, 3 | coaval 18018 |
. 2
โข (๐ โ ((๐พ ยท ๐บ) ยท ๐น) = โจ๐, ๐, ((2nd โ(๐พ ยท ๐บ))(โจ๐, ๐โฉ(compโ๐ถ)๐)(2nd โ๐น))โฉ) |
34 | 25, 5, 4, 18 | coahom 18020 |
. . 3
โข (๐ โ (๐บ ยท ๐น) โ (๐๐ป๐)) |
35 | 25, 5, 34, 12, 3 | coaval 18018 |
. 2
โข (๐ โ (๐พ ยท (๐บ ยท ๐น)) = โจ๐, ๐, ((2nd โ๐พ)(โจ๐, ๐โฉ(compโ๐ถ)๐)(2nd โ(๐บ ยท ๐น)))โฉ) |
36 | 31, 33, 35 | 3eqtr4d 2783 |
1
โข (๐ โ ((๐พ ยท ๐บ) ยท ๐น) = (๐พ ยท (๐บ ยท ๐น))) |