![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > drngunit | Structured version Visualization version GIF version |
Description: Elementhood in the set of units when π is a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
Ref | Expression |
---|---|
isdrng.b | β’ π΅ = (Baseβπ ) |
isdrng.u | β’ π = (Unitβπ ) |
isdrng.z | β’ 0 = (0gβπ ) |
Ref | Expression |
---|---|
drngunit | β’ (π β DivRing β (π β π β (π β π΅ β§ π β 0 ))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isdrng.b | . . . . 5 β’ π΅ = (Baseβπ ) | |
2 | isdrng.u | . . . . 5 β’ π = (Unitβπ ) | |
3 | isdrng.z | . . . . 5 β’ 0 = (0gβπ ) | |
4 | 1, 2, 3 | isdrng 20504 | . . . 4 β’ (π β DivRing β (π β Ring β§ π = (π΅ β { 0 }))) |
5 | 4 | simprbi 495 | . . 3 β’ (π β DivRing β π = (π΅ β { 0 })) |
6 | 5 | eleq2d 2817 | . 2 β’ (π β DivRing β (π β π β π β (π΅ β { 0 }))) |
7 | eldifsn 4789 | . 2 β’ (π β (π΅ β { 0 }) β (π β π΅ β§ π β 0 )) | |
8 | 6, 7 | bitrdi 286 | 1 β’ (π β DivRing β (π β π β (π β π΅ β§ π β 0 ))) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β wb 205 β§ wa 394 = wceq 1539 β wcel 2104 β wne 2938 β cdif 3944 {csn 4627 βcfv 6542 Basecbs 17148 0gc0g 17389 Ringcrg 20127 Unitcui 20246 DivRingcdr 20500 |
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-ne 2939 df-rab 3431 df-v 3474 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-iota 6494 df-fv 6550 df-drng 20502 |
This theorem is referenced by: drngunz 20519 drnginvrcl 20522 drnginvrn0 20523 drnginvrl 20525 drnginvrr 20526 issubdrg 20544 sdrgunit 20555 abvdiv 20588 qsssubdrg 21204 redvr 21389 drnguc1p 25923 lgseisenlem3 27116 sdrgdvcl 32667 sdrginvcl 32668 ornglmullt 32695 orngrmullt 32696 isarchiofld 32705 ply1asclunit 32928 qqhval2lem 33259 qqhf 33264 matunitlindf 36789 fldhmf1 41261 lincreslvec3 47250 isldepslvec2 47253 |
Copyright terms: Public domain | W3C validator |