ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  isunitd GIF version

Theorem isunitd 13281
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
isunitd.1 (𝜑𝑈 = (Unit‘𝑅))
isunitd.2 (𝜑1 = (1r𝑅))
isunitd.3 (𝜑 = (∥r𝑅))
isunitd.4 (𝜑𝑆 = (oppr𝑅))
isunitd.5 (𝜑𝐸 = (∥r𝑆))
isunitd.r (𝜑𝑅 ∈ SRing)
Assertion
Ref Expression
isunitd (𝜑 → (𝑋𝑈 ↔ (𝑋 1𝑋𝐸 1 )))

Proof of Theorem isunitd
Dummy variable 𝑟 is distinct from all other variables.
StepHypRef Expression
1 isunitd.1 . . . 4 (𝜑𝑈 = (Unit‘𝑅))
2 df-unit 13265 . . . . 5 Unit = (𝑟 ∈ V ↦ (((∥r𝑟) ∩ (∥r‘(oppr𝑟))) “ {(1r𝑟)}))
3 fveq2 5517 . . . . . . . 8 (𝑟 = 𝑅 → (∥r𝑟) = (∥r𝑅))
4 2fveq3 5522 . . . . . . . 8 (𝑟 = 𝑅 → (∥r‘(oppr𝑟)) = (∥r‘(oppr𝑅)))
53, 4ineq12d 3339 . . . . . . 7 (𝑟 = 𝑅 → ((∥r𝑟) ∩ (∥r‘(oppr𝑟))) = ((∥r𝑅) ∩ (∥r‘(oppr𝑅))))
65cnveqd 4805 . . . . . 6 (𝑟 = 𝑅((∥r𝑟) ∩ (∥r‘(oppr𝑟))) = ((∥r𝑅) ∩ (∥r‘(oppr𝑅))))
7 fveq2 5517 . . . . . . 7 (𝑟 = 𝑅 → (1r𝑟) = (1r𝑅))
87sneqd 3607 . . . . . 6 (𝑟 = 𝑅 → {(1r𝑟)} = {(1r𝑅)})
96, 8imaeq12d 4973 . . . . 5 (𝑟 = 𝑅 → (((∥r𝑟) ∩ (∥r‘(oppr𝑟))) “ {(1r𝑟)}) = (((∥r𝑅) ∩ (∥r‘(oppr𝑅))) “ {(1r𝑅)}))
10 isunitd.r . . . . . 6 (𝜑𝑅 ∈ SRing)
1110elexd 2752 . . . . 5 (𝜑𝑅 ∈ V)
12 dvdsrex 13273 . . . . . . 7 (𝑅 ∈ SRing → (∥r𝑅) ∈ V)
13 inex1g 4141 . . . . . . 7 ((∥r𝑅) ∈ V → ((∥r𝑅) ∩ (∥r‘(oppr𝑅))) ∈ V)
1410, 12, 133syl 17 . . . . . 6 (𝜑 → ((∥r𝑅) ∩ (∥r‘(oppr𝑅))) ∈ V)
15 cnvexg 5168 . . . . . 6 (((∥r𝑅) ∩ (∥r‘(oppr𝑅))) ∈ V → ((∥r𝑅) ∩ (∥r‘(oppr𝑅))) ∈ V)
16 imaexg 4984 . . . . . 6 (((∥r𝑅) ∩ (∥r‘(oppr𝑅))) ∈ V → (((∥r𝑅) ∩ (∥r‘(oppr𝑅))) “ {(1r𝑅)}) ∈ V)
1714, 15, 163syl 17 . . . . 5 (𝜑 → (((∥r𝑅) ∩ (∥r‘(oppr𝑅))) “ {(1r𝑅)}) ∈ V)
182, 9, 11, 17fvmptd3 5612 . . . 4 (𝜑 → (Unit‘𝑅) = (((∥r𝑅) ∩ (∥r‘(oppr𝑅))) “ {(1r𝑅)}))
191, 18eqtrd 2210 . . 3 (𝜑𝑈 = (((∥r𝑅) ∩ (∥r‘(oppr𝑅))) “ {(1r𝑅)}))
2019eleq2d 2247 . 2 (𝜑 → (𝑋𝑈𝑋 ∈ (((∥r𝑅) ∩ (∥r‘(oppr𝑅))) “ {(1r𝑅)})))
21 isunitd.3 . . . . . 6 (𝜑 = (∥r𝑅))
22 isunitd.5 . . . . . . 7 (𝜑𝐸 = (∥r𝑆))
23 isunitd.4 . . . . . . . 8 (𝜑𝑆 = (oppr𝑅))
2423fveq2d 5521 . . . . . . 7 (𝜑 → (∥r𝑆) = (∥r‘(oppr𝑅)))
2522, 24eqtrd 2210 . . . . . 6 (𝜑𝐸 = (∥r‘(oppr𝑅)))
2621, 25ineq12d 3339 . . . . 5 (𝜑 → ( 𝐸) = ((∥r𝑅) ∩ (∥r‘(oppr𝑅))))
2726cnveqd 4805 . . . 4 (𝜑( 𝐸) = ((∥r𝑅) ∩ (∥r‘(oppr𝑅))))
28 isunitd.2 . . . . 5 (𝜑1 = (1r𝑅))
2928sneqd 3607 . . . 4 (𝜑 → { 1 } = {(1r𝑅)})
3027, 29imaeq12d 4973 . . 3 (𝜑 → (( 𝐸) “ { 1 }) = (((∥r𝑅) ∩ (∥r‘(oppr𝑅))) “ {(1r𝑅)}))
3130eleq2d 2247 . 2 (𝜑 → (𝑋 ∈ (( 𝐸) “ { 1 }) ↔ 𝑋 ∈ (((∥r𝑅) ∩ (∥r‘(oppr𝑅))) “ {(1r𝑅)})))
32 reldvdsrsrg 13267 . . . . . 6 (𝑅 ∈ SRing → Rel (∥r𝑅))
3310, 32syl 14 . . . . 5 (𝜑 → Rel (∥r𝑅))
3421releqd 4712 . . . . 5 (𝜑 → (Rel ↔ Rel (∥r𝑅)))
3533, 34mpbird 167 . . . 4 (𝜑 → Rel )
36 relin1 4746 . . . 4 (Rel → Rel ( 𝐸))
37 eliniseg2 5010 . . . 4 (Rel ( 𝐸) → (𝑋 ∈ (( 𝐸) “ { 1 }) ↔ 𝑋( 𝐸) 1 ))
3835, 36, 373syl 17 . . 3 (𝜑 → (𝑋 ∈ (( 𝐸) “ { 1 }) ↔ 𝑋( 𝐸) 1 ))
39 brin 4057 . . 3 (𝑋( 𝐸) 1 ↔ (𝑋 1𝑋𝐸 1 ))
4038, 39bitrdi 196 . 2 (𝜑 → (𝑋 ∈ (( 𝐸) “ { 1 }) ↔ (𝑋 1𝑋𝐸 1 )))
4120, 31, 403bitr2d 216 1 (𝜑 → (𝑋𝑈 ↔ (𝑋 1𝑋𝐸 1 )))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1353  wcel 2148  Vcvv 2739  cin 3130  {csn 3594   class class class wbr 4005  ccnv 4627  cima 4631  Rel wrel 4633  cfv 5218  1rcur 13148  SRingcsrg 13152  opprcoppr 13245  rcdsr 13261  Unitcui 13262
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-cnex 7905  ax-resscn 7906  ax-1cn 7907  ax-1re 7908  ax-icn 7909  ax-addcl 7910  ax-addrcl 7911  ax-mulcl 7912  ax-addcom 7914  ax-addass 7916  ax-i2m1 7919  ax-0lt1 7920  ax-0id 7922  ax-rnegex 7923  ax-pre-ltirr 7926  ax-pre-ltadd 7930
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-fv 5226  df-riota 5834  df-ov 5881  df-oprab 5882  df-mpo 5883  df-pnf 7997  df-mnf 7998  df-ltxr 8000  df-inn 8923  df-2 8981  df-3 8982  df-ndx 12468  df-slot 12469  df-base 12471  df-sets 12472  df-plusg 12552  df-mulr 12553  df-0g 12713  df-mgm 12781  df-sgrp 12814  df-mnd 12824  df-mgp 13137  df-srg 13153  df-dvdsr 13264  df-unit 13265
This theorem is referenced by:  1unit  13282  unitcld  13283  opprunitd  13285  crngunit  13286  unitmulcl  13288  unitgrp  13291  unitnegcl  13305  unitpropdg  13323  subrguss  13363  subrgunit  13366
  Copyright terms: Public domain W3C validator