Step | Hyp | Ref
| Expression |
1 | | rngcsectALTV.b |
. . 3
β’ π΅ = (BaseβπΆ) |
2 | | eqid 2726 |
. . 3
β’ (Hom
βπΆ) = (Hom
βπΆ) |
3 | | eqid 2726 |
. . 3
β’
(compβπΆ) =
(compβπΆ) |
4 | | eqid 2726 |
. . 3
β’
(IdβπΆ) =
(IdβπΆ) |
5 | | rngcsectALTV.n |
. . 3
β’ π = (SectβπΆ) |
6 | | rngcsectALTV.u |
. . . 4
β’ (π β π β π) |
7 | | rngcsectALTV.c |
. . . . 5
β’ πΆ = (RngCatALTVβπ) |
8 | 7 | rngccatALTV 47223 |
. . . 4
β’ (π β π β πΆ β Cat) |
9 | 6, 8 | syl 17 |
. . 3
β’ (π β πΆ β Cat) |
10 | | rngcsectALTV.x |
. . 3
β’ (π β π β π΅) |
11 | | rngcsectALTV.y |
. . 3
β’ (π β π β π΅) |
12 | 1, 2, 3, 4, 5, 9, 10, 11 | issect 17709 |
. 2
β’ (π β (πΉ(πππ)πΊ β (πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)))) |
13 | 7, 1, 6, 2, 10, 11 | rngchomALTV 47218 |
. . . . . . 7
β’ (π β (π(Hom βπΆ)π) = (π RngHom π)) |
14 | 13 | eleq2d 2813 |
. . . . . 6
β’ (π β (πΉ β (π(Hom βπΆ)π) β πΉ β (π RngHom π))) |
15 | 7, 1, 6, 2, 11, 10 | rngchomALTV 47218 |
. . . . . . 7
β’ (π β (π(Hom βπΆ)π) = (π RngHom π)) |
16 | 15 | eleq2d 2813 |
. . . . . 6
β’ (π β (πΊ β (π(Hom βπΆ)π) β πΊ β (π RngHom π))) |
17 | 14, 16 | anbi12d 630 |
. . . . 5
β’ (π β ((πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π)) β (πΉ β (π RngHom π) β§ πΊ β (π RngHom π)))) |
18 | 17 | anbi1d 629 |
. . . 4
β’ (π β (((πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π)) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)) β ((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)))) |
19 | 6 | adantr 480 |
. . . . . . 7
β’ ((π β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β π β π) |
20 | 10 | adantr 480 |
. . . . . . 7
β’ ((π β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β π β π΅) |
21 | 11 | adantr 480 |
. . . . . . 7
β’ ((π β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β π β π΅) |
22 | | simprl 768 |
. . . . . . 7
β’ ((π β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β πΉ β (π RngHom π)) |
23 | | simprr 770 |
. . . . . . 7
β’ ((π β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β πΊ β (π RngHom π)) |
24 | 7, 1, 19, 3, 20, 21, 20, 22, 23 | rngccoALTV 47221 |
. . . . . 6
β’ ((π β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = (πΊ β πΉ)) |
25 | | rngcsectALTV.e |
. . . . . . . 8
β’ πΈ = (Baseβπ) |
26 | 7, 1, 4, 6, 10, 25 | rngcidALTV 47224 |
. . . . . . 7
β’ (π β ((IdβπΆ)βπ) = ( I βΎ πΈ)) |
27 | 26 | adantr 480 |
. . . . . 6
β’ ((π β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β ((IdβπΆ)βπ) = ( I βΎ πΈ)) |
28 | 24, 27 | eqeq12d 2742 |
. . . . 5
β’ ((π β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β ((πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ) β (πΊ β πΉ) = ( I βΎ πΈ))) |
29 | 28 | pm5.32da 578 |
. . . 4
β’ (π β (((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)) β ((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ πΈ)))) |
30 | 18, 29 | bitrd 279 |
. . 3
β’ (π β (((πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π)) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)) β ((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ πΈ)))) |
31 | | df-3an 1086 |
. . 3
β’ ((πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)) β ((πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π)) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ))) |
32 | | df-3an 1086 |
. . 3
β’ ((πΉ β (π RngHom π) β§ πΊ β (π RngHom π) β§ (πΊ β πΉ) = ( I βΎ πΈ)) β ((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ πΈ))) |
33 | 30, 31, 32 | 3bitr4g 314 |
. 2
β’ (π β ((πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)) β (πΉ β (π RngHom π) β§ πΊ β (π RngHom π) β§ (πΊ β πΉ) = ( I βΎ πΈ)))) |
34 | 12, 33 | bitrd 279 |
1
β’ (π β (πΉ(πππ)πΊ β (πΉ β (π RngHom π) β§ πΊ β (π RngHom π) β§ (πΊ β πΉ) = ( I βΎ πΈ)))) |