MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isunit Structured version   Visualization version   GIF version

Theorem isunit 19055
Description: Property of being a unit of a ring. A unit is an element that left- and right-divides one. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 8-Dec-2015.)
Hypotheses
Ref Expression
unit.1 𝑈 = (Unit‘𝑅)
unit.2 1 = (1r𝑅)
unit.3 = (∥r𝑅)
unit.4 𝑆 = (oppr𝑅)
unit.5 𝐸 = (∥r𝑆)
Assertion
Ref Expression
isunit (𝑋𝑈 ↔ (𝑋 1𝑋𝐸 1 ))

Proof of Theorem isunit
Dummy variable 𝑟 is distinct from all other variables.
StepHypRef Expression
1 elfvdm 6480 . . . 4 (𝑋 ∈ (Unit‘𝑅) → 𝑅 ∈ dom Unit)
2 unit.1 . . . 4 𝑈 = (Unit‘𝑅)
31, 2eleq2s 2877 . . 3 (𝑋𝑈𝑅 ∈ dom Unit)
43elexd 3416 . 2 (𝑋𝑈𝑅 ∈ V)
5 df-br 4889 . . . 4 (𝑋 1 ↔ ⟨𝑋, 1 ⟩ ∈ )
6 elfvdm 6480 . . . . . 6 (⟨𝑋, 1 ⟩ ∈ (∥r𝑅) → 𝑅 ∈ dom ∥r)
7 unit.3 . . . . . 6 = (∥r𝑅)
86, 7eleq2s 2877 . . . . 5 (⟨𝑋, 1 ⟩ ∈ 𝑅 ∈ dom ∥r)
98elexd 3416 . . . 4 (⟨𝑋, 1 ⟩ ∈ 𝑅 ∈ V)
105, 9sylbi 209 . . 3 (𝑋 1𝑅 ∈ V)
1110adantr 474 . 2 ((𝑋 1𝑋𝐸 1 ) → 𝑅 ∈ V)
12 fveq2 6448 . . . . . . . . . 10 (𝑟 = 𝑅 → (∥r𝑟) = (∥r𝑅))
1312, 7syl6eqr 2832 . . . . . . . . 9 (𝑟 = 𝑅 → (∥r𝑟) = )
14 fveq2 6448 . . . . . . . . . . . 12 (𝑟 = 𝑅 → (oppr𝑟) = (oppr𝑅))
15 unit.4 . . . . . . . . . . . 12 𝑆 = (oppr𝑅)
1614, 15syl6eqr 2832 . . . . . . . . . . 11 (𝑟 = 𝑅 → (oppr𝑟) = 𝑆)
1716fveq2d 6452 . . . . . . . . . 10 (𝑟 = 𝑅 → (∥r‘(oppr𝑟)) = (∥r𝑆))
18 unit.5 . . . . . . . . . 10 𝐸 = (∥r𝑆)
1917, 18syl6eqr 2832 . . . . . . . . 9 (𝑟 = 𝑅 → (∥r‘(oppr𝑟)) = 𝐸)
2013, 19ineq12d 4038 . . . . . . . 8 (𝑟 = 𝑅 → ((∥r𝑟) ∩ (∥r‘(oppr𝑟))) = ( 𝐸))
2120cnveqd 5545 . . . . . . 7 (𝑟 = 𝑅((∥r𝑟) ∩ (∥r‘(oppr𝑟))) = ( 𝐸))
22 fveq2 6448 . . . . . . . . 9 (𝑟 = 𝑅 → (1r𝑟) = (1r𝑅))
23 unit.2 . . . . . . . . 9 1 = (1r𝑅)
2422, 23syl6eqr 2832 . . . . . . . 8 (𝑟 = 𝑅 → (1r𝑟) = 1 )
2524sneqd 4410 . . . . . . 7 (𝑟 = 𝑅 → {(1r𝑟)} = { 1 })
2621, 25imaeq12d 5723 . . . . . 6 (𝑟 = 𝑅 → (((∥r𝑟) ∩ (∥r‘(oppr𝑟))) “ {(1r𝑟)}) = (( 𝐸) “ { 1 }))
27 df-unit 19040 . . . . . 6 Unit = (𝑟 ∈ V ↦ (((∥r𝑟) ∩ (∥r‘(oppr𝑟))) “ {(1r𝑟)}))
287fvexi 6462 . . . . . . . . 9 ∈ V
2928inex1 5038 . . . . . . . 8 ( 𝐸) ∈ V
3029cnvex 7394 . . . . . . 7 ( 𝐸) ∈ V
3130imaex 7385 . . . . . 6 (( 𝐸) “ { 1 }) ∈ V
3226, 27, 31fvmpt 6544 . . . . 5 (𝑅 ∈ V → (Unit‘𝑅) = (( 𝐸) “ { 1 }))
332, 32syl5eq 2826 . . . 4 (𝑅 ∈ V → 𝑈 = (( 𝐸) “ { 1 }))
3433eleq2d 2845 . . 3 (𝑅 ∈ V → (𝑋𝑈𝑋 ∈ (( 𝐸) “ { 1 })))
35 inss1 4053 . . . . . 6 ( 𝐸) ⊆
367reldvdsr 19042 . . . . . 6 Rel
37 relss 5456 . . . . . 6 (( 𝐸) ⊆ → (Rel → Rel ( 𝐸)))
3835, 36, 37mp2 9 . . . . 5 Rel ( 𝐸)
39 eliniseg2 5761 . . . . 5 (Rel ( 𝐸) → (𝑋 ∈ (( 𝐸) “ { 1 }) ↔ 𝑋( 𝐸) 1 ))
4038, 39ax-mp 5 . . . 4 (𝑋 ∈ (( 𝐸) “ { 1 }) ↔ 𝑋( 𝐸) 1 )
41 brin 4940 . . . 4 (𝑋( 𝐸) 1 ↔ (𝑋 1𝑋𝐸 1 ))
4240, 41bitri 267 . . 3 (𝑋 ∈ (( 𝐸) “ { 1 }) ↔ (𝑋 1𝑋𝐸 1 ))
4334, 42syl6bb 279 . 2 (𝑅 ∈ V → (𝑋𝑈 ↔ (𝑋 1𝑋𝐸 1 )))
444, 11, 43pm5.21nii 370 1 (𝑋𝑈 ↔ (𝑋 1𝑋𝐸 1 ))
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 386   = wceq 1601  wcel 2107  Vcvv 3398  cin 3791  wss 3792  {csn 4398  cop 4404   class class class wbr 4888  ccnv 5356  dom cdm 5357  cima 5360  Rel wrel 5362  cfv 6137  1rcur 18899  opprcoppr 19020  rcdsr 19036  Unitcui 19037
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-mpt 4968  df-id 5263  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-iota 6101  df-fun 6139  df-fv 6145  df-dvdsr 19039  df-unit 19040
This theorem is referenced by:  1unit  19056  unitcl  19057  opprunit  19059  crngunit  19060  unitmulcl  19062  unitgrp  19065  unitnegcl  19079  unitpropd  19095  isdrng2  19160  subrguss  19198  subrgunit  19201  fidomndrng  19715  invrvald  20899  elrhmunit  30390
  Copyright terms: Public domain W3C validator