![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > drngui | Structured version Visualization version GIF version |
Description: The set of units of a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
Ref | Expression |
---|---|
drngui.b | β’ π΅ = (Baseβπ ) |
drngui.z | β’ 0 = (0gβπ ) |
drngui.r | β’ π β DivRing |
Ref | Expression |
---|---|
drngui | β’ (π΅ β { 0 }) = (Unitβπ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | drngui.r | . . . 4 β’ π β DivRing | |
2 | drngui.b | . . . . 5 β’ π΅ = (Baseβπ ) | |
3 | eqid 2730 | . . . . 5 β’ (Unitβπ ) = (Unitβπ ) | |
4 | drngui.z | . . . . 5 β’ 0 = (0gβπ ) | |
5 | 2, 3, 4 | isdrng 20506 | . . . 4 β’ (π β DivRing β (π β Ring β§ (Unitβπ ) = (π΅ β { 0 }))) |
6 | 1, 5 | mpbi 229 | . . 3 β’ (π β Ring β§ (Unitβπ ) = (π΅ β { 0 })) |
7 | 6 | simpri 484 | . 2 β’ (Unitβπ ) = (π΅ β { 0 }) |
8 | 7 | eqcomi 2739 | 1 β’ (π΅ β { 0 }) = (Unitβπ ) |
Colors of variables: wff setvar class |
Syntax hints: β§ wa 394 = wceq 1539 β wcel 2104 β cdif 3946 {csn 4629 βcfv 6544 Basecbs 17150 0gc0g 17391 Ringcrg 20129 Unitcui 20248 DivRingcdr 20502 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-ext 2701 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-rab 3431 df-v 3474 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-iota 6496 df-fv 6552 df-drng 20504 |
This theorem is referenced by: cnflddiv 21177 cnfldinv 21178 cnsubdrglem 21198 cnmgpabl 21208 cnmsubglem 21210 gzrngunit 21213 zringunit 21239 expghm 21248 psgninv 21356 zrhpsgnmhm 21358 amgmlem 26728 dchrghm 26993 dchrabs 26997 sum2dchr 27011 lgseisenlem4 27115 qrngdiv 27361 proot1ex 42247 amgmwlem 47938 amgmlemALT 47939 |
Copyright terms: Public domain | W3C validator |