Step | Hyp | Ref
| Expression |
1 | | fthsect.b |
. . . 4
β’ π΅ = (BaseβπΆ) |
2 | | fthsect.h |
. . . 4
β’ π» = (Hom βπΆ) |
3 | | fthsect.f |
. . . 4
β’ (π β πΉ(πΆ Faith π·)πΊ) |
4 | | fthsect.x |
. . . 4
β’ (π β π β π΅) |
5 | | fthsect.y |
. . . 4
β’ (π β π β π΅) |
6 | | fthsect.m |
. . . 4
β’ (π β π β (ππ»π)) |
7 | | fthsect.n |
. . . 4
β’ (π β π β (ππ»π)) |
8 | | eqid 2733 |
. . . 4
β’
(SectβπΆ) =
(SectβπΆ) |
9 | | eqid 2733 |
. . . 4
β’
(Sectβπ·) =
(Sectβπ·) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | fthsect 17817 |
. . 3
β’ (π β (π(π(SectβπΆ)π)π β ((ππΊπ)βπ)((πΉβπ)(Sectβπ·)(πΉβπ))((ππΊπ)βπ))) |
11 | 1, 2, 3, 5, 4, 7, 6, 8, 9 | fthsect 17817 |
. . 3
β’ (π β (π(π(SectβπΆ)π)π β ((ππΊπ)βπ)((πΉβπ)(Sectβπ·)(πΉβπ))((ππΊπ)βπ))) |
12 | 10, 11 | anbi12d 632 |
. 2
β’ (π β ((π(π(SectβπΆ)π)π β§ π(π(SectβπΆ)π)π) β (((ππΊπ)βπ)((πΉβπ)(Sectβπ·)(πΉβπ))((ππΊπ)βπ) β§ ((ππΊπ)βπ)((πΉβπ)(Sectβπ·)(πΉβπ))((ππΊπ)βπ)))) |
13 | | fthinv.s |
. . 3
β’ πΌ = (InvβπΆ) |
14 | | fthfunc 17799 |
. . . . . . . 8
β’ (πΆ Faith π·) β (πΆ Func π·) |
15 | 14 | ssbri 5151 |
. . . . . . 7
β’ (πΉ(πΆ Faith π·)πΊ β πΉ(πΆ Func π·)πΊ) |
16 | 3, 15 | syl 17 |
. . . . . 6
β’ (π β πΉ(πΆ Func π·)πΊ) |
17 | | df-br 5107 |
. . . . . 6
β’ (πΉ(πΆ Func π·)πΊ β β¨πΉ, πΊβ© β (πΆ Func π·)) |
18 | 16, 17 | sylib 217 |
. . . . 5
β’ (π β β¨πΉ, πΊβ© β (πΆ Func π·)) |
19 | | funcrcl 17754 |
. . . . 5
β’
(β¨πΉ, πΊβ© β (πΆ Func π·) β (πΆ β Cat β§ π· β Cat)) |
20 | 18, 19 | syl 17 |
. . . 4
β’ (π β (πΆ β Cat β§ π· β Cat)) |
21 | 20 | simpld 496 |
. . 3
β’ (π β πΆ β Cat) |
22 | 1, 13, 21, 4, 5, 8 | isinv 17648 |
. 2
β’ (π β (π(ππΌπ)π β (π(π(SectβπΆ)π)π β§ π(π(SectβπΆ)π)π))) |
23 | | eqid 2733 |
. . 3
β’
(Baseβπ·) =
(Baseβπ·) |
24 | | fthinv.t |
. . 3
β’ π½ = (Invβπ·) |
25 | 20 | simprd 497 |
. . 3
β’ (π β π· β Cat) |
26 | 1, 23, 16 | funcf1 17757 |
. . . 4
β’ (π β πΉ:π΅βΆ(Baseβπ·)) |
27 | 26, 4 | ffvelcdmd 7037 |
. . 3
β’ (π β (πΉβπ) β (Baseβπ·)) |
28 | 26, 5 | ffvelcdmd 7037 |
. . 3
β’ (π β (πΉβπ) β (Baseβπ·)) |
29 | 23, 24, 25, 27, 28, 9 | isinv 17648 |
. 2
β’ (π β (((ππΊπ)βπ)((πΉβπ)π½(πΉβπ))((ππΊπ)βπ) β (((ππΊπ)βπ)((πΉβπ)(Sectβπ·)(πΉβπ))((ππΊπ)βπ) β§ ((ππΊπ)βπ)((πΉβπ)(Sectβπ·)(πΉβπ))((ππΊπ)βπ)))) |
30 | 12, 22, 29 | 3bitr4d 311 |
1
β’ (π β (π(ππΌπ)π β ((ππΊπ)βπ)((πΉβπ)π½(πΉβπ))((ππΊπ)βπ))) |