Step | Hyp | Ref
| Expression |
1 | | invisoinv.b |
. . . 4
β’ π΅ = (BaseβπΆ) |
2 | | invisoinv.i |
. . . 4
β’ πΌ = (IsoβπΆ) |
3 | | invisoinv.n |
. . . 4
β’ π = (InvβπΆ) |
4 | | invisoinv.c |
. . . 4
β’ (π β πΆ β Cat) |
5 | | invisoinv.x |
. . . 4
β’ (π β π β π΅) |
6 | | invisoinv.y |
. . . 4
β’ (π β π β π΅) |
7 | | invisoinv.f |
. . . 4
β’ (π β πΉ β (ππΌπ)) |
8 | 1, 2, 3, 4, 5, 6, 7 | invisoinvr 17738 |
. . 3
β’ (π β πΉ(πππ)((πππ)βπΉ)) |
9 | | eqid 2733 |
. . . . 5
β’
(SectβπΆ) =
(SectβπΆ) |
10 | 1, 3, 4, 5, 6, 9 | isinv 17707 |
. . . 4
β’ (π β (πΉ(πππ)((πππ)βπΉ) β (πΉ(π(SectβπΆ)π)((πππ)βπΉ) β§ ((πππ)βπΉ)(π(SectβπΆ)π)πΉ))) |
11 | | simpl 484 |
. . . 4
β’ ((πΉ(π(SectβπΆ)π)((πππ)βπΉ) β§ ((πππ)βπΉ)(π(SectβπΆ)π)πΉ) β πΉ(π(SectβπΆ)π)((πππ)βπΉ)) |
12 | 10, 11 | syl6bi 253 |
. . 3
β’ (π β (πΉ(πππ)((πππ)βπΉ) β πΉ(π(SectβπΆ)π)((πππ)βπΉ))) |
13 | 8, 12 | mpd 15 |
. 2
β’ (π β πΉ(π(SectβπΆ)π)((πππ)βπΉ)) |
14 | | eqid 2733 |
. . . 4
β’ (Hom
βπΆ) = (Hom
βπΆ) |
15 | | eqid 2733 |
. . . 4
β’
(compβπΆ) =
(compβπΆ) |
16 | | invcoisoid.1 |
. . . 4
β’ 1 =
(IdβπΆ) |
17 | 1, 14, 2, 4, 5, 6 | isohom 17723 |
. . . . 5
β’ (π β (ππΌπ) β (π(Hom βπΆ)π)) |
18 | 17, 7 | sseldd 3984 |
. . . 4
β’ (π β πΉ β (π(Hom βπΆ)π)) |
19 | 1, 14, 2, 4, 6, 5 | isohom 17723 |
. . . . 5
β’ (π β (ππΌπ) β (π(Hom βπΆ)π)) |
20 | 1, 3, 4, 5, 6, 2 | invf 17715 |
. . . . . 6
β’ (π β (πππ):(ππΌπ)βΆ(ππΌπ)) |
21 | 20, 7 | ffvelcdmd 7088 |
. . . . 5
β’ (π β ((πππ)βπΉ) β (ππΌπ)) |
22 | 19, 21 | sseldd 3984 |
. . . 4
β’ (π β ((πππ)βπΉ) β (π(Hom βπΆ)π)) |
23 | 1, 14, 15, 16, 9, 4, 5, 6, 18,
22 | issect2 17701 |
. . 3
β’ (π β (πΉ(π(SectβπΆ)π)((πππ)βπΉ) β (((πππ)βπΉ)(β¨π, πβ©(compβπΆ)π)πΉ) = ( 1 βπ))) |
24 | | invcoisoid.o |
. . . . . . 7
β’ β¬ =
(β¨π, πβ©(compβπΆ)π) |
25 | 24 | a1i 11 |
. . . . . 6
β’ (π β β¬ = (β¨π, πβ©(compβπΆ)π)) |
26 | 25 | eqcomd 2739 |
. . . . 5
β’ (π β (β¨π, πβ©(compβπΆ)π) = β¬ ) |
27 | 26 | oveqd 7426 |
. . . 4
β’ (π β (((πππ)βπΉ)(β¨π, πβ©(compβπΆ)π)πΉ) = (((πππ)βπΉ) β¬ πΉ)) |
28 | 27 | eqeq1d 2735 |
. . 3
β’ (π β ((((πππ)βπΉ)(β¨π, πβ©(compβπΆ)π)πΉ) = ( 1 βπ) β (((πππ)βπΉ) β¬ πΉ) = ( 1 βπ))) |
29 | 23, 28 | bitrd 279 |
. 2
β’ (π β (πΉ(π(SectβπΆ)π)((πππ)βπΉ) β (((πππ)βπΉ) β¬ πΉ) = ( 1 βπ))) |
30 | 13, 29 | mpbid 231 |
1
β’ (π β (((πππ)βπΉ) β¬ πΉ) = ( 1 βπ)) |