![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > drngui | Structured version Visualization version Unicode version |
Description: The set of units of a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
Ref | Expression |
---|---|
drngui.b |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
drngui.z |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
drngui.r |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
drngui |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | drngui.r |
. . . 4
![]() ![]() ![]() ![]() | |
2 | drngui.b |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | eqid 2450 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | drngui.z |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | isdrng 17972 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 5 | mpbi 212 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6 | simpri 464 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7 | eqcomi 2459 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ral 2741 df-rex 2742 df-rab 2745 df-v 3046 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-nul 3731 df-if 3881 df-sn 3968 df-pr 3970 df-op 3974 df-uni 4198 df-br 4402 df-iota 5545 df-fv 5589 df-drng 17970 |
This theorem is referenced by: cnflddiv 18991 cnfldinv 18992 cnsubdrglem 19012 cnmgpabl 19022 cnmsubglem 19023 gzrngunit 19026 zringunit 19055 expghm 19060 psgninv 19143 zrhpsgnmhm 19145 amgmlem 23908 dchrghm 24177 dchrabs 24181 sum2dchr 24195 lgseisenlem4 24273 qrngdiv 24455 proot1ex 36072 |
Copyright terms: Public domain | W3C validator |