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 | invisoinvl 17600 |
. . 3
β’ (π β ((πππ)βπΉ)(πππ)πΉ) |
9 | | eqid 2736 |
. . . . 5
β’
(SectβπΆ) =
(SectβπΆ) |
10 | 1, 3, 4, 6, 5, 9 | isinv 17570 |
. . . 4
β’ (π β (((πππ)βπΉ)(πππ)πΉ β (((πππ)βπΉ)(π(SectβπΆ)π)πΉ β§ πΉ(π(SectβπΆ)π)((πππ)βπΉ)))) |
11 | | simpl 483 |
. . . 4
β’ ((((πππ)βπΉ)(π(SectβπΆ)π)πΉ β§ πΉ(π(SectβπΆ)π)((πππ)βπΉ)) β ((πππ)βπΉ)(π(SectβπΆ)π)πΉ) |
12 | 10, 11 | syl6bi 252 |
. . 3
β’ (π β (((πππ)βπΉ)(πππ)πΉ β ((πππ)βπΉ)(π(SectβπΆ)π)πΉ)) |
13 | 8, 12 | mpd 15 |
. 2
β’ (π β ((πππ)βπΉ)(π(SectβπΆ)π)πΉ) |
14 | | eqid 2736 |
. . . 4
β’ (Hom
βπΆ) = (Hom
βπΆ) |
15 | | eqid 2736 |
. . . 4
β’
(compβπΆ) =
(compβπΆ) |
16 | | invcoisoid.1 |
. . . 4
β’ 1 =
(IdβπΆ) |
17 | 1, 14, 2, 4, 6, 5 | isohom 17586 |
. . . . 5
β’ (π β (ππΌπ) β (π(Hom βπΆ)π)) |
18 | 1, 3, 4, 5, 6, 2 | invf 17578 |
. . . . . 6
β’ (π β (πππ):(ππΌπ)βΆ(ππΌπ)) |
19 | 18, 7 | ffvelcdmd 7019 |
. . . . 5
β’ (π β ((πππ)βπΉ) β (ππΌπ)) |
20 | 17, 19 | sseldd 3933 |
. . . 4
β’ (π β ((πππ)βπΉ) β (π(Hom βπΆ)π)) |
21 | 1, 14, 2, 4, 5, 6 | isohom 17586 |
. . . . 5
β’ (π β (ππΌπ) β (π(Hom βπΆ)π)) |
22 | 21, 7 | sseldd 3933 |
. . . 4
β’ (π β πΉ β (π(Hom βπΆ)π)) |
23 | 1, 14, 15, 16, 9, 4, 6, 5, 20,
22 | issect2 17564 |
. . 3
β’ (π β (((πππ)βπΉ)(π(SectβπΆ)π)πΉ β (πΉ(β¨π, πβ©(compβπΆ)π)((πππ)βπΉ)) = ( 1 βπ))) |
24 | | isocoinvid.o |
. . . . . . 7
β’ β¬ =
(β¨π, πβ©(compβπΆ)π) |
25 | 24 | a1i 11 |
. . . . . 6
β’ (π β β¬ = (β¨π, πβ©(compβπΆ)π)) |
26 | 25 | eqcomd 2742 |
. . . . 5
β’ (π β (β¨π, πβ©(compβπΆ)π) = β¬ ) |
27 | 26 | oveqd 7355 |
. . . 4
β’ (π β (πΉ(β¨π, πβ©(compβπΆ)π)((πππ)βπΉ)) = (πΉ β¬ ((πππ)βπΉ))) |
28 | 27 | eqeq1d 2738 |
. . 3
β’ (π β ((πΉ(β¨π, πβ©(compβπΆ)π)((πππ)βπΉ)) = ( 1 βπ) β (πΉ β¬ ((πππ)βπΉ)) = ( 1 βπ))) |
29 | 23, 28 | bitrd 278 |
. 2
β’ (π β (((πππ)βπΉ)(π(SectβπΆ)π)πΉ β (πΉ β¬ ((πππ)βπΉ)) = ( 1 βπ))) |
30 | 13, 29 | mpbid 231 |
1
β’ (π β (πΉ β¬ ((πππ)βπΉ)) = ( 1 βπ)) |