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 34047
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 34043 . . . . 5 (𝑅 ∈ RingOps → 𝐻 ∈ MndOp)
31eleq1i 2826 . . . . . 6 (𝐻 ∈ MndOp ↔ (2nd𝑅) ∈ MndOp)
4 mndoismgmOLD 33978 . . . . . . 7 ((2nd𝑅) ∈ MndOp → (2nd𝑅) ∈ Magma)
5 mndoisexid 33977 . . . . . . 7 ((2nd𝑅) ∈ MndOp → (2nd𝑅) ∈ ExId )
64, 5jca 555 . . . . . 6 ((2nd𝑅) ∈ MndOp → ((2nd𝑅) ∈ Magma ∧ (2nd𝑅) ∈ ExId ))
73, 6sylbi 207 . . . . 5 (𝐻 ∈ MndOp → ((2nd𝑅) ∈ Magma ∧ (2nd𝑅) ∈ ExId ))
82, 7syl 17 . . . 4 (𝑅 ∈ RingOps → ((2nd𝑅) ∈ Magma ∧ (2nd𝑅) ∈ ExId ))
9 elin 3935 . . . 4 ((2nd𝑅) ∈ (Magma ∩ ExId ) ↔ ((2nd𝑅) ∈ Magma ∧ (2nd𝑅) ∈ ExId ))
108, 9sylibr 224 . . 3 (𝑅 ∈ RingOps → (2nd𝑅) ∈ (Magma ∩ ExId ))
11 eqid 2756 . . . 4 ran (2nd𝑅) = ran (2nd𝑅)
12 ring1cl.3 . . . . 5 𝑈 = (GId‘𝐻)
131fveq2i 6351 . . . . 5 (GId‘𝐻) = (GId‘(2nd𝑅))
1412, 13eqtri 2778 . . . 4 𝑈 = (GId‘(2nd𝑅))
1511, 14iorlid 33966 . . 3 ((2nd𝑅) ∈ (Magma ∩ ExId ) → 𝑈 ∈ ran (2nd𝑅))
1610, 15syl 17 . 2 (𝑅 ∈ RingOps → 𝑈 ∈ ran (2nd𝑅))
17 ring1cl.1 . . 3 𝑋 = ran (1st𝑅)
18 eqid 2756 . . . 4 (2nd𝑅) = (2nd𝑅)
19 eqid 2756 . . . 4 (1st𝑅) = (1st𝑅)
2018, 19rngorn1eq 34042 . . 3 (𝑅 ∈ RingOps → ran (1st𝑅) = ran (2nd𝑅))
21 eqtr 2775 . . . 4 ((𝑋 = ran (1st𝑅) ∧ ran (1st𝑅) = ran (2nd𝑅)) → 𝑋 = ran (2nd𝑅))
2221eleq2d 2821 . . 3 ((𝑋 = ran (1st𝑅) ∧ ran (1st𝑅) = ran (2nd𝑅)) → (𝑈𝑋𝑈 ∈ ran (2nd𝑅)))
2317, 20, 22sylancr 698 . 2 (𝑅 ∈ RingOps → (𝑈𝑋𝑈 ∈ ran (2nd𝑅)))
2416, 23mpbird 247 1 (𝑅 ∈ RingOps → 𝑈𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1628  wcel 2135  cin 3710  ran crn 5263  cfv 6045  1st c1st 7327  2nd c2nd 7328  GIdcgi 27649   ExId cexid 33952  Magmacmagm 33956  MndOpcmndo 33974  RingOpscrngo 34002
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-reu 3053  df-rmo 3054  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-nul 4055  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4585  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-id 5170  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-fo 6051  df-fv 6053  df-riota 6770  df-ov 6812  df-1st 7329  df-2nd 7330  df-grpo 27652  df-gid 27653  df-ablo 27704  df-ass 33951  df-exid 33953  df-mgmOLD 33957  df-sgrOLD 33969  df-mndo 33975  df-rngo 34003
This theorem is referenced by:  rngoueqz  34048  rngonegmn1l  34049  rngonegmn1r  34050  rngoneglmul  34051  rngonegrmul  34052  isdrngo2  34066  rngohomco  34082  rngoisocnv  34089  idlnegcl  34130  1idl  34134  0rngo  34135  smprngopr  34160  prnc  34175  isfldidl  34176  isdmn3  34182
  Copyright terms: Public domain W3C validator