Theorem ringlidm 20376

Description: The unity element of a ring is a left multiplicative identity. (Contributed by NM, 15-Sep-2011.)

Hypotheses

Ref	Expression
ringidm.b	⊢ 𝐵 = (Base‘𝑅)
ringidm.t	⊢ · = (.r‘𝑅)
ringidm.u	⊢ 1 = (1r‘𝑅)

Assertion

Ref	Expression
ringlidm	⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ( 1 · 𝑋) = 𝑋)

Proof of Theorem ringlidm

Step	Hyp	Ref	Expression
1		ringidm.b	. . 3 ⊢ 𝐵 = (Base‘𝑅)
2		ringidm.t	. . 3 ⊢ · = (.r‘𝑅)
3		ringidm.u	. . 3 ⊢ 1 = (1r‘𝑅)
4	1, 2, 3	ringidmlem 20375	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (( 1 · 𝑋) = 𝑋 ∧ (𝑋 · 1 ) = 𝑋))
5	4	simpld 500	1 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ( 1 · 𝑋) = 𝑋)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ‘cfv 6540  (class class class)co 7416  Basecbs 17286  ._rcmulr 17328  1_rcur 20286  Ringcrg 20338

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-cnex 11167  ax-resscn 11168  ax-1cn 11169  ax-icn 11170  ax-addcl 11171  ax-addrcl 11172  ax-mulcl 11173  ax-mulrcl 11174  ax-mulcom 11175  ax-addass 11176  ax-mulass 11177  ax-distr 11178  ax-i2m1 11179  ax-1ne0 11180  ax-1rid 11181  ax-rnegex 11182  ax-rrecex 11183  ax-cnre 11184  ax-pre-lttri 11185  ax-pre-lttrn 11186  ax-pre-ltadd 11187  ax-pre-mulgt0 11188

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-er 8696  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260  df-sub 11454  df-neg 11455  df-nn 12245  df-2 12314  df-sets 17241  df-slot 17259  df-ndx 17271  df-base 17287  df-plusg 17340  df-0g 17511  df-mgm 18715  df-sgrp 18798  df-mnd 18814  df-mgp 20240  df-ur 20287  df-ring 20340

This theorem is used by:  ringlidmd  20379  ringo2times  20382  ringidss  20384  ringcomlem  20386  ring1eq0  20406  ringinvnzdiv  20409  ringnegl  20410  imasring  20437  xpsring1d  20440  opprring  20454  dvdsrid  20474  unitmulcl  20487  unitgrp  20490  1rinv  20502  dvreq1  20518  ringinvdv  20521  subrginv  20716  issubrg2  20720  unitrrg  20831  isdrng2  20872  isdrng3lem2  20881  isdrngd  20897  isdrngdOLD  20899  abv1z  20956  issrngd  20987  ornglmullt  21001  orng0le1  21006  sralmod  21337  rngqiprngfulem5  21484  mulgrhm  21656  dvdschrmulg  21707  freshmansdream  21753  asclmul1  22065  psrlmod  22138  psrlidm  22140  mplmonmul  22216  evlslem1  22262  coe1pwmul  22469  mamulid  22627  madetsumid  22647  1mavmul  22734  m1detdiag  22783  mdetralt  22794  mdetunilem7  22804  mdetuni  22808  mdetmul  22809  m2detleib  22817  chfacfpmmulgsum  23050  cpmadugsumlemB  23060  nrginvrcnlem  24877  cphsubrglem  25365  ply1divex  26323  isarchiofld  33542  ress1r  33575  dvrcan5  33578  elrspunidl  33759  mxidlprm  33776  madjusmdetlem1  34240  matunitlindflem1  38300  lfl0  39872  lfladd  39873  eqlkr3  39908  lcfrlem1  42349  hdmapinvlem4  42728  hdmapglem5  42729  mon1psubm  43959  lidldomn1  49029  invginvrid  49180  ply1sclrmsm  49197  ldepsprlem  49285