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

Theorem isunit 20324
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 6933 . . . 4 (𝑋 ∈ (Unit‘𝑅) → 𝑅 ∈ dom Unit)
2 unit.1 . . . 4 𝑈 = (Unit‘𝑅)
31, 2eleq2s 2843 . . 3 (𝑋𝑈𝑅 ∈ dom Unit)
43elexd 3483 . 2 (𝑋𝑈𝑅 ∈ V)
5 df-br 5150 . . . 4 (𝑋 1 ↔ ⟨𝑋, 1 ⟩ ∈ )
6 elfvdm 6933 . . . . . 6 (⟨𝑋, 1 ⟩ ∈ (∥r𝑅) → 𝑅 ∈ dom ∥r)
7 unit.3 . . . . . 6 = (∥r𝑅)
86, 7eleq2s 2843 . . . . 5 (⟨𝑋, 1 ⟩ ∈ 𝑅 ∈ dom ∥r)
98elexd 3483 . . . 4 (⟨𝑋, 1 ⟩ ∈ 𝑅 ∈ V)
105, 9sylbi 216 . . 3 (𝑋 1𝑅 ∈ V)
1110adantr 479 . 2 ((𝑋 1𝑋𝐸 1 ) → 𝑅 ∈ V)
12 fveq2 6896 . . . . . . . . . 10 (𝑟 = 𝑅 → (∥r𝑟) = (∥r𝑅))
1312, 7eqtr4di 2783 . . . . . . . . 9 (𝑟 = 𝑅 → (∥r𝑟) = )
14 fveq2 6896 . . . . . . . . . . . 12 (𝑟 = 𝑅 → (oppr𝑟) = (oppr𝑅))
15 unit.4 . . . . . . . . . . . 12 𝑆 = (oppr𝑅)
1614, 15eqtr4di 2783 . . . . . . . . . . 11 (𝑟 = 𝑅 → (oppr𝑟) = 𝑆)
1716fveq2d 6900 . . . . . . . . . 10 (𝑟 = 𝑅 → (∥r‘(oppr𝑟)) = (∥r𝑆))
18 unit.5 . . . . . . . . . 10 𝐸 = (∥r𝑆)
1917, 18eqtr4di 2783 . . . . . . . . 9 (𝑟 = 𝑅 → (∥r‘(oppr𝑟)) = 𝐸)
2013, 19ineq12d 4211 . . . . . . . 8 (𝑟 = 𝑅 → ((∥r𝑟) ∩ (∥r‘(oppr𝑟))) = ( 𝐸))
2120cnveqd 5878 . . . . . . 7 (𝑟 = 𝑅((∥r𝑟) ∩ (∥r‘(oppr𝑟))) = ( 𝐸))
22 fveq2 6896 . . . . . . . . 9 (𝑟 = 𝑅 → (1r𝑟) = (1r𝑅))
23 unit.2 . . . . . . . . 9 1 = (1r𝑅)
2422, 23eqtr4di 2783 . . . . . . . 8 (𝑟 = 𝑅 → (1r𝑟) = 1 )
2524sneqd 4642 . . . . . . 7 (𝑟 = 𝑅 → {(1r𝑟)} = { 1 })
2621, 25imaeq12d 6065 . . . . . 6 (𝑟 = 𝑅 → (((∥r𝑟) ∩ (∥r‘(oppr𝑟))) “ {(1r𝑟)}) = (( 𝐸) “ { 1 }))
27 df-unit 20309 . . . . . 6 Unit = (𝑟 ∈ V ↦ (((∥r𝑟) ∩ (∥r‘(oppr𝑟))) “ {(1r𝑟)}))
287fvexi 6910 . . . . . . . . 9 ∈ V
2928inex1 5318 . . . . . . . 8 ( 𝐸) ∈ V
3029cnvex 7933 . . . . . . 7 ( 𝐸) ∈ V
3130imaex 7922 . . . . . 6 (( 𝐸) “ { 1 }) ∈ V
3226, 27, 31fvmpt 7004 . . . . 5 (𝑅 ∈ V → (Unit‘𝑅) = (( 𝐸) “ { 1 }))
332, 32eqtrid 2777 . . . 4 (𝑅 ∈ V → 𝑈 = (( 𝐸) “ { 1 }))
3433eleq2d 2811 . . 3 (𝑅 ∈ V → (𝑋𝑈𝑋 ∈ (( 𝐸) “ { 1 })))
35 inss1 4227 . . . . . 6 ( 𝐸) ⊆
367reldvdsr 20311 . . . . . 6 Rel
37 relss 5783 . . . . . 6 (( 𝐸) ⊆ → (Rel → Rel ( 𝐸)))
3835, 36, 37mp2 9 . . . . 5 Rel ( 𝐸)
39 eliniseg2 6111 . . . . 5 (Rel ( 𝐸) → (𝑋 ∈ (( 𝐸) “ { 1 }) ↔ 𝑋( 𝐸) 1 ))
4038, 39ax-mp 5 . . . 4 (𝑋 ∈ (( 𝐸) “ { 1 }) ↔ 𝑋( 𝐸) 1 )
41 brin 5201 . . . 4 (𝑋( 𝐸) 1 ↔ (𝑋 1𝑋𝐸 1 ))
4240, 41bitri 274 . . 3 (𝑋 ∈ (( 𝐸) “ { 1 }) ↔ (𝑋 1𝑋𝐸 1 ))
4334, 42bitrdi 286 . 2 (𝑅 ∈ V → (𝑋𝑈 ↔ (𝑋 1𝑋𝐸 1 )))
444, 11, 43pm5.21nii 377 1 (𝑋𝑈 ↔ (𝑋 1𝑋𝐸 1 ))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394   = wceq 1533  wcel 2098  Vcvv 3461  cin 3943  wss 3944  {csn 4630  cop 4636   class class class wbr 5149  ccnv 5677  dom cdm 5678  cima 5681  Rel wrel 5683  cfv 6549  1rcur 20133  opprcoppr 20284  rcdsr 20305  Unitcui 20306
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fv 6557  df-dvdsr 20308  df-unit 20309
This theorem is referenced by:  1unit  20325  unitcl  20326  opprunit  20328  crngunit  20329  unitmulcl  20331  unitgrp  20334  unitnegcl  20348  unitpropd  20368  elrhmunit  20461  subrguss  20538  subrgunit  20541  isdrng2  20650  fidomndrng  21278  invrvald  22622  isdrng4  33083
  Copyright terms: Public domain W3C validator