![]() |
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 19241 | . . . 4 ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 }))) |
5 | 4 | simprbi 489 | . . 3 ⊢ (𝑅 ∈ DivRing → 𝑈 = (𝐵 ∖ { 0 })) |
6 | 5 | eleq2d 2845 | . 2 ⊢ (𝑅 ∈ DivRing → (𝑋 ∈ 𝑈 ↔ 𝑋 ∈ (𝐵 ∖ { 0 }))) |
7 | eldifsn 4589 | . 2 ⊢ (𝑋 ∈ (𝐵 ∖ { 0 }) ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 )) | |
8 | 6, 7 | syl6bb 279 | 1 ⊢ (𝑅 ∈ DivRing → (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 = wceq 1507 ∈ wcel 2050 ≠ wne 2961 ∖ cdif 3820 {csn 4435 ‘cfv 6185 Basecbs 16337 0gc0g 16567 Ringcrg 19032 Unitcui 19124 DivRingcdr 19237 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2744 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-ral 3087 df-rex 3088 df-rab 3091 df-v 3411 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-nul 4173 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4709 df-br 4926 df-iota 6149 df-fv 6193 df-drng 19239 |
This theorem is referenced by: drngunz 19252 drnginvrcl 19254 drnginvrn0 19255 drnginvrl 19256 drnginvrr 19257 issubdrg 19295 abvdiv 19342 qsssubdrg 20318 redvr 20475 drnguc1p 24479 lgseisenlem3 25667 ornglmullt 30588 orngrmullt 30589 isarchiofld 30598 qqhval2lem 30895 qqhf 30900 matunitlindf 34360 lincreslvec3 43929 isldepslvec2 43932 |
Copyright terms: Public domain | W3C validator |