Step | Hyp | Ref
| Expression |
1 | | functhinc.e |
. . . . 5
โข (๐ โ ๐ธ โ ThinCat) |
2 | 1 | ad2antrr 724 |
. . . 4
โข (((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โ ๐ธ โ ThinCat) |
3 | | functhinc.c |
. . . 4
โข ๐ถ = (Baseโ๐ธ) |
4 | | functhinc.j |
. . . 4
โข ๐ฝ = (Hom โ๐ธ) |
5 | | functhinc.f |
. . . . . 6
โข (๐ โ ๐น:๐ตโถ๐ถ) |
6 | 5 | adantr 481 |
. . . . 5
โข ((๐ โง ๐บ = ๐พ) โ ๐น:๐ตโถ๐ถ) |
7 | 6 | ffvelcdmda 7086 |
. . . 4
โข (((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โ (๐นโ๐) โ ๐ถ) |
8 | | functhinclem4.i |
. . . 4
โข ๐ผ = (Idโ๐ธ) |
9 | | simpr 485 |
. . . . 5
โข (((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
10 | | functhinc.b |
. . . . . 6
โข ๐ต = (Baseโ๐ท) |
11 | | functhinc.h |
. . . . . 6
โข ๐ป = (Hom โ๐ท) |
12 | | functhinclem4.1 |
. . . . . 6
โข 1 =
(Idโ๐ท) |
13 | | functhinc.d |
. . . . . . 7
โข (๐ โ ๐ท โ Cat) |
14 | 13 | ad2antrr 724 |
. . . . . 6
โข (((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โ ๐ท โ Cat) |
15 | 10, 11, 12, 14, 9 | catidcl 17625 |
. . . . 5
โข (((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โ ( 1 โ๐) โ (๐๐ป๐)) |
16 | | simplr 767 |
. . . . . 6
โข (((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โ ๐บ = ๐พ) |
17 | | functhinc.k |
. . . . . . 7
โข ๐พ = (๐ฅ โ ๐ต, ๐ฆ โ ๐ต โฆ ((๐ฅ๐ป๐ฆ) ร ((๐นโ๐ฅ)๐ฝ(๐นโ๐ฆ)))) |
18 | | oveq1 7415 |
. . . . . . . . 9
โข (๐ฅ = ๐ฃ โ (๐ฅ๐ป๐ฆ) = (๐ฃ๐ป๐ฆ)) |
19 | | fveq2 6891 |
. . . . . . . . . 10
โข (๐ฅ = ๐ฃ โ (๐นโ๐ฅ) = (๐นโ๐ฃ)) |
20 | 19 | oveq1d 7423 |
. . . . . . . . 9
โข (๐ฅ = ๐ฃ โ ((๐นโ๐ฅ)๐ฝ(๐นโ๐ฆ)) = ((๐นโ๐ฃ)๐ฝ(๐นโ๐ฆ))) |
21 | 18, 20 | xpeq12d 5707 |
. . . . . . . 8
โข (๐ฅ = ๐ฃ โ ((๐ฅ๐ป๐ฆ) ร ((๐นโ๐ฅ)๐ฝ(๐นโ๐ฆ))) = ((๐ฃ๐ป๐ฆ) ร ((๐นโ๐ฃ)๐ฝ(๐นโ๐ฆ)))) |
22 | | oveq2 7416 |
. . . . . . . . 9
โข (๐ฆ = ๐ข โ (๐ฃ๐ป๐ฆ) = (๐ฃ๐ป๐ข)) |
23 | | fveq2 6891 |
. . . . . . . . . 10
โข (๐ฆ = ๐ข โ (๐นโ๐ฆ) = (๐นโ๐ข)) |
24 | 23 | oveq2d 7424 |
. . . . . . . . 9
โข (๐ฆ = ๐ข โ ((๐นโ๐ฃ)๐ฝ(๐นโ๐ฆ)) = ((๐นโ๐ฃ)๐ฝ(๐นโ๐ข))) |
25 | 22, 24 | xpeq12d 5707 |
. . . . . . . 8
โข (๐ฆ = ๐ข โ ((๐ฃ๐ป๐ฆ) ร ((๐นโ๐ฃ)๐ฝ(๐นโ๐ฆ))) = ((๐ฃ๐ป๐ข) ร ((๐นโ๐ฃ)๐ฝ(๐นโ๐ข)))) |
26 | 21, 25 | cbvmpov 7503 |
. . . . . . 7
โข (๐ฅ โ ๐ต, ๐ฆ โ ๐ต โฆ ((๐ฅ๐ป๐ฆ) ร ((๐นโ๐ฅ)๐ฝ(๐นโ๐ฆ)))) = (๐ฃ โ ๐ต, ๐ข โ ๐ต โฆ ((๐ฃ๐ป๐ข) ร ((๐นโ๐ฃ)๐ฝ(๐นโ๐ข)))) |
27 | 17, 26 | eqtri 2760 |
. . . . . 6
โข ๐พ = (๐ฃ โ ๐ต, ๐ข โ ๐ต โฆ ((๐ฃ๐ป๐ข) ร ((๐นโ๐ฃ)๐ฝ(๐นโ๐ข)))) |
28 | 16, 27 | eqtrdi 2788 |
. . . . 5
โข (((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โ ๐บ = (๐ฃ โ ๐ต, ๐ข โ ๐ต โฆ ((๐ฃ๐ป๐ข) ร ((๐นโ๐ฃ)๐ฝ(๐นโ๐ข))))) |
29 | | functhinc.1 |
. . . . . . 7
โข (๐ โ โ๐ง โ ๐ต โ๐ค โ ๐ต (((๐นโ๐ง)๐ฝ(๐นโ๐ค)) = โ
โ (๐ง๐ป๐ค) = โ
)) |
30 | 29 | ad2antrr 724 |
. . . . . 6
โข (((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โ โ๐ง โ ๐ต โ๐ค โ ๐ต (((๐นโ๐ง)๐ฝ(๐นโ๐ค)) = โ
โ (๐ง๐ป๐ค) = โ
)) |
31 | 9, 9, 30 | functhinclem2 47652 |
. . . . 5
โข (((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โ (((๐นโ๐)๐ฝ(๐นโ๐)) = โ
โ (๐๐ป๐) = โ
)) |
32 | 2, 7, 7, 3, 4 | thincmo 47639 |
. . . . 5
โข (((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โ โ*๐ ๐ โ ((๐นโ๐)๐ฝ(๐นโ๐))) |
33 | 9, 9, 15, 28, 31, 32 | functhinclem3 47653 |
. . . 4
โข (((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โ ((๐๐บ๐)โ( 1 โ๐)) โ ((๐นโ๐)๐ฝ(๐นโ๐))) |
34 | 2, 3, 4, 7, 8, 33 | thincid 47643 |
. . 3
โข (((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โ ((๐๐บ๐)โ( 1 โ๐)) = (๐ผโ(๐นโ๐))) |
35 | 7 | ad2antrr 724 |
. . . . . 6
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ (๐นโ๐) โ ๐ถ) |
36 | 5 | ad4antr 730 |
. . . . . . 7
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ ๐น:๐ตโถ๐ถ) |
37 | | simplrr 776 |
. . . . . . 7
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ ๐ โ ๐ต) |
38 | 36, 37 | ffvelcdmd 7087 |
. . . . . 6
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ (๐นโ๐) โ ๐ถ) |
39 | 9 | ad2antrr 724 |
. . . . . . 7
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ ๐ โ ๐ต) |
40 | | functhinclem4.x |
. . . . . . . 8
โข ยท =
(compโ๐ท) |
41 | 13 | ad4antr 730 |
. . . . . . . 8
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ ๐ท โ Cat) |
42 | | simplrl 775 |
. . . . . . . 8
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ ๐ โ ๐ต) |
43 | | simprl 769 |
. . . . . . . 8
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ ๐ โ (๐๐ป๐)) |
44 | | simprr 771 |
. . . . . . . 8
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ ๐ โ (๐๐ป๐)) |
45 | 10, 11, 40, 41, 39, 42, 37, 43, 44 | catcocl 17628 |
. . . . . . 7
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ (๐(โจ๐, ๐โฉ ยท ๐)๐) โ (๐๐ป๐)) |
46 | 28 | ad2antrr 724 |
. . . . . . 7
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ ๐บ = (๐ฃ โ ๐ต, ๐ข โ ๐ต โฆ ((๐ฃ๐ป๐ข) ร ((๐นโ๐ฃ)๐ฝ(๐นโ๐ข))))) |
47 | 29 | ad4antr 730 |
. . . . . . . 8
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ โ๐ง โ ๐ต โ๐ค โ ๐ต (((๐นโ๐ง)๐ฝ(๐นโ๐ค)) = โ
โ (๐ง๐ป๐ค) = โ
)) |
48 | 39, 37, 47 | functhinclem2 47652 |
. . . . . . 7
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ (((๐นโ๐)๐ฝ(๐นโ๐)) = โ
โ (๐๐ป๐) = โ
)) |
49 | 1 | ad4antr 730 |
. . . . . . . 8
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ ๐ธ โ ThinCat) |
50 | 49, 35, 38, 3, 4 | thincmo 47639 |
. . . . . . 7
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ โ*๐ ๐ โ ((๐นโ๐)๐ฝ(๐นโ๐))) |
51 | 39, 37, 45, 46, 48, 50 | functhinclem3 47653 |
. . . . . 6
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ ((๐๐บ๐)โ(๐(โจ๐, ๐โฉ ยท ๐)๐)) โ ((๐นโ๐)๐ฝ(๐นโ๐))) |
52 | | functhinclem4.o |
. . . . . . 7
โข ๐ = (compโ๐ธ) |
53 | 2 | thinccd 47635 |
. . . . . . . 8
โข (((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โ ๐ธ โ Cat) |
54 | 53 | ad2antrr 724 |
. . . . . . 7
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ ๐ธ โ Cat) |
55 | 36, 42 | ffvelcdmd 7087 |
. . . . . . 7
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ (๐นโ๐) โ ๐ถ) |
56 | 39, 42, 47 | functhinclem2 47652 |
. . . . . . . 8
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ (((๐นโ๐)๐ฝ(๐นโ๐)) = โ
โ (๐๐ป๐) = โ
)) |
57 | 49, 35, 55, 3, 4 | thincmo 47639 |
. . . . . . . 8
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ โ*๐ ๐ โ ((๐นโ๐)๐ฝ(๐นโ๐))) |
58 | 39, 42, 43, 46, 56, 57 | functhinclem3 47653 |
. . . . . . 7
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ ((๐๐บ๐)โ๐) โ ((๐นโ๐)๐ฝ(๐นโ๐))) |
59 | 42, 37, 47 | functhinclem2 47652 |
. . . . . . . 8
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ (((๐นโ๐)๐ฝ(๐นโ๐)) = โ
โ (๐๐ป๐) = โ
)) |
60 | 49, 55, 38, 3, 4 | thincmo 47639 |
. . . . . . . 8
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ โ*๐ ๐ โ ((๐นโ๐)๐ฝ(๐นโ๐))) |
61 | 42, 37, 44, 46, 59, 60 | functhinclem3 47653 |
. . . . . . 7
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ ((๐๐บ๐)โ๐) โ ((๐นโ๐)๐ฝ(๐นโ๐))) |
62 | 3, 4, 52, 54, 35, 55, 38, 58, 61 | catcocl 17628 |
. . . . . 6
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ (((๐๐บ๐)โ๐)(โจ(๐นโ๐), (๐นโ๐)โฉ๐(๐นโ๐))((๐๐บ๐)โ๐)) โ ((๐นโ๐)๐ฝ(๐นโ๐))) |
63 | 35, 38, 51, 62, 3, 4, 49 | thincmo2 47638 |
. . . . 5
โข
(((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ (๐๐ป๐) โง ๐ โ (๐๐ป๐))) โ ((๐๐บ๐)โ(๐(โจ๐, ๐โฉ ยท ๐)๐)) = (((๐๐บ๐)โ๐)(โจ(๐นโ๐), (๐นโ๐)โฉ๐(๐นโ๐))((๐๐บ๐)โ๐))) |
64 | 63 | ralrimivva 3200 |
. . . 4
โข ((((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ โ๐ โ (๐๐ป๐)โ๐ โ (๐๐ป๐)((๐๐บ๐)โ(๐(โจ๐, ๐โฉ ยท ๐)๐)) = (((๐๐บ๐)โ๐)(โจ(๐นโ๐), (๐นโ๐)โฉ๐(๐นโ๐))((๐๐บ๐)โ๐))) |
65 | 64 | ralrimivva 3200 |
. . 3
โข (((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โ โ๐ โ ๐ต โ๐ โ ๐ต โ๐ โ (๐๐ป๐)โ๐ โ (๐๐ป๐)((๐๐บ๐)โ(๐(โจ๐, ๐โฉ ยท ๐)๐)) = (((๐๐บ๐)โ๐)(โจ(๐นโ๐), (๐นโ๐)โฉ๐(๐นโ๐))((๐๐บ๐)โ๐))) |
66 | 34, 65 | jca 512 |
. 2
โข (((๐ โง ๐บ = ๐พ) โง ๐ โ ๐ต) โ (((๐๐บ๐)โ( 1 โ๐)) = (๐ผโ(๐นโ๐)) โง โ๐ โ ๐ต โ๐ โ ๐ต โ๐ โ (๐๐ป๐)โ๐ โ (๐๐ป๐)((๐๐บ๐)โ(๐(โจ๐, ๐โฉ ยท ๐)๐)) = (((๐๐บ๐)โ๐)(โจ(๐นโ๐), (๐นโ๐)โฉ๐(๐นโ๐))((๐๐บ๐)โ๐)))) |
67 | 66 | ralrimiva 3146 |
1
โข ((๐ โง ๐บ = ๐พ) โ โ๐ โ ๐ต (((๐๐บ๐)โ( 1 โ๐)) = (๐ผโ(๐นโ๐)) โง โ๐ โ ๐ต โ๐ โ ๐ต โ๐ โ (๐๐ป๐)โ๐ โ (๐๐ป๐)((๐๐บ๐)โ(๐(โจ๐, ๐โฉ ยท ๐)๐)) = (((๐๐บ๐)โ๐)(โจ(๐นโ๐), (๐นโ๐)โฉ๐(๐นโ๐))((๐๐บ๐)โ๐)))) |