Step | Hyp | Ref
| Expression |
1 | | rngcsect.b |
. . 3
β’ π΅ = (BaseβπΆ) |
2 | | eqid 2731 |
. . 3
β’ (Hom
βπΆ) = (Hom
βπΆ) |
3 | | eqid 2731 |
. . 3
β’
(compβπΆ) =
(compβπΆ) |
4 | | eqid 2731 |
. . 3
β’
(IdβπΆ) =
(IdβπΆ) |
5 | | rngcsect.n |
. . 3
β’ π = (SectβπΆ) |
6 | | rngcsect.u |
. . . 4
β’ (π β π β π) |
7 | | rngcsect.c |
. . . . 5
β’ πΆ = (RngCatβπ) |
8 | 7 | rngccat 46429 |
. . . 4
β’ (π β π β πΆ β Cat) |
9 | 6, 8 | syl 17 |
. . 3
β’ (π β πΆ β Cat) |
10 | | rngcsect.x |
. . 3
β’ (π β π β π΅) |
11 | | rngcsect.y |
. . 3
β’ (π β π β π΅) |
12 | 1, 2, 3, 4, 5, 9, 10, 11 | issect 17665 |
. 2
β’ (π β (πΉ(πππ)πΊ β (πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)))) |
13 | 7, 1, 6, 2, 10, 11 | rngchom 46418 |
. . . . . . 7
β’ (π β (π(Hom βπΆ)π) = (π RngHomo π)) |
14 | 13 | eleq2d 2818 |
. . . . . 6
β’ (π β (πΉ β (π(Hom βπΆ)π) β πΉ β (π RngHomo π))) |
15 | 7, 1, 6, 2, 11, 10 | rngchom 46418 |
. . . . . . 7
β’ (π β (π(Hom βπΆ)π) = (π RngHomo π)) |
16 | 15 | eleq2d 2818 |
. . . . . 6
β’ (π β (πΊ β (π(Hom βπΆ)π) β πΊ β (π RngHomo π))) |
17 | 14, 16 | anbi12d 631 |
. . . . 5
β’ (π β ((πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π)) β (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)))) |
18 | 17 | anbi1d 630 |
. . . 4
β’ (π β (((πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π)) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)) β ((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)))) |
19 | 6 | adantr 481 |
. . . . . . 7
β’ ((π β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β π β π) |
20 | 10 | adantr 481 |
. . . . . . . 8
β’ ((π β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β π β π΅) |
21 | 7, 1, 6 | rngcbas 46416 |
. . . . . . . . . . 11
β’ (π β π΅ = (π β© Rng)) |
22 | 21 | eleq2d 2818 |
. . . . . . . . . 10
β’ (π β (π β π΅ β π β (π β© Rng))) |
23 | | inss1 4208 |
. . . . . . . . . . . 12
β’ (π β© Rng) β π |
24 | 23 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (π β© Rng) β π) |
25 | 24 | sseld 3961 |
. . . . . . . . . 10
β’ (π β (π β (π β© Rng) β π β π)) |
26 | 22, 25 | sylbid 239 |
. . . . . . . . 9
β’ (π β (π β π΅ β π β π)) |
27 | 26 | adantr 481 |
. . . . . . . 8
β’ ((π β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β (π β π΅ β π β π)) |
28 | 20, 27 | mpd 15 |
. . . . . . 7
β’ ((π β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β π β π) |
29 | 11 | adantr 481 |
. . . . . . . 8
β’ ((π β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β π β π΅) |
30 | 21 | eleq2d 2818 |
. . . . . . . . . 10
β’ (π β (π β π΅ β π β (π β© Rng))) |
31 | 24 | sseld 3961 |
. . . . . . . . . 10
β’ (π β (π β (π β© Rng) β π β π)) |
32 | 30, 31 | sylbid 239 |
. . . . . . . . 9
β’ (π β (π β π΅ β π β π)) |
33 | 32 | adantr 481 |
. . . . . . . 8
β’ ((π β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β (π β π΅ β π β π)) |
34 | 29, 33 | mpd 15 |
. . . . . . 7
β’ ((π β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β π β π) |
35 | | eqid 2731 |
. . . . . . . . . 10
β’
(Baseβπ) =
(Baseβπ) |
36 | | eqid 2731 |
. . . . . . . . . 10
β’
(Baseβπ) =
(Baseβπ) |
37 | 35, 36 | rnghmf 46350 |
. . . . . . . . 9
β’ (πΉ β (π RngHomo π) β πΉ:(Baseβπ)βΆ(Baseβπ)) |
38 | 37 | adantr 481 |
. . . . . . . 8
β’ ((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β πΉ:(Baseβπ)βΆ(Baseβπ)) |
39 | 38 | adantl 482 |
. . . . . . 7
β’ ((π β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β πΉ:(Baseβπ)βΆ(Baseβπ)) |
40 | 36, 35 | rnghmf 46350 |
. . . . . . . . 9
β’ (πΊ β (π RngHomo π) β πΊ:(Baseβπ)βΆ(Baseβπ)) |
41 | 40 | adantl 482 |
. . . . . . . 8
β’ ((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β πΊ:(Baseβπ)βΆ(Baseβπ)) |
42 | 41 | adantl 482 |
. . . . . . 7
β’ ((π β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β πΊ:(Baseβπ)βΆ(Baseβπ)) |
43 | 7, 19, 3, 28, 34, 28, 39, 42 | rngcco 46422 |
. . . . . 6
β’ ((π β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = (πΊ β πΉ)) |
44 | | rngcsect.e |
. . . . . . . 8
β’ πΈ = (Baseβπ) |
45 | 7, 1, 4, 6, 10, 44 | rngcid 46430 |
. . . . . . 7
β’ (π β ((IdβπΆ)βπ) = ( I βΎ πΈ)) |
46 | 45 | adantr 481 |
. . . . . 6
β’ ((π β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β ((IdβπΆ)βπ) = ( I βΎ πΈ)) |
47 | 43, 46 | eqeq12d 2747 |
. . . . 5
β’ ((π β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β ((πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ) β (πΊ β πΉ) = ( I βΎ πΈ))) |
48 | 47 | pm5.32da 579 |
. . . 4
β’ (π β (((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)) β ((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ πΈ)))) |
49 | 18, 48 | bitrd 278 |
. . 3
β’ (π β (((πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π)) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)) β ((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ πΈ)))) |
50 | | df-3an 1089 |
. . 3
β’ ((πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)) β ((πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π)) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ))) |
51 | | df-3an 1089 |
. . 3
β’ ((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π) β§ (πΊ β πΉ) = ( I βΎ πΈ)) β ((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ πΈ))) |
52 | 49, 50, 51 | 3bitr4g 313 |
. 2
β’ (π β ((πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)) β (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π) β§ (πΊ β πΉ) = ( I βΎ πΈ)))) |
53 | 12, 52 | bitrd 278 |
1
β’ (π β (πΉ(πππ)πΊ β (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π) β§ (πΊ β πΉ) = ( I βΎ πΈ)))) |