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

Theorem rngoidmlem 35441
 Description: The unit of a ring is an identity element for the multiplication. (Contributed by FL, 18-Feb-2010.) (New usage is discouraged.)
Hypotheses
Ref Expression
uridm.1 𝐻 = (2nd𝑅)
uridm.2 𝑋 = ran (1st𝑅)
uridm.3 𝑈 = (GId‘𝐻)
Assertion
Ref Expression
rngoidmlem ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ((𝑈𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑈) = 𝐴))

Proof of Theorem rngoidmlem
StepHypRef Expression
1 uridm.1 . . . . 5 𝐻 = (2nd𝑅)
21rngomndo 35440 . . . 4 (𝑅 ∈ RingOps → 𝐻 ∈ MndOp)
3 mndomgmid 35376 . . . 4 (𝐻 ∈ MndOp → 𝐻 ∈ (Magma ∩ ExId ))
4 eqid 2798 . . . . . 6 ran 𝐻 = ran 𝐻
5 uridm.3 . . . . . 6 𝑈 = (GId‘𝐻)
64, 5cmpidelt 35364 . . . . 5 ((𝐻 ∈ (Magma ∩ ExId ) ∧ 𝐴 ∈ ran 𝐻) → ((𝑈𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑈) = 𝐴))
76ex 416 . . . 4 (𝐻 ∈ (Magma ∩ ExId ) → (𝐴 ∈ ran 𝐻 → ((𝑈𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑈) = 𝐴)))
82, 3, 73syl 18 . . 3 (𝑅 ∈ RingOps → (𝐴 ∈ ran 𝐻 → ((𝑈𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑈) = 𝐴)))
9 eqid 2798 . . . . 5 (1st𝑅) = (1st𝑅)
101, 9rngorn1eq 35439 . . . 4 (𝑅 ∈ RingOps → ran (1st𝑅) = ran 𝐻)
11 uridm.2 . . . . 5 𝑋 = ran (1st𝑅)
12 eqtr 2818 . . . . . 6 ((𝑋 = ran (1st𝑅) ∧ ran (1st𝑅) = ran 𝐻) → 𝑋 = ran 𝐻)
13 simpl 486 . . . . . . . . 9 ((𝑋 = ran 𝐻𝑅 ∈ RingOps) → 𝑋 = ran 𝐻)
1413eleq2d 2875 . . . . . . . 8 ((𝑋 = ran 𝐻𝑅 ∈ RingOps) → (𝐴𝑋𝐴 ∈ ran 𝐻))
1514imbi1d 345 . . . . . . 7 ((𝑋 = ran 𝐻𝑅 ∈ RingOps) → ((𝐴𝑋 → ((𝑈𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑈) = 𝐴)) ↔ (𝐴 ∈ ran 𝐻 → ((𝑈𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑈) = 𝐴))))
1615ex 416 . . . . . 6 (𝑋 = ran 𝐻 → (𝑅 ∈ RingOps → ((𝐴𝑋 → ((𝑈𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑈) = 𝐴)) ↔ (𝐴 ∈ ran 𝐻 → ((𝑈𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑈) = 𝐴)))))
1712, 16syl 17 . . . . 5 ((𝑋 = ran (1st𝑅) ∧ ran (1st𝑅) = ran 𝐻) → (𝑅 ∈ RingOps → ((𝐴𝑋 → ((𝑈𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑈) = 𝐴)) ↔ (𝐴 ∈ ran 𝐻 → ((𝑈𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑈) = 𝐴)))))
1811, 17mpan 689 . . . 4 (ran (1st𝑅) = ran 𝐻 → (𝑅 ∈ RingOps → ((𝐴𝑋 → ((𝑈𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑈) = 𝐴)) ↔ (𝐴 ∈ ran 𝐻 → ((𝑈𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑈) = 𝐴)))))
1910, 18mpcom 38 . . 3 (𝑅 ∈ RingOps → ((𝐴𝑋 → ((𝑈𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑈) = 𝐴)) ↔ (𝐴 ∈ ran 𝐻 → ((𝑈𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑈) = 𝐴))))
208, 19mpbird 260 . 2 (𝑅 ∈ RingOps → (𝐴𝑋 → ((𝑈𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑈) = 𝐴)))
2120imp 410 1 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ((𝑈𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑈) = 𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ∩ cin 3881  ran crn 5523  ‘cfv 6329  (class class class)co 7142  1st c1st 7679  2nd c2nd 7680  GIdcgi 28314   ExId cexid 35349  Magmacmagm 35353  MndOpcmndo 35371  RingOpscrngo 35399 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5170  ax-nul 5177  ax-pr 5298  ax-un 7451 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3722  df-csb 3830  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-nul 4246  df-if 4428  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-iota 6288  df-fun 6331  df-fn 6332  df-f 6333  df-fo 6335  df-fv 6337  df-riota 7100  df-ov 7145  df-1st 7681  df-2nd 7682  df-grpo 28317  df-gid 28318  df-ablo 28369  df-ass 35348  df-exid 35350  df-mgmOLD 35354  df-sgrOLD 35366  df-mndo 35372  df-rngo 35400 This theorem is referenced by:  rngolidm  35442  rngoridm  35443
 Copyright terms: Public domain W3C validator