Step | Hyp | Ref
| Expression |
1 | | ringcsect.b |
. . 3
β’ π΅ = (BaseβπΆ) |
2 | | ringcinv.n |
. . 3
β’ π = (InvβπΆ) |
3 | | ringcsect.u |
. . . 4
β’ (π β π β π) |
4 | | ringcsect.c |
. . . . 5
β’ πΆ = (RingCatβπ) |
5 | 4 | ringccat 46396 |
. . . 4
β’ (π β π β πΆ β Cat) |
6 | 3, 5 | syl 17 |
. . 3
β’ (π β πΆ β Cat) |
7 | | ringcsect.x |
. . 3
β’ (π β π β π΅) |
8 | | ringcsect.y |
. . 3
β’ (π β π β π΅) |
9 | | eqid 2737 |
. . 3
β’
(SectβπΆ) =
(SectβπΆ) |
10 | 1, 2, 6, 7, 8, 9 | isinv 17650 |
. 2
β’ (π β (πΉ(πππ)πΊ β (πΉ(π(SectβπΆ)π)πΊ β§ πΊ(π(SectβπΆ)π)πΉ))) |
11 | | eqid 2737 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
12 | 4, 1, 3, 7, 8, 11,
9 | ringcsect 46403 |
. . . . 5
β’ (π β (πΉ(π(SectβπΆ)π)πΊ β (πΉ β (π RingHom π) β§ πΊ β (π RingHom π) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))))) |
13 | | df-3an 1090 |
. . . . 5
β’ ((πΉ β (π RingHom π) β§ πΊ β (π RingHom π) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β ((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ)))) |
14 | 12, 13 | bitrdi 287 |
. . . 4
β’ (π β (πΉ(π(SectβπΆ)π)πΊ β ((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))))) |
15 | | eqid 2737 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
16 | 4, 1, 3, 8, 7, 15,
9 | ringcsect 46403 |
. . . . 5
β’ (π β (πΊ(π(SectβπΆ)π)πΉ β (πΊ β (π RingHom π) β§ πΉ β (π RingHom π) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) |
17 | | 3ancoma 1099 |
. . . . . 6
β’ ((πΊ β (π RingHom π) β§ πΉ β (π RingHom π) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))) β (πΉ β (π RingHom π) β§ πΊ β (π RingHom π) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) |
18 | | df-3an 1090 |
. . . . . 6
β’ ((πΉ β (π RingHom π) β§ πΊ β (π RingHom π) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))) β ((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) |
19 | 17, 18 | bitri 275 |
. . . . 5
β’ ((πΊ β (π RingHom π) β§ πΉ β (π RingHom π) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))) β ((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) |
20 | 16, 19 | bitrdi 287 |
. . . 4
β’ (π β (πΊ(π(SectβπΆ)π)πΉ β ((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) |
21 | 14, 20 | anbi12d 632 |
. . 3
β’ (π β ((πΉ(π(SectβπΆ)π)πΊ β§ πΊ(π(SectβπΆ)π)πΉ) β (((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ ((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))))) |
22 | | anandi 675 |
. . 3
β’ ((((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ ((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) β ((((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RingHom π) β§ πΊ β (π RingHom π))) β§ (((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) |
23 | 21, 22 | bitrdi 287 |
. 2
β’ (π β ((πΉ(π(SectβπΆ)π)πΊ β§ πΊ(π(SectβπΆ)π)πΉ) β ((((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RingHom π) β§ πΊ β (π RingHom π))) β§ (((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))))) |
24 | | simplrl 776 |
. . . . . 6
β’
(((((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RingHom π) β§ πΊ β (π RingHom π))) β§ (((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) β πΉ β (π RingHom π)) |
25 | 24 | adantl 483 |
. . . . 5
β’ ((π β§ ((((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RingHom π) β§ πΊ β (π RingHom π))) β§ (((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) β πΉ β (π RingHom π)) |
26 | 11, 15 | rhmf 20167 |
. . . . . . . . . 10
β’ (πΉ β (π RingHom π) β πΉ:(Baseβπ)βΆ(Baseβπ)) |
27 | 15, 11 | rhmf 20167 |
. . . . . . . . . 10
β’ (πΊ β (π RingHom π) β πΊ:(Baseβπ)βΆ(Baseβπ)) |
28 | 26, 27 | anim12i 614 |
. . . . . . . . 9
β’ ((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β (πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ))) |
29 | 28 | ad2antlr 726 |
. . . . . . . 8
β’
(((((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RingHom π) β§ πΊ β (π RingHom π))) β§ (((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) β (πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ))) |
30 | | simpr 486 |
. . . . . . . . 9
β’ ((((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))) β (πΉ β πΊ) = ( I βΎ (Baseβπ))) |
31 | 30 | adantl 483 |
. . . . . . . 8
β’
(((((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RingHom π) β§ πΊ β (π RingHom π))) β§ (((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) β (πΉ β πΊ) = ( I βΎ (Baseβπ))) |
32 | | simpr 486 |
. . . . . . . . 9
β’ (((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β (πΊ β πΉ) = ( I βΎ (Baseβπ))) |
33 | 32 | ad2antrl 727 |
. . . . . . . 8
β’
(((((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RingHom π) β§ πΊ β (π RingHom π))) β§ (((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) β (πΊ β πΉ) = ( I βΎ (Baseβπ))) |
34 | 29, 31, 33 | jca32 517 |
. . . . . . 7
β’
(((((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RingHom π) β§ πΊ β (π RingHom π))) β§ (((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) β ((πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ)) β§ ((πΉ β πΊ) = ( I βΎ (Baseβπ)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))))) |
35 | 34 | adantl 483 |
. . . . . 6
β’ ((π β§ ((((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RingHom π) β§ πΊ β (π RingHom π))) β§ (((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) β ((πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ)) β§ ((πΉ β πΊ) = ( I βΎ (Baseβπ)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))))) |
36 | | fcof1o 7247 |
. . . . . . 7
β’ (((πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ)) β§ ((πΉ β πΊ) = ( I βΎ (Baseβπ)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ)))) β (πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ β‘πΉ = πΊ)) |
37 | | eqcom 2744 |
. . . . . . . 8
β’ (β‘πΉ = πΊ β πΊ = β‘πΉ) |
38 | 37 | anbi2i 624 |
. . . . . . 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
β’ ((π β§ ((((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RingHom π) β§ πΊ β (π RingHom π))) β§ (((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) β (πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ πΊ = β‘πΉ)) |
41 | | anass 470 |
. . . . 5
β’ (((πΉ β (π RingHom π) β§ πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)) β§ πΊ = β‘πΉ) β (πΉ β (π RingHom π) β§ (πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ πΊ = β‘πΉ))) |
42 | 25, 40, 41 | sylanbrc 584 |
. . . 4
β’ ((π β§ ((((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RingHom π) β§ πΊ β (π RingHom π))) β§ (((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) β ((πΉ β (π RingHom π) β§ πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)) β§ πΊ = β‘πΉ)) |
43 | 11, 15 | isrim 20174 |
. . . . . . 7
β’ (πΉ β (π RingIso π) β (πΉ β (π RingHom π) β§ πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ))) |
44 | 43 | a1i 11 |
. . . . . 6
β’ (π β (πΉ β (π RingIso π) β (πΉ β (π RingHom π) β§ πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)))) |
45 | 44 | anbi1d 631 |
. . . . 5
β’ (π β ((πΉ β (π RingIso π) β§ πΊ = β‘πΉ) β ((πΉ β (π RingHom π) β§ πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)) β§ πΊ = β‘πΉ))) |
46 | 45 | adantr 482 |
. . . 4
β’ ((π β§ ((((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RingHom π) β§ πΊ β (π RingHom π))) β§ (((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) β ((πΉ β (π RingIso π) β§ πΊ = β‘πΉ) β ((πΉ β (π RingHom π) β§ πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)) β§ πΊ = β‘πΉ))) |
47 | 42, 46 | mpbird 257 |
. . 3
β’ ((π β§ ((((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RingHom π) β§ πΊ β (π RingHom π))) β§ (((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) β (πΉ β (π RingIso π) β§ πΊ = β‘πΉ)) |
48 | | rimrhm 20178 |
. . . . . 6
β’ (πΉ β (π RingIso π) β πΉ β (π RingHom π)) |
49 | 48 | ad2antrl 727 |
. . . . 5
β’ ((π β§ (πΉ β (π RingIso π) β§ πΊ = β‘πΉ)) β πΉ β (π RingHom π)) |
50 | | isrim0 20165 |
. . . . . . . . 9
β’ (πΉ β (π RingIso π) β (πΉ β (π RingHom π) β§ β‘πΉ β (π RingHom π))) |
51 | 50 | simprbi 498 |
. . . . . . . 8
β’ (πΉ β (π RingIso π) β β‘πΉ β (π RingHom π)) |
52 | | eleq1 2826 |
. . . . . . . 8
β’ (πΊ = β‘πΉ β (πΊ β (π RingHom π) β β‘πΉ β (π RingHom π))) |
53 | 51, 52 | syl5ibrcom 247 |
. . . . . . 7
β’ (πΉ β (π RingIso π) β (πΊ = β‘πΉ β πΊ β (π RingHom π))) |
54 | 53 | imp 408 |
. . . . . 6
β’ ((πΉ β (π RingIso π) β§ πΊ = β‘πΉ) β πΊ β (π RingHom π)) |
55 | 54 | adantl 483 |
. . . . 5
β’ ((π β§ (πΉ β (π RingIso π) β§ πΊ = β‘πΉ)) β πΊ β (π RingHom π)) |
56 | | coeq1 5818 |
. . . . . . 7
β’ (πΊ = β‘πΉ β (πΊ β πΉ) = (β‘πΉ β πΉ)) |
57 | 56 | ad2antll 728 |
. . . . . 6
β’ ((π β§ (πΉ β (π RingIso π) β§ πΊ = β‘πΉ)) β (πΊ β πΉ) = (β‘πΉ β πΉ)) |
58 | 11, 15 | rimf1o 20176 |
. . . . . . . 8
β’ (πΉ β (π RingIso π) β πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)) |
59 | 58 | ad2antrl 727 |
. . . . . . 7
β’ ((π β§ (πΉ β (π RingIso π) β§ πΊ = β‘πΉ)) β πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)) |
60 | | f1ococnv1 6818 |
. . . . . . 7
β’ (πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ) β (β‘πΉ β πΉ) = ( I βΎ (Baseβπ))) |
61 | 59, 60 | syl 17 |
. . . . . 6
β’ ((π β§ (πΉ β (π RingIso π) β§ πΊ = β‘πΉ)) β (β‘πΉ β πΉ) = ( I βΎ (Baseβπ))) |
62 | 57, 61 | eqtrd 2777 |
. . . . 5
β’ ((π β§ (πΉ β (π RingIso π) β§ πΊ = β‘πΉ)) β (πΊ β πΉ) = ( I βΎ (Baseβπ))) |
63 | 49, 55, 62 | jca31 516 |
. . . 4
β’ ((π β§ (πΉ β (π RingIso π) β§ πΊ = β‘πΉ)) β ((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ)))) |
64 | 50 | biimpi 215 |
. . . . . 6
β’ (πΉ β (π RingIso π) β (πΉ β (π RingHom π) β§ β‘πΉ β (π RingHom π))) |
65 | 64 | ad2antrl 727 |
. . . . 5
β’ ((π β§ (πΉ β (π RingIso π) β§ πΊ = β‘πΉ)) β (πΉ β (π RingHom π) β§ β‘πΉ β (π RingHom π))) |
66 | 52 | ad2antll 728 |
. . . . . 6
β’ ((π β§ (πΉ β (π RingIso π) β§ πΊ = β‘πΉ)) β (πΊ β (π RingHom π) β β‘πΉ β (π RingHom π))) |
67 | 66 | anbi2d 630 |
. . . . 5
β’ ((π β§ (πΉ β (π RingIso π) β§ πΊ = β‘πΉ)) β ((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β (πΉ β (π RingHom π) β§ β‘πΉ β (π RingHom π)))) |
68 | 65, 67 | mpbird 257 |
. . . 4
β’ ((π β§ (πΉ β (π RingIso π) β§ πΊ = β‘πΉ)) β (πΉ β (π RingHom π) β§ πΊ β (π RingHom π))) |
69 | | coeq2 5819 |
. . . . . . 7
β’ (πΊ = β‘πΉ β (πΉ β πΊ) = (πΉ β β‘πΉ)) |
70 | 69 | ad2antll 728 |
. . . . . 6
β’ ((π β§ (πΉ β (π RingIso π) β§ πΊ = β‘πΉ)) β (πΉ β πΊ) = (πΉ β β‘πΉ)) |
71 | | f1ococnv2 6816 |
. . . . . . 7
β’ (πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ) β (πΉ β β‘πΉ) = ( I βΎ (Baseβπ))) |
72 | 59, 71 | syl 17 |
. . . . . 6
β’ ((π β§ (πΉ β (π RingIso π) β§ πΊ = β‘πΉ)) β (πΉ β β‘πΉ) = ( I βΎ (Baseβπ))) |
73 | 70, 72 | eqtrd 2777 |
. . . . 5
β’ ((π β§ (πΉ β (π RingIso π) β§ πΊ = β‘πΉ)) β (πΉ β πΊ) = ( I βΎ (Baseβπ))) |
74 | 68, 62, 73 | jca31 516 |
. . . 4
β’ ((π β§ (πΉ β (π RingIso π) β§ πΊ = β‘πΉ)) β (((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) |
75 | 63, 68, 74 | jca31 516 |
. . 3
β’ ((π β§ (πΉ β (π RingIso π) β§ πΊ = β‘πΉ)) β ((((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RingHom π) β§ πΊ β (π RingHom π))) β§ (((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) |
76 | 47, 75 | impbida 800 |
. 2
β’ (π β (((((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RingHom π) β§ πΊ β (π RingHom π))) β§ (((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) β (πΉ β (π RingIso π) β§ πΊ = β‘πΉ))) |
77 | 10, 23, 76 | 3bitrd 305 |
1
β’ (π β (πΉ(πππ)πΊ β (πΉ β (π RingIso π) β§ πΊ = β‘πΉ))) |