Theorem unitcl 20464

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2142   class class class wbr 5108  ‘cfv 6536  Basecbs 17275  1_rcur 20269  opp_rcoppr 20425  ∥_rcdsr 20443  Unitcui 20444

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5237  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5555  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-iota 6492  df-fun 6538  df-fv 6544  df-ov 7415  df-dvdsr 20446  df-unit 20447

This theorem is used by:  unitss  20465  unitmulcl  20469  unitgrp  20472  ringinvcl  20481  unitnegcl  20486  ringunitnzdiv  20487  unitdvcl  20494  dvrid  20495  dvrcan1  20498  dvrcan3  20499  dvreq1  20500  irredrmul  20516  subrguss  20697  subrginv  20698  subrgunit  20700  unitrrg  20813  isdrng4  20850  isdrng2  20854  gzrngunitlem  21593  gzrngunit  21594  zringunit  21627  matinv  22845  cramerimp  22854  unitnmn0  24836  nminvr  24837  nrginvrcnlem  24859  ig1peu  26343  dchrelbas3  27413  dchrmulcl  27424  kerunit  33654  dvdsruasso2  33708  unitmulrprm  33827  1arithidomlem1  33834  1arithidomlem2  33835  1arithidom  33836  ply1unit  33874  m1pmeq  33884  fldhmf1  42885  invginvrid  49175  lincresunit3lem3  49282  lincresunit3lem1  49287