![]() |
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 2733 | . . . . 5 ⊢ (Unit‘𝑅) = (Unit‘𝑅) | |
4 | drngui.z | . . . . 5 ⊢ 0 = (0g‘𝑅) | |
5 | 2, 3, 4 | isdrng 20312 | . . . 4 ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ (Unit‘𝑅) = (𝐵 ∖ { 0 }))) |
6 | 1, 5 | mpbi 229 | . . 3 ⊢ (𝑅 ∈ Ring ∧ (Unit‘𝑅) = (𝐵 ∖ { 0 })) |
7 | 6 | simpri 487 | . 2 ⊢ (Unit‘𝑅) = (𝐵 ∖ { 0 }) |
8 | 7 | eqcomi 2742 | 1 ⊢ (𝐵 ∖ { 0 }) = (Unit‘𝑅) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∖ cdif 3945 {csn 4628 ‘cfv 6541 Basecbs 17141 0gc0g 17382 Ringcrg 20050 Unitcui 20162 DivRingcdr 20308 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-iota 6493 df-fv 6549 df-drng 20310 |
This theorem is referenced by: cnflddiv 20968 cnfldinv 20969 cnsubdrglem 20989 cnmgpabl 20999 cnmsubglem 21001 gzrngunit 21004 zringunit 21028 expghm 21037 psgninv 21127 zrhpsgnmhm 21129 amgmlem 26484 dchrghm 26749 dchrabs 26753 sum2dchr 26767 lgseisenlem4 26871 qrngdiv 27117 proot1ex 41929 amgmwlem 47803 amgmlemALT 47804 |
Copyright terms: Public domain | W3C validator |