![]() |
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 2795 | . . . . 5 ⊢ (Unit‘𝑅) = (Unit‘𝑅) | |
4 | drngui.z | . . . . 5 ⊢ 0 = (0g‘𝑅) | |
5 | 2, 3, 4 | isdrng 19196 | . . . 4 ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ (Unit‘𝑅) = (𝐵 ∖ { 0 }))) |
6 | 1, 5 | mpbi 231 | . . 3 ⊢ (𝑅 ∈ Ring ∧ (Unit‘𝑅) = (𝐵 ∖ { 0 })) |
7 | 6 | simpri 486 | . 2 ⊢ (Unit‘𝑅) = (𝐵 ∖ { 0 }) |
8 | 7 | eqcomi 2804 | 1 ⊢ (𝐵 ∖ { 0 }) = (Unit‘𝑅) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 396 = wceq 1522 ∈ wcel 2081 ∖ cdif 3856 {csn 4472 ‘cfv 6225 Basecbs 16312 0gc0g 16542 Ringcrg 18987 Unitcui 19079 DivRingcdr 19192 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-br 4963 df-iota 6189 df-fv 6233 df-drng 19194 |
This theorem is referenced by: cnflddiv 20257 cnfldinv 20258 cnsubdrglem 20278 cnmgpabl 20288 cnmsubglem 20290 gzrngunit 20293 zringunit 20317 expghm 20325 psgninv 20408 zrhpsgnmhm 20410 amgmlem 25249 dchrghm 25514 dchrabs 25518 sum2dchr 25532 lgseisenlem4 25636 qrngdiv 25882 proot1ex 39305 amgmwlem 44403 amgmlemALT 44404 |
Copyright terms: Public domain | W3C validator |