ringlidm - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ringlidm		Structured version Visualization version GIF version

Theorem ringlidm 20491

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

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

**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 = (1_r‘𝑅)
4	1, 2, 3	ringidmlem 20490	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (( 1 · 𝑋) = 𝑋 ∧ (𝑋 · 1 ) = 𝑋))
5	4	simpld 500	1 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ( 1 · 𝑋) = 𝑋)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ‘cfv 6537 (class class class)co 7418 Basecbs 17380 ._rcmulr 17422 1_rcur 20400 Ringcrg 20452

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 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270

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 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-om 7876 df-2nd 8000 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-er 8710 df-en 8967 df-dom 8968 df-sdom 8969 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-nn 12329 df-2 12398 df-sets 17335 df-slot 17353 df-ndx 17365 df-base 17381 df-plusg 17434 df-0g 17605 df-mgm 18809 df-sgrp 18901 df-mnd 18917 df-mgp 20354 df-ur 20401 df-ring 20454

This theorem is used by: ringlidmd 20494 ringo2times 20497 ringidss 20499 ringcomlem 20501 ring1eq0 20522 ringinvnzdiv 20525 ringnegl 20526 imasring 20553 xpsring1d 20556 opprring 20570 dvdsrid 20590 unitmulcl 20603 unitgrp 20606 1rinv 20618 dvreq1 20634 ringinvdv 20637 subrginv 20833 issubrg2 20837 unitrrg 20948 isdrng2 20990 isdrng3lem2 20999 isdrngd 21015 isdrngdOLD 21017 abv1z 21074 issrngd 21105 ornglmullt 21119 orng0le1 21124 sralmod 21455 rngqiprngfulem5 21604 mulgrhm 21776 dvdschrmulg 21827 freshmansdream 21873 asclmul1 22187 psrlmod 22260 psrlidm 22262 mplmonmul 22338 evlslem1 22384 coe1pwmul 22591 mamulid 22749 madetsumid 22769 1mavmul 22856 m1detdiag 22905 mdetralt 22916 mdetunilem7 22926 mdetuni 22930 mdetmul 22931 m2detleib 22939 matunitlindflem1 22987 chfacfpmmulgsum 23175 cpmadugsumlemB 23185 nrginvrcnlem 25003 cphsubrglem 25491 ply1divex 26448 isarchiofld 33753 ress1r 33786 dvrcan5 33789 elrspunidl 33971 mxidlprm 33988 madjusmdetlem1 34452 lfl0 40102 lfladd 40103 eqlkr3 40138 lcfrlem1 42579 hdmapinvlem4 42958 hdmapglem5 42959 mon1psubm 44185 lidldomn1 49297 invginvrid 49448 ply1sclrmsm 49465 ldepsprlem 49553

W3C validator