Step | Hyp | Ref
| Expression |
1 | | rngcsect.b |
. . 3
β’ π΅ = (BaseβπΆ) |
2 | | rngcinv.n |
. . 3
β’ π = (InvβπΆ) |
3 | | rngcsect.u |
. . . 4
β’ (π β π β π) |
4 | | rngcsect.c |
. . . . 5
β’ πΆ = (RngCatβπ) |
5 | 4 | rngccat 20527 |
. . . 4
β’ (π β π β πΆ β Cat) |
6 | 3, 5 | syl 17 |
. . 3
β’ (π β πΆ β Cat) |
7 | | rngcsect.x |
. . 3
β’ (π β π β π΅) |
8 | | rngcsect.y |
. . 3
β’ (π β π β π΅) |
9 | | eqid 2726 |
. . 3
β’
(SectβπΆ) =
(SectβπΆ) |
10 | 1, 2, 6, 7, 8, 9 | isinv 17713 |
. 2
β’ (π β (πΉ(πππ)πΊ β (πΉ(π(SectβπΆ)π)πΊ β§ πΊ(π(SectβπΆ)π)πΉ))) |
11 | | eqid 2726 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
12 | 4, 1, 3, 7, 8, 11,
9 | rngcsect 20529 |
. . . . 5
β’ (π β (πΉ(π(SectβπΆ)π)πΊ β (πΉ β (π RngHom π) β§ πΊ β (π RngHom π) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))))) |
13 | | df-3an 1086 |
. . . . 5
β’ ((πΉ β (π RngHom π) β§ πΊ β (π RngHom π) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β ((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ)))) |
14 | 12, 13 | bitrdi 287 |
. . . 4
β’ (π β (πΉ(π(SectβπΆ)π)πΊ β ((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))))) |
15 | | eqid 2726 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
16 | 4, 1, 3, 8, 7, 15,
9 | rngcsect 20529 |
. . . . 5
β’ (π β (πΊ(π(SectβπΆ)π)πΉ β (πΊ β (π RngHom π) β§ πΉ β (π RngHom π) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) |
17 | | 3ancoma 1095 |
. . . . . 6
β’ ((πΊ β (π RngHom π) β§ πΉ β (π RngHom π) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))) β (πΉ β (π RngHom π) β§ πΊ β (π RngHom π) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) |
18 | | df-3an 1086 |
. . . . . 6
β’ ((πΉ β (π RngHom π) β§ πΊ β (π RngHom π) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))) β ((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) |
19 | 17, 18 | bitri 275 |
. . . . 5
β’ ((πΊ β (π RngHom π) β§ πΉ β (π RngHom π) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))) β ((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) |
20 | 16, 19 | bitrdi 287 |
. . . 4
β’ (π β (πΊ(π(SectβπΆ)π)πΉ β ((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) |
21 | 14, 20 | anbi12d 630 |
. . 3
β’ (π β ((πΉ(π(SectβπΆ)π)πΊ β§ πΊ(π(SectβπΆ)π)πΉ) β (((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ ((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))))) |
22 | | anandi 673 |
. . 3
β’ ((((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ ((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) β ((((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β§ (((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) |
23 | 21, 22 | bitrdi 287 |
. 2
β’ (π β ((πΉ(π(SectβπΆ)π)πΊ β§ πΊ(π(SectβπΆ)π)πΉ) β ((((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β§ (((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))))) |
24 | | simplrl 774 |
. . . . . 6
β’
(((((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β§ (((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) β πΉ β (π RngHom π)) |
25 | 24 | adantl 481 |
. . . . 5
β’ ((π β§ ((((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β§ (((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) β πΉ β (π RngHom π)) |
26 | 11, 15 | rnghmf 20347 |
. . . . . . . . . 10
β’ (πΉ β (π RngHom π) β πΉ:(Baseβπ)βΆ(Baseβπ)) |
27 | 15, 11 | rnghmf 20347 |
. . . . . . . . . 10
β’ (πΊ β (π RngHom π) β πΊ:(Baseβπ)βΆ(Baseβπ)) |
28 | 26, 27 | anim12i 612 |
. . . . . . . . 9
β’ ((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β (πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ))) |
29 | 28 | ad2antlr 724 |
. . . . . . . 8
β’
(((((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β§ (((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) β (πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ))) |
30 | | simpr 484 |
. . . . . . . . 9
β’ ((((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))) β (πΉ β πΊ) = ( I βΎ (Baseβπ))) |
31 | 30 | adantl 481 |
. . . . . . . 8
β’
(((((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β§ (((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) β (πΉ β πΊ) = ( I βΎ (Baseβπ))) |
32 | | simpr 484 |
. . . . . . . . 9
β’ (((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β (πΊ β πΉ) = ( I βΎ (Baseβπ))) |
33 | 32 | ad2antrl 725 |
. . . . . . . 8
β’
(((((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β§ (((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) β (πΊ β πΉ) = ( I βΎ (Baseβπ))) |
34 | 29, 31, 33 | jca32 515 |
. . . . . . 7
β’
(((((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β§ (((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) β ((πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ)) β§ ((πΉ β πΊ) = ( I βΎ (Baseβπ)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))))) |
35 | 34 | adantl 481 |
. . . . . 6
β’ ((π β§ ((((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β§ (((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) β ((πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ)) β§ ((πΉ β πΊ) = ( I βΎ (Baseβπ)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))))) |
36 | | fcof1o 7289 |
. . . . . . 7
β’ (((πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ)) β§ ((πΉ β πΊ) = ( I βΎ (Baseβπ)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ)))) β (πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ β‘πΉ = πΊ)) |
37 | | eqcom 2733 |
. . . . . . . 8
β’ (β‘πΉ = πΊ β πΊ = β‘πΉ) |
38 | 37 | anbi2i 622 |
. . . . . . 7
β’ ((πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ β‘πΉ = πΊ) β (πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ πΊ = β‘πΉ)) |
39 | 36, 38 | sylib 217 |
. . . . . 6
β’ (((πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ)) β§ ((πΉ β πΊ) = ( I βΎ (Baseβπ)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ)))) β (πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ πΊ = β‘πΉ)) |
40 | 35, 39 | syl 17 |
. . . . 5
β’ ((π β§ ((((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β§ (((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) β (πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ πΊ = β‘πΉ)) |
41 | | anass 468 |
. . . . 5
β’ (((πΉ β (π RngHom π) β§ πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)) β§ πΊ = β‘πΉ) β (πΉ β (π RngHom π) β§ (πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ πΊ = β‘πΉ))) |
42 | 25, 40, 41 | sylanbrc 582 |
. . . 4
β’ ((π β§ ((((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β§ (((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) β ((πΉ β (π RngHom π) β§ πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)) β§ πΊ = β‘πΉ)) |
43 | 11, 15 | isrngim2 20352 |
. . . . . . 7
β’ ((π β π΅ β§ π β π΅) β (πΉ β (π RngIso π) β (πΉ β (π RngHom π) β§ πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)))) |
44 | 7, 8, 43 | syl2anc 583 |
. . . . . 6
β’ (π β (πΉ β (π RngIso π) β (πΉ β (π RngHom π) β§ πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)))) |
45 | 44 | anbi1d 629 |
. . . . 5
β’ (π β ((πΉ β (π RngIso π) β§ πΊ = β‘πΉ) β ((πΉ β (π RngHom π) β§ πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)) β§ πΊ = β‘πΉ))) |
46 | 45 | adantr 480 |
. . . 4
β’ ((π β§ ((((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β§ (((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) β ((πΉ β (π RngIso π) β§ πΊ = β‘πΉ) β ((πΉ β (π RngHom π) β§ πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)) β§ πΊ = β‘πΉ))) |
47 | 42, 46 | mpbird 257 |
. . 3
β’ ((π β§ ((((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β§ (((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) β (πΉ β (π RngIso π) β§ πΊ = β‘πΉ)) |
48 | 11, 15 | rngimrnghm 20354 |
. . . . . 6
β’ (πΉ β (π RngIso π) β πΉ β (π RngHom π)) |
49 | 48 | ad2antrl 725 |
. . . . 5
β’ ((π β§ (πΉ β (π RngIso π) β§ πΊ = β‘πΉ)) β πΉ β (π RngHom π)) |
50 | | isrngim 20344 |
. . . . . . . . . . 11
β’ ((π β π΅ β§ π β π΅) β (πΉ β (π RngIso π) β (πΉ β (π RngHom π) β§ β‘πΉ β (π RngHom π)))) |
51 | 7, 8, 50 | syl2anc 583 |
. . . . . . . . . 10
β’ (π β (πΉ β (π RngIso π) β (πΉ β (π RngHom π) β§ β‘πΉ β (π RngHom π)))) |
52 | | eleq1 2815 |
. . . . . . . . . . . 12
β’ (β‘πΉ = πΊ β (β‘πΉ β (π RngHom π) β πΊ β (π RngHom π))) |
53 | 52 | eqcoms 2734 |
. . . . . . . . . . 11
β’ (πΊ = β‘πΉ β (β‘πΉ β (π RngHom π) β πΊ β (π RngHom π))) |
54 | 53 | anbi2d 628 |
. . . . . . . . . 10
β’ (πΊ = β‘πΉ β ((πΉ β (π RngHom π) β§ β‘πΉ β (π RngHom π)) β (πΉ β (π RngHom π) β§ πΊ β (π RngHom π)))) |
55 | 51, 54 | sylan9bbr 510 |
. . . . . . . . 9
β’ ((πΊ = β‘πΉ β§ π) β (πΉ β (π RngIso π) β (πΉ β (π RngHom π) β§ πΊ β (π RngHom π)))) |
56 | | simpr 484 |
. . . . . . . . 9
β’ ((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β πΊ β (π RngHom π)) |
57 | 55, 56 | biimtrdi 252 |
. . . . . . . 8
β’ ((πΊ = β‘πΉ β§ π) β (πΉ β (π RngIso π) β πΊ β (π RngHom π))) |
58 | 57 | com12 32 |
. . . . . . 7
β’ (πΉ β (π RngIso π) β ((πΊ = β‘πΉ β§ π) β πΊ β (π RngHom π))) |
59 | 58 | expdimp 452 |
. . . . . 6
β’ ((πΉ β (π RngIso π) β§ πΊ = β‘πΉ) β (π β πΊ β (π RngHom π))) |
60 | 59 | impcom 407 |
. . . . 5
β’ ((π β§ (πΉ β (π RngIso π) β§ πΊ = β‘πΉ)) β πΊ β (π RngHom π)) |
61 | | coeq1 5850 |
. . . . . . 7
β’ (πΊ = β‘πΉ β (πΊ β πΉ) = (β‘πΉ β πΉ)) |
62 | 61 | ad2antll 726 |
. . . . . 6
β’ ((π β§ (πΉ β (π RngIso π) β§ πΊ = β‘πΉ)) β (πΊ β πΉ) = (β‘πΉ β πΉ)) |
63 | 11, 15 | rngimf1o 20353 |
. . . . . . . 8
β’ (πΉ β (π RngIso π) β πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)) |
64 | 63 | ad2antrl 725 |
. . . . . . 7
β’ ((π β§ (πΉ β (π RngIso π) β§ πΊ = β‘πΉ)) β πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)) |
65 | | f1ococnv1 6855 |
. . . . . . 7
β’ (πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ) β (β‘πΉ β πΉ) = ( I βΎ (Baseβπ))) |
66 | 64, 65 | syl 17 |
. . . . . 6
β’ ((π β§ (πΉ β (π RngIso π) β§ πΊ = β‘πΉ)) β (β‘πΉ β πΉ) = ( I βΎ (Baseβπ))) |
67 | 62, 66 | eqtrd 2766 |
. . . . 5
β’ ((π β§ (πΉ β (π RngIso π) β§ πΊ = β‘πΉ)) β (πΊ β πΉ) = ( I βΎ (Baseβπ))) |
68 | 49, 60, 67 | jca31 514 |
. . . 4
β’ ((π β§ (πΉ β (π RngIso π) β§ πΊ = β‘πΉ)) β ((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ)))) |
69 | 51 | biimpcd 248 |
. . . . . . 7
β’ (πΉ β (π RngIso π) β (π β (πΉ β (π RngHom π) β§ β‘πΉ β (π RngHom π)))) |
70 | 69 | adantr 480 |
. . . . . 6
β’ ((πΉ β (π RngIso π) β§ πΊ = β‘πΉ) β (π β (πΉ β (π RngHom π) β§ β‘πΉ β (π RngHom π)))) |
71 | 70 | impcom 407 |
. . . . 5
β’ ((π β§ (πΉ β (π RngIso π) β§ πΊ = β‘πΉ)) β (πΉ β (π RngHom π) β§ β‘πΉ β (π RngHom π))) |
72 | | eleq1 2815 |
. . . . . . 7
β’ (πΊ = β‘πΉ β (πΊ β (π RngHom π) β β‘πΉ β (π RngHom π))) |
73 | 72 | ad2antll 726 |
. . . . . 6
β’ ((π β§ (πΉ β (π RngIso π) β§ πΊ = β‘πΉ)) β (πΊ β (π RngHom π) β β‘πΉ β (π RngHom π))) |
74 | 73 | anbi2d 628 |
. . . . 5
β’ ((π β§ (πΉ β (π RngIso π) β§ πΊ = β‘πΉ)) β ((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β (πΉ β (π RngHom π) β§ β‘πΉ β (π RngHom π)))) |
75 | 71, 74 | mpbird 257 |
. . . 4
β’ ((π β§ (πΉ β (π RngIso π) β§ πΊ = β‘πΉ)) β (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) |
76 | | coeq2 5851 |
. . . . . . 7
β’ (πΊ = β‘πΉ β (πΉ β πΊ) = (πΉ β β‘πΉ)) |
77 | 76 | ad2antll 726 |
. . . . . 6
β’ ((π β§ (πΉ β (π RngIso π) β§ πΊ = β‘πΉ)) β (πΉ β πΊ) = (πΉ β β‘πΉ)) |
78 | | f1ococnv2 6853 |
. . . . . . 7
β’ (πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ) β (πΉ β β‘πΉ) = ( I βΎ (Baseβπ))) |
79 | 64, 78 | syl 17 |
. . . . . 6
β’ ((π β§ (πΉ β (π RngIso π) β§ πΊ = β‘πΉ)) β (πΉ β β‘πΉ) = ( I βΎ (Baseβπ))) |
80 | 77, 79 | eqtrd 2766 |
. . . . 5
β’ ((π β§ (πΉ β (π RngIso π) β§ πΊ = β‘πΉ)) β (πΉ β πΊ) = ( I βΎ (Baseβπ))) |
81 | 75, 67, 80 | jca31 514 |
. . . 4
β’ ((π β§ (πΉ β (π RngIso π) β§ πΊ = β‘πΉ)) β (((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) |
82 | 68, 75, 81 | jca31 514 |
. . 3
β’ ((π β§ (πΉ β (π RngIso π) β§ πΊ = β‘πΉ)) β ((((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β§ (((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) |
83 | 47, 82 | impbida 798 |
. 2
β’ (π β (((((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β§ (((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) β (πΉ β (π RngIso π) β§ πΊ = β‘πΉ))) |
84 | 10, 23, 83 | 3bitrd 305 |
1
β’ (π β (πΉ(πππ)πΊ β (πΉ β (π RngIso π) β§ πΊ = β‘πΉ))) |