Step | Hyp | Ref
| Expression |
1 | | issect.s |
. 2
โข ๐ = (Sectโ๐ถ) |
2 | | issect.c |
. . 3
โข (๐ โ ๐ถ โ Cat) |
3 | | fveq2 6839 |
. . . . . 6
โข (๐ = ๐ถ โ (Baseโ๐) = (Baseโ๐ถ)) |
4 | | issect.b |
. . . . . 6
โข ๐ต = (Baseโ๐ถ) |
5 | 3, 4 | eqtr4di 2795 |
. . . . 5
โข (๐ = ๐ถ โ (Baseโ๐) = ๐ต) |
6 | | fvexd 6854 |
. . . . . . 7
โข (๐ = ๐ถ โ (Hom โ๐) โ V) |
7 | | fveq2 6839 |
. . . . . . . 8
โข (๐ = ๐ถ โ (Hom โ๐) = (Hom โ๐ถ)) |
8 | | issect.h |
. . . . . . . 8
โข ๐ป = (Hom โ๐ถ) |
9 | 7, 8 | eqtr4di 2795 |
. . . . . . 7
โข (๐ = ๐ถ โ (Hom โ๐) = ๐ป) |
10 | | simpr 485 |
. . . . . . . . . . 11
โข ((๐ = ๐ถ โง โ = ๐ป) โ โ = ๐ป) |
11 | 10 | oveqd 7368 |
. . . . . . . . . 10
โข ((๐ = ๐ถ โง โ = ๐ป) โ (๐ฅโ๐ฆ) = (๐ฅ๐ป๐ฆ)) |
12 | 11 | eleq2d 2823 |
. . . . . . . . 9
โข ((๐ = ๐ถ โง โ = ๐ป) โ (๐ โ (๐ฅโ๐ฆ) โ ๐ โ (๐ฅ๐ป๐ฆ))) |
13 | 10 | oveqd 7368 |
. . . . . . . . . 10
โข ((๐ = ๐ถ โง โ = ๐ป) โ (๐ฆโ๐ฅ) = (๐ฆ๐ป๐ฅ)) |
14 | 13 | eleq2d 2823 |
. . . . . . . . 9
โข ((๐ = ๐ถ โง โ = ๐ป) โ (๐ โ (๐ฆโ๐ฅ) โ ๐ โ (๐ฆ๐ป๐ฅ))) |
15 | 12, 14 | anbi12d 631 |
. . . . . . . 8
โข ((๐ = ๐ถ โง โ = ๐ป) โ ((๐ โ (๐ฅโ๐ฆ) โง ๐ โ (๐ฆโ๐ฅ)) โ (๐ โ (๐ฅ๐ป๐ฆ) โง ๐ โ (๐ฆ๐ป๐ฅ)))) |
16 | | simpl 483 |
. . . . . . . . . . . . 13
โข ((๐ = ๐ถ โง โ = ๐ป) โ ๐ = ๐ถ) |
17 | 16 | fveq2d 6843 |
. . . . . . . . . . . 12
โข ((๐ = ๐ถ โง โ = ๐ป) โ (compโ๐) = (compโ๐ถ)) |
18 | | issect.o |
. . . . . . . . . . . 12
โข ยท =
(compโ๐ถ) |
19 | 17, 18 | eqtr4di 2795 |
. . . . . . . . . . 11
โข ((๐ = ๐ถ โง โ = ๐ป) โ (compโ๐) = ยท ) |
20 | 19 | oveqd 7368 |
. . . . . . . . . 10
โข ((๐ = ๐ถ โง โ = ๐ป) โ (โจ๐ฅ, ๐ฆโฉ(compโ๐)๐ฅ) = (โจ๐ฅ, ๐ฆโฉ ยท ๐ฅ)) |
21 | 20 | oveqd 7368 |
. . . . . . . . 9
โข ((๐ = ๐ถ โง โ = ๐ป) โ (๐(โจ๐ฅ, ๐ฆโฉ(compโ๐)๐ฅ)๐) = (๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ฅ)๐)) |
22 | 16 | fveq2d 6843 |
. . . . . . . . . . 11
โข ((๐ = ๐ถ โง โ = ๐ป) โ (Idโ๐) = (Idโ๐ถ)) |
23 | | issect.i |
. . . . . . . . . . 11
โข 1 =
(Idโ๐ถ) |
24 | 22, 23 | eqtr4di 2795 |
. . . . . . . . . 10
โข ((๐ = ๐ถ โง โ = ๐ป) โ (Idโ๐) = 1 ) |
25 | 24 | fveq1d 6841 |
. . . . . . . . 9
โข ((๐ = ๐ถ โง โ = ๐ป) โ ((Idโ๐)โ๐ฅ) = ( 1 โ๐ฅ)) |
26 | 21, 25 | eqeq12d 2753 |
. . . . . . . 8
โข ((๐ = ๐ถ โง โ = ๐ป) โ ((๐(โจ๐ฅ, ๐ฆโฉ(compโ๐)๐ฅ)๐) = ((Idโ๐)โ๐ฅ) โ (๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ฅ)๐) = ( 1 โ๐ฅ))) |
27 | 15, 26 | anbi12d 631 |
. . . . . . 7
โข ((๐ = ๐ถ โง โ = ๐ป) โ (((๐ โ (๐ฅโ๐ฆ) โง ๐ โ (๐ฆโ๐ฅ)) โง (๐(โจ๐ฅ, ๐ฆโฉ(compโ๐)๐ฅ)๐) = ((Idโ๐)โ๐ฅ)) โ ((๐ โ (๐ฅ๐ป๐ฆ) โง ๐ โ (๐ฆ๐ป๐ฅ)) โง (๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ฅ)๐) = ( 1 โ๐ฅ)))) |
28 | 6, 9, 27 | sbcied2 3784 |
. . . . . 6
โข (๐ = ๐ถ โ ([(Hom โ๐) / โ]((๐ โ (๐ฅโ๐ฆ) โง ๐ โ (๐ฆโ๐ฅ)) โง (๐(โจ๐ฅ, ๐ฆโฉ(compโ๐)๐ฅ)๐) = ((Idโ๐)โ๐ฅ)) โ ((๐ โ (๐ฅ๐ป๐ฆ) โง ๐ โ (๐ฆ๐ป๐ฅ)) โง (๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ฅ)๐) = ( 1 โ๐ฅ)))) |
29 | 28 | opabbidv 5169 |
. . . . 5
โข (๐ = ๐ถ โ {โจ๐, ๐โฉ โฃ [(Hom โ๐) / โ]((๐ โ (๐ฅโ๐ฆ) โง ๐ โ (๐ฆโ๐ฅ)) โง (๐(โจ๐ฅ, ๐ฆโฉ(compโ๐)๐ฅ)๐) = ((Idโ๐)โ๐ฅ))} = {โจ๐, ๐โฉ โฃ ((๐ โ (๐ฅ๐ป๐ฆ) โง ๐ โ (๐ฆ๐ป๐ฅ)) โง (๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ฅ)๐) = ( 1 โ๐ฅ))}) |
30 | 5, 5, 29 | mpoeq123dv 7426 |
. . . 4
โข (๐ = ๐ถ โ (๐ฅ โ (Baseโ๐), ๐ฆ โ (Baseโ๐) โฆ {โจ๐, ๐โฉ โฃ [(Hom โ๐) / โ]((๐ โ (๐ฅโ๐ฆ) โง ๐ โ (๐ฆโ๐ฅ)) โง (๐(โจ๐ฅ, ๐ฆโฉ(compโ๐)๐ฅ)๐) = ((Idโ๐)โ๐ฅ))}) = (๐ฅ โ ๐ต, ๐ฆ โ ๐ต โฆ {โจ๐, ๐โฉ โฃ ((๐ โ (๐ฅ๐ป๐ฆ) โง ๐ โ (๐ฆ๐ป๐ฅ)) โง (๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ฅ)๐) = ( 1 โ๐ฅ))})) |
31 | | df-sect 17590 |
. . . 4
โข Sect =
(๐ โ Cat โฆ
(๐ฅ โ (Baseโ๐), ๐ฆ โ (Baseโ๐) โฆ {โจ๐, ๐โฉ โฃ [(Hom โ๐) / โ]((๐ โ (๐ฅโ๐ฆ) โง ๐ โ (๐ฆโ๐ฅ)) โง (๐(โจ๐ฅ, ๐ฆโฉ(compโ๐)๐ฅ)๐) = ((Idโ๐)โ๐ฅ))})) |
32 | 4 | fvexi 6853 |
. . . . 5
โข ๐ต โ V |
33 | 32, 32 | mpoex 8004 |
. . . 4
โข (๐ฅ โ ๐ต, ๐ฆ โ ๐ต โฆ {โจ๐, ๐โฉ โฃ ((๐ โ (๐ฅ๐ป๐ฆ) โง ๐ โ (๐ฆ๐ป๐ฅ)) โง (๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ฅ)๐) = ( 1 โ๐ฅ))}) โ V |
34 | 30, 31, 33 | fvmpt 6945 |
. . 3
โข (๐ถ โ Cat โ
(Sectโ๐ถ) = (๐ฅ โ ๐ต, ๐ฆ โ ๐ต โฆ {โจ๐, ๐โฉ โฃ ((๐ โ (๐ฅ๐ป๐ฆ) โง ๐ โ (๐ฆ๐ป๐ฅ)) โง (๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ฅ)๐) = ( 1 โ๐ฅ))})) |
35 | 2, 34 | syl 17 |
. 2
โข (๐ โ (Sectโ๐ถ) = (๐ฅ โ ๐ต, ๐ฆ โ ๐ต โฆ {โจ๐, ๐โฉ โฃ ((๐ โ (๐ฅ๐ป๐ฆ) โง ๐ โ (๐ฆ๐ป๐ฅ)) โง (๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ฅ)๐) = ( 1 โ๐ฅ))})) |
36 | 1, 35 | eqtrid 2789 |
1
โข (๐ โ ๐ = (๐ฅ โ ๐ต, ๐ฆ โ ๐ต โฆ {โจ๐, ๐โฉ โฃ ((๐ โ (๐ฅ๐ป๐ฆ) โง ๐ โ (๐ฆ๐ป๐ฅ)) โง (๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ฅ)๐) = ( 1 โ๐ฅ))})) |