Theorem unitcl 20344

Description: A unit is an element of the base set. (Contributed by Mario Carneiro, 1-Dec-2014.)

Hypotheses

Ref	Expression
unitcl.1	⊢ 𝐵 = (Base‘𝑅)
unitcl.2	⊢ 𝑈 = (Unit‘𝑅)

Assertion

Ref	Expression
unitcl	⊢ (𝑋 ∈ 𝑈 → 𝑋 ∈ 𝐵)

Proof of Theorem unitcl

Step	Hyp	Ref	Expression
1		unitcl.2	. . . 4 ⊢ 𝑈 = (Unit‘𝑅)
2		eqid 2734	. . . 4 ⊢ (1r‘𝑅) = (1r‘𝑅)
3		eqid 2734	. . . 4 ⊢ (∥r‘𝑅) = (∥r‘𝑅)
4		eqid 2734	. . . 4 ⊢ (oppr‘𝑅) = (oppr‘𝑅)
5		eqid 2734	. . . 4 ⊢ (∥r‘(oppr‘𝑅)) = (∥r‘(oppr‘𝑅))
6	1, 2, 3, 4, 5	isunit 20342	. . 3 ⊢ (𝑋 ∈ 𝑈 ↔ (𝑋(∥r‘𝑅)(1r‘𝑅) ∧ 𝑋(∥r‘(oppr‘𝑅))(1r‘𝑅)))
7	6	simplbi 497	. 2 ⊢ (𝑋 ∈ 𝑈 → 𝑋(∥r‘𝑅)(1r‘𝑅))
8		unitcl.1	. . 3 ⊢ 𝐵 = (Base‘𝑅)
9	8, 3	dvdsrcl 20334	. 2 ⊢ (𝑋(∥r‘𝑅)(1r‘𝑅) → 𝑋 ∈ 𝐵)
10	7, 9	syl 17	1 ⊢ (𝑋 ∈ 𝑈 → 𝑋 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107   class class class wbr 5123  ‘cfv 6541  Basecbs 17230  1_rcur 20147  opp_rcoppr 20302  ∥_rcdsr 20323  Unitcui 20324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5259  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6494  df-fun 6543  df-fv 6549  df-ov 7416  df-dvdsr 20326  df-unit 20327

This theorem is referenced by:  unitss  20345  unitmulcl  20349  unitgrp  20352  ringinvcl  20361  unitnegcl  20366  ringunitnzdiv  20367  unitdvcl  20374  dvrid  20375  dvrcan1  20378  dvrcan3  20379  dvreq1  20380  irredrmul  20396  subrguss  20556  subrginv  20557  subrgunit  20559  unitrrg  20672  isdrng2  20712  gzrngunitlem  21413  gzrngunit  21414  zringunit  21440  matinv  22632  cramerimp  22641  unitnmn0  24626  nminvr  24627  nrginvrcnlem  24649  ig1peu  26151  dchrelbas3  27219  dchrmulcl  27230  isdrng4  33242  kerunit  33294  dvdsruasso2  33354  unitmulrprm  33496  1arithidomlem1  33503  1arithidomlem2  33504  1arithidom  33505  ply1unit  33540  m1pmeq  33548  fldhmf1  42066  invginvrid  48256  lincresunit3lem3  48364  lincresunit3lem1  48369