Theorem unitcl 20392

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 2752	. . . 4 ⊢ (1r‘𝑅) = (1r‘𝑅)
3		eqid 2752	. . . 4 ⊢ (∥r‘𝑅) = (∥r‘𝑅)
4		eqid 2752	. . . 4 ⊢ (oppr‘𝑅) = (oppr‘𝑅)
5		eqid 2752	. . . 4 ⊢ (∥r‘(oppr‘𝑅)) = (∥r‘(oppr‘𝑅))
6	1, 2, 3, 4, 5	isunit 20390	. . 3 ⊢ (𝑋 ∈ 𝑈 ↔ (𝑋(∥r‘𝑅)(1r‘𝑅) ∧ 𝑋(∥r‘(oppr‘𝑅))(1r‘𝑅)))
7	6	simplbi 499	. 2 ⊢ (𝑋 ∈ 𝑈 → 𝑋(∥r‘𝑅)(1r‘𝑅))
8		unitcl.1	. . 3 ⊢ 𝐵 = (Base‘𝑅)
9	8, 3	dvdsrcl 20382	. 2 ⊢ (𝑋(∥r‘𝑅)(1r‘𝑅) → 𝑋 ∈ 𝐵)
10	7, 9	syl 17	1 ⊢ (𝑋 ∈ 𝑈 → 𝑋 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1550   ∈ wcel 2132   class class class wbr 5090  ‘cfv 6506  Basecbs 17217  1_rcur 20199  opp_rcoppr 20353  ∥_rcdsr 20371  Unitcui 20372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-rep 5217  ax-sep 5236  ax-nul 5246  ax-pow 5312  ax-pr 5380  ax-un 7703

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-sbc 3736  df-csb 3844  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-iun 4941  df-br 5091  df-opab 5153  df-mpt 5172  df-id 5531  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-iota 6462  df-fun 6508  df-fv 6514  df-ov 7384  df-dvdsr 20374  df-unit 20375

This theorem is referenced by:  unitss  20393  unitmulcl  20397  unitgrp  20400  ringinvcl  20409  unitnegcl  20414  ringunitnzdiv  20415  unitdvcl  20422  dvrid  20423  dvrcan1  20426  dvrcan3  20427  dvreq1  20428  irredrmul  20444  subrguss  20605  subrginv  20606  subrgunit  20608  unitrrg  20721  isdrng2  20761  gzrngunitlem  21453  gzrngunit  21454  zringunit  21487  matinv  22706  cramerimp  22715  unitnmn0  24697  nminvr  24698  nrginvrcnlem  24720  ig1peu  26204  dchrelbas3  27268  dchrmulcl  27279  isdrng4  33428  kerunit  33457  dvdsruasso2  33518  unitmulrprm  33668  1arithidomlem1  33675  1arithidomlem2  33676  1arithidom  33677  ply1unit  33715  m1pmeq  33725  fldhmf1  42645  invginvrid  48927  lincresunit3lem3  49034  lincresunit3lem1  49039