Step | Hyp | Ref
| Expression |
1 | | animorrl 980 |
. . . . . 6
β’ (((π
β DivRing β§ π β π) β§ π = { 0 }) β (π = { 0 } β¨ π = π΅)) |
2 | | drngring 20204 |
. . . . . . . . . . 11
β’ (π
β DivRing β π
β Ring) |
3 | 2 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π
β DivRing β§ π β π) β§ π β { 0 }) β π
β Ring) |
4 | | simplr 768 |
. . . . . . . . . 10
β’ (((π
β DivRing β§ π β π) β§ π β { 0 }) β π β π) |
5 | | simpr 486 |
. . . . . . . . . 10
β’ (((π
β DivRing β§ π β π) β§ π β { 0 }) β π β { 0 }) |
6 | | drngnidl.u |
. . . . . . . . . . 11
β’ π = (LIdealβπ
) |
7 | | drngnidl.z |
. . . . . . . . . . 11
β’ 0 =
(0gβπ
) |
8 | 6, 7 | lidlnz 20714 |
. . . . . . . . . 10
β’ ((π
β Ring β§ π β π β§ π β { 0 }) β βπ β π π β 0 ) |
9 | 3, 4, 5, 8 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π
β DivRing β§ π β π) β§ π β { 0 }) β βπ β π π β 0 ) |
10 | | simpll 766 |
. . . . . . . . . . . . 13
β’ (((π
β DivRing β§ π β π) β§ (π β π β§ π β 0 )) β π
β
DivRing) |
11 | | drngnidl.b |
. . . . . . . . . . . . . . . . 17
β’ π΅ = (Baseβπ
) |
12 | 11, 6 | lidlss 20696 |
. . . . . . . . . . . . . . . 16
β’ (π β π β π β π΅) |
13 | 12 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π
β DivRing β§ π β π) β π β π΅) |
14 | 13 | sselda 3945 |
. . . . . . . . . . . . . 14
β’ (((π
β DivRing β§ π β π) β§ π β π) β π β π΅) |
15 | 14 | adantrr 716 |
. . . . . . . . . . . . 13
β’ (((π
β DivRing β§ π β π) β§ (π β π β§ π β 0 )) β π β π΅) |
16 | | simprr 772 |
. . . . . . . . . . . . 13
β’ (((π
β DivRing β§ π β π) β§ (π β π β§ π β 0 )) β π β 0 ) |
17 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(.rβπ
) = (.rβπ
) |
18 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(1rβπ
) = (1rβπ
) |
19 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(invrβπ
) = (invrβπ
) |
20 | 11, 7, 17, 18, 19 | drnginvrl 20220 |
. . . . . . . . . . . . 13
β’ ((π
β DivRing β§ π β π΅ β§ π β 0 ) β
(((invrβπ
)βπ)(.rβπ
)π) = (1rβπ
)) |
21 | 10, 15, 16, 20 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π
β DivRing β§ π β π) β§ (π β π β§ π β 0 )) β
(((invrβπ
)βπ)(.rβπ
)π) = (1rβπ
)) |
22 | 2 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π
β DivRing β§ π β π) β§ (π β π β§ π β 0 )) β π
β Ring) |
23 | | simplr 768 |
. . . . . . . . . . . . 13
β’ (((π
β DivRing β§ π β π) β§ (π β π β§ π β 0 )) β π β π) |
24 | 11, 7, 19 | drnginvrcl 20217 |
. . . . . . . . . . . . . 14
β’ ((π
β DivRing β§ π β π΅ β§ π β 0 ) β
((invrβπ
)βπ) β π΅) |
25 | 10, 15, 16, 24 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π
β DivRing β§ π β π) β§ (π β π β§ π β 0 )) β
((invrβπ
)βπ) β π΅) |
26 | | simprl 770 |
. . . . . . . . . . . . 13
β’ (((π
β DivRing β§ π β π) β§ (π β π β§ π β 0 )) β π β π) |
27 | 6, 11, 17 | lidlmcl 20703 |
. . . . . . . . . . . . 13
β’ (((π
β Ring β§ π β π) β§ (((invrβπ
)βπ) β π΅ β§ π β π)) β (((invrβπ
)βπ)(.rβπ
)π) β π) |
28 | 22, 23, 25, 26, 27 | syl22anc 838 |
. . . . . . . . . . . 12
β’ (((π
β DivRing β§ π β π) β§ (π β π β§ π β 0 )) β
(((invrβπ
)βπ)(.rβπ
)π) β π) |
29 | 21, 28 | eqeltrrd 2835 |
. . . . . . . . . . 11
β’ (((π
β DivRing β§ π β π) β§ (π β π β§ π β 0 )) β
(1rβπ
)
β π) |
30 | 29 | rexlimdvaa 3150 |
. . . . . . . . . 10
β’ ((π
β DivRing β§ π β π) β (βπ β π π β 0 β
(1rβπ
)
β π)) |
31 | 30 | imp 408 |
. . . . . . . . 9
β’ (((π
β DivRing β§ π β π) β§ βπ β π π β 0 ) β
(1rβπ
)
β π) |
32 | 9, 31 | syldan 592 |
. . . . . . . 8
β’ (((π
β DivRing β§ π β π) β§ π β { 0 }) β
(1rβπ
)
β π) |
33 | 6, 11, 18 | lidl1el 20704 |
. . . . . . . . . 10
β’ ((π
β Ring β§ π β π) β ((1rβπ
) β π β π = π΅)) |
34 | 2, 33 | sylan 581 |
. . . . . . . . 9
β’ ((π
β DivRing β§ π β π) β ((1rβπ
) β π β π = π΅)) |
35 | 34 | adantr 482 |
. . . . . . . 8
β’ (((π
β DivRing β§ π β π) β§ π β { 0 }) β
((1rβπ
)
β π β π = π΅)) |
36 | 32, 35 | mpbid 231 |
. . . . . . 7
β’ (((π
β DivRing β§ π β π) β§ π β { 0 }) β π = π΅) |
37 | 36 | olcd 873 |
. . . . . 6
β’ (((π
β DivRing β§ π β π) β§ π β { 0 }) β (π = { 0 } β¨ π = π΅)) |
38 | 1, 37 | pm2.61dane 3029 |
. . . . 5
β’ ((π
β DivRing β§ π β π) β (π = { 0 } β¨ π = π΅)) |
39 | | vex 3448 |
. . . . . 6
β’ π β V |
40 | 39 | elpr 4610 |
. . . . 5
β’ (π β {{ 0 }, π΅} β (π = { 0 } β¨ π = π΅)) |
41 | 38, 40 | sylibr 233 |
. . . 4
β’ ((π
β DivRing β§ π β π) β π β {{ 0 }, π΅}) |
42 | 41 | ex 414 |
. . 3
β’ (π
β DivRing β (π β π β π β {{ 0 }, π΅})) |
43 | 42 | ssrdv 3951 |
. 2
β’ (π
β DivRing β π β {{ 0 }, π΅}) |
44 | 6, 7 | lidl0 20705 |
. . . 4
β’ (π
β Ring β { 0 } β
π) |
45 | 6, 11 | lidl1 20706 |
. . . 4
β’ (π
β Ring β π΅ β π) |
46 | 44, 45 | prssd 4783 |
. . 3
β’ (π
β Ring β {{ 0 }, π΅} β π) |
47 | 2, 46 | syl 17 |
. 2
β’ (π
β DivRing β {{ 0 }, π΅} β π) |
48 | 43, 47 | eqssd 3962 |
1
β’ (π
β DivRing β π = {{ 0 }, π΅}) |