Step | Hyp | Ref
| Expression |
1 | | invfval.b |
. . 3
β’ π΅ = (BaseβπΆ) |
2 | | invco.o |
. . 3
β’ Β· =
(compβπΆ) |
3 | | eqid 2738 |
. . 3
β’
(SectβπΆ) =
(SectβπΆ) |
4 | | invfval.c |
. . 3
β’ (π β πΆ β Cat) |
5 | | invfval.x |
. . 3
β’ (π β π β π΅) |
6 | | invfval.y |
. . 3
β’ (π β π β π΅) |
7 | | invco.z |
. . 3
β’ (π β π β π΅) |
8 | | invinv.f |
. . . . . . 7
β’ (π β πΉ β (ππΌπ)) |
9 | | invfval.n |
. . . . . . . 8
β’ π = (InvβπΆ) |
10 | | isoval.n |
. . . . . . . 8
β’ πΌ = (IsoβπΆ) |
11 | 1, 9, 4, 5, 6, 10 | isoval 17583 |
. . . . . . 7
β’ (π β (ππΌπ) = dom (πππ)) |
12 | 8, 11 | eleqtrd 2841 |
. . . . . 6
β’ (π β πΉ β dom (πππ)) |
13 | 1, 9, 4, 5, 6 | invfun 17582 |
. . . . . . 7
β’ (π β Fun (πππ)) |
14 | | funfvbrb 6997 |
. . . . . . 7
β’ (Fun
(πππ) β (πΉ β dom (πππ) β πΉ(πππ)((πππ)βπΉ))) |
15 | 13, 14 | syl 17 |
. . . . . 6
β’ (π β (πΉ β dom (πππ) β πΉ(πππ)((πππ)βπΉ))) |
16 | 12, 15 | mpbid 231 |
. . . . 5
β’ (π β πΉ(πππ)((πππ)βπΉ)) |
17 | 1, 9, 4, 5, 6, 3 | isinv 17578 |
. . . . 5
β’ (π β (πΉ(πππ)((πππ)βπΉ) β (πΉ(π(SectβπΆ)π)((πππ)βπΉ) β§ ((πππ)βπΉ)(π(SectβπΆ)π)πΉ))) |
18 | 16, 17 | mpbid 231 |
. . . 4
β’ (π β (πΉ(π(SectβπΆ)π)((πππ)βπΉ) β§ ((πππ)βπΉ)(π(SectβπΆ)π)πΉ)) |
19 | 18 | simpld 496 |
. . 3
β’ (π β πΉ(π(SectβπΆ)π)((πππ)βπΉ)) |
20 | | invco.f |
. . . . . . 7
β’ (π β πΊ β (ππΌπ)) |
21 | 1, 9, 4, 6, 7, 10 | isoval 17583 |
. . . . . . 7
β’ (π β (ππΌπ) = dom (πππ)) |
22 | 20, 21 | eleqtrd 2841 |
. . . . . 6
β’ (π β πΊ β dom (πππ)) |
23 | 1, 9, 4, 6, 7 | invfun 17582 |
. . . . . . 7
β’ (π β Fun (πππ)) |
24 | | funfvbrb 6997 |
. . . . . . 7
β’ (Fun
(πππ) β (πΊ β dom (πππ) β πΊ(πππ)((πππ)βπΊ))) |
25 | 23, 24 | syl 17 |
. . . . . 6
β’ (π β (πΊ β dom (πππ) β πΊ(πππ)((πππ)βπΊ))) |
26 | 22, 25 | mpbid 231 |
. . . . 5
β’ (π β πΊ(πππ)((πππ)βπΊ)) |
27 | 1, 9, 4, 6, 7, 3 | isinv 17578 |
. . . . 5
β’ (π β (πΊ(πππ)((πππ)βπΊ) β (πΊ(π(SectβπΆ)π)((πππ)βπΊ) β§ ((πππ)βπΊ)(π(SectβπΆ)π)πΊ))) |
28 | 26, 27 | mpbid 231 |
. . . 4
β’ (π β (πΊ(π(SectβπΆ)π)((πππ)βπΊ) β§ ((πππ)βπΊ)(π(SectβπΆ)π)πΊ)) |
29 | 28 | simpld 496 |
. . 3
β’ (π β πΊ(π(SectβπΆ)π)((πππ)βπΊ)) |
30 | 1, 2, 3, 4, 5, 6, 7, 19, 29 | sectco 17574 |
. 2
β’ (π β (πΊ(β¨π, πβ© Β· π)πΉ)(π(SectβπΆ)π)(((πππ)βπΉ)(β¨π, πβ© Β· π)((πππ)βπΊ))) |
31 | 28 | simprd 497 |
. . 3
β’ (π β ((πππ)βπΊ)(π(SectβπΆ)π)πΊ) |
32 | 18 | simprd 497 |
. . 3
β’ (π β ((πππ)βπΉ)(π(SectβπΆ)π)πΉ) |
33 | 1, 2, 3, 4, 7, 6, 5, 31, 32 | sectco 17574 |
. 2
β’ (π β (((πππ)βπΉ)(β¨π, πβ© Β· π)((πππ)βπΊ))(π(SectβπΆ)π)(πΊ(β¨π, πβ© Β· π)πΉ)) |
34 | 1, 9, 4, 5, 7, 3 | isinv 17578 |
. 2
β’ (π β ((πΊ(β¨π, πβ© Β· π)πΉ)(πππ)(((πππ)βπΉ)(β¨π, πβ© Β· π)((πππ)βπΊ)) β ((πΊ(β¨π, πβ© Β· π)πΉ)(π(SectβπΆ)π)(((πππ)βπΉ)(β¨π, πβ© Β· π)((πππ)βπΊ)) β§ (((πππ)βπΉ)(β¨π, πβ© Β· π)((πππ)βπΊ))(π(SectβπΆ)π)(πΊ(β¨π, πβ© Β· π)πΉ)))) |
35 | 30, 33, 34 | mpbir2and 712 |
1
β’ (π β (πΊ(β¨π, πβ© Β· π)πΉ)(πππ)(((πππ)βπΉ)(β¨π, πβ© Β· π)((πππ)βπΊ))) |