Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rngo1cl Structured version   Visualization version   GIF version

Theorem rngo1cl 35870
Description: The unit of a ring belongs to the base set. (Contributed by FL, 12-Feb-2010.) (New usage is discouraged.)
Hypotheses
Ref Expression
ring1cl.1 𝑋 = ran (1st𝑅)
ring1cl.2 𝐻 = (2nd𝑅)
ring1cl.3 𝑈 = (GId‘𝐻)
Assertion
Ref Expression
rngo1cl (𝑅 ∈ RingOps → 𝑈𝑋)

Proof of Theorem rngo1cl
StepHypRef Expression
1 ring1cl.2 . . . . . 6 𝐻 = (2nd𝑅)
21rngomndo 35866 . . . . 5 (𝑅 ∈ RingOps → 𝐻 ∈ MndOp)
31eleq1i 2830 . . . . . 6 (𝐻 ∈ MndOp ↔ (2nd𝑅) ∈ MndOp)
4 mndoismgmOLD 35801 . . . . . . 7 ((2nd𝑅) ∈ MndOp → (2nd𝑅) ∈ Magma)
5 mndoisexid 35800 . . . . . . 7 ((2nd𝑅) ∈ MndOp → (2nd𝑅) ∈ ExId )
64, 5jca 515 . . . . . 6 ((2nd𝑅) ∈ MndOp → ((2nd𝑅) ∈ Magma ∧ (2nd𝑅) ∈ ExId ))
73, 6sylbi 220 . . . . 5 (𝐻 ∈ MndOp → ((2nd𝑅) ∈ Magma ∧ (2nd𝑅) ∈ ExId ))
82, 7syl 17 . . . 4 (𝑅 ∈ RingOps → ((2nd𝑅) ∈ Magma ∧ (2nd𝑅) ∈ ExId ))
9 elin 3899 . . . 4 ((2nd𝑅) ∈ (Magma ∩ ExId ) ↔ ((2nd𝑅) ∈ Magma ∧ (2nd𝑅) ∈ ExId ))
108, 9sylibr 237 . . 3 (𝑅 ∈ RingOps → (2nd𝑅) ∈ (Magma ∩ ExId ))
11 eqid 2739 . . . 4 ran (2nd𝑅) = ran (2nd𝑅)
12 ring1cl.3 . . . . 5 𝑈 = (GId‘𝐻)
131fveq2i 6741 . . . . 5 (GId‘𝐻) = (GId‘(2nd𝑅))
1412, 13eqtri 2767 . . . 4 𝑈 = (GId‘(2nd𝑅))
1511, 14iorlid 35789 . . 3 ((2nd𝑅) ∈ (Magma ∩ ExId ) → 𝑈 ∈ ran (2nd𝑅))
1610, 15syl 17 . 2 (𝑅 ∈ RingOps → 𝑈 ∈ ran (2nd𝑅))
17 ring1cl.1 . . 3 𝑋 = ran (1st𝑅)
18 eqid 2739 . . . 4 (2nd𝑅) = (2nd𝑅)
19 eqid 2739 . . . 4 (1st𝑅) = (1st𝑅)
2018, 19rngorn1eq 35865 . . 3 (𝑅 ∈ RingOps → ran (1st𝑅) = ran (2nd𝑅))
21 eqtr 2762 . . . 4 ((𝑋 = ran (1st𝑅) ∧ ran (1st𝑅) = ran (2nd𝑅)) → 𝑋 = ran (2nd𝑅))
2221eleq2d 2825 . . 3 ((𝑋 = ran (1st𝑅) ∧ ran (1st𝑅) = ran (2nd𝑅)) → (𝑈𝑋𝑈 ∈ ran (2nd𝑅)))
2317, 20, 22sylancr 590 . 2 (𝑅 ∈ RingOps → (𝑈𝑋𝑈 ∈ ran (2nd𝑅)))
2416, 23mpbird 260 1 (𝑅 ∈ RingOps → 𝑈𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1543  wcel 2112  cin 3882  ran crn 5569  cfv 6400  1st c1st 7780  2nd c2nd 7781  GIdcgi 28602   ExId cexid 35775  Magmacmagm 35779  MndOpcmndo 35797  RingOpscrngo 35825
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5208  ax-nul 5215  ax-pr 5338  ax-un 7544
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4456  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4836  df-iun 4922  df-br 5070  df-opab 5132  df-mpt 5152  df-id 5471  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-fo 6406  df-fv 6408  df-riota 7191  df-ov 7237  df-1st 7782  df-2nd 7783  df-grpo 28605  df-gid 28606  df-ablo 28657  df-ass 35774  df-exid 35776  df-mgmOLD 35780  df-sgrOLD 35792  df-mndo 35798  df-rngo 35826
This theorem is referenced by:  rngoueqz  35871  rngonegmn1l  35872  rngonegmn1r  35873  rngoneglmul  35874  rngonegrmul  35875  isdrngo2  35889  rngohomco  35905  rngoisocnv  35912  idlnegcl  35953  1idl  35957  0rngo  35958  smprngopr  35983  prnc  35998  isfldidl  35999  isdmn3  36005
  Copyright terms: Public domain W3C validator