![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ringlz | Structured version Visualization version GIF version |
Description: The zero of a unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.) |
Ref | Expression |
---|---|
ringz.b | ⊢ 𝐵 = (Base‘𝑅) |
ringz.t | ⊢ · = (.r‘𝑅) |
ringz.z | ⊢ 0 = (0g‘𝑅) |
Ref | Expression |
---|---|
ringlz | ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ( 0 · 𝑋) = 0 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ringgrp 20051 | . . . . . 6 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | |
2 | ringz.b | . . . . . . 7 ⊢ 𝐵 = (Base‘𝑅) | |
3 | ringz.z | . . . . . . 7 ⊢ 0 = (0g‘𝑅) | |
4 | 2, 3 | grpidcl 18845 | . . . . . 6 ⊢ (𝑅 ∈ Grp → 0 ∈ 𝐵) |
5 | eqid 2733 | . . . . . . 7 ⊢ (+g‘𝑅) = (+g‘𝑅) | |
6 | 2, 5, 3 | grplid 18847 | . . . . . 6 ⊢ ((𝑅 ∈ Grp ∧ 0 ∈ 𝐵) → ( 0 (+g‘𝑅) 0 ) = 0 ) |
7 | 1, 4, 6 | syl2anc2 586 | . . . . 5 ⊢ (𝑅 ∈ Ring → ( 0 (+g‘𝑅) 0 ) = 0 ) |
8 | 7 | adantr 482 | . . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ( 0 (+g‘𝑅) 0 ) = 0 ) |
9 | 8 | oveq1d 7418 | . . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (( 0 (+g‘𝑅) 0 ) · 𝑋) = ( 0 · 𝑋)) |
10 | 1, 4 | syl 17 | . . . . . 6 ⊢ (𝑅 ∈ Ring → 0 ∈ 𝐵) |
11 | 10 | adantr 482 | . . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 0 ∈ 𝐵) |
12 | simpr 486 | . . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ 𝐵) | |
13 | 11, 11, 12 | 3jca 1129 | . . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ( 0 ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) |
14 | ringz.t | . . . . 5 ⊢ · = (.r‘𝑅) | |
15 | 2, 5, 14 | ringdir 20071 | . . . 4 ⊢ ((𝑅 ∈ Ring ∧ ( 0 ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) → (( 0 (+g‘𝑅) 0 ) · 𝑋) = (( 0 · 𝑋)(+g‘𝑅)( 0 · 𝑋))) |
16 | 13, 15 | syldan 592 | . . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (( 0 (+g‘𝑅) 0 ) · 𝑋) = (( 0 · 𝑋)(+g‘𝑅)( 0 · 𝑋))) |
17 | 1 | adantr 482 | . . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 𝑅 ∈ Grp) |
18 | simpl 484 | . . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 𝑅 ∈ Ring) | |
19 | 2, 14 | ringcl 20063 | . . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ( 0 · 𝑋) ∈ 𝐵) |
20 | 18, 11, 12, 19 | syl3anc 1372 | . . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ( 0 · 𝑋) ∈ 𝐵) |
21 | 2, 5, 3 | grprid 18848 | . . . . 5 ⊢ ((𝑅 ∈ Grp ∧ ( 0 · 𝑋) ∈ 𝐵) → (( 0 · 𝑋)(+g‘𝑅) 0 ) = ( 0 · 𝑋)) |
22 | 21 | eqcomd 2739 | . . . 4 ⊢ ((𝑅 ∈ Grp ∧ ( 0 · 𝑋) ∈ 𝐵) → ( 0 · 𝑋) = (( 0 · 𝑋)(+g‘𝑅) 0 )) |
23 | 17, 20, 22 | syl2anc 585 | . . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ( 0 · 𝑋) = (( 0 · 𝑋)(+g‘𝑅) 0 )) |
24 | 9, 16, 23 | 3eqtr3d 2781 | . 2 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (( 0 · 𝑋)(+g‘𝑅)( 0 · 𝑋)) = (( 0 · 𝑋)(+g‘𝑅) 0 )) |
25 | 2, 5 | grplcan 18880 | . . 3 ⊢ ((𝑅 ∈ Grp ∧ (( 0 · 𝑋) ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ ( 0 · 𝑋) ∈ 𝐵)) → ((( 0 · 𝑋)(+g‘𝑅)( 0 · 𝑋)) = (( 0 · 𝑋)(+g‘𝑅) 0 ) ↔ ( 0 · 𝑋) = 0 )) |
26 | 17, 20, 11, 20, 25 | syl13anc 1373 | . 2 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ((( 0 · 𝑋)(+g‘𝑅)( 0 · 𝑋)) = (( 0 · 𝑋)(+g‘𝑅) 0 ) ↔ ( 0 · 𝑋) = 0 )) |
27 | 24, 26 | mpbid 231 | 1 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ( 0 · 𝑋) = 0 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ‘cfv 6539 (class class class)co 7403 Basecbs 17139 +gcplusg 17192 .rcmulr 17193 0gc0g 17380 Grpcgrp 18814 Ringcrg 20046 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5297 ax-nul 5304 ax-pow 5361 ax-pr 5425 ax-un 7719 ax-cnex 11161 ax-resscn 11162 ax-1cn 11163 ax-icn 11164 ax-addcl 11165 ax-addrcl 11166 ax-mulcl 11167 ax-mulrcl 11168 ax-mulcom 11169 ax-addass 11170 ax-mulass 11171 ax-distr 11172 ax-i2m1 11173 ax-1ne0 11174 ax-1rid 11175 ax-rnegex 11176 ax-rrecex 11177 ax-cnre 11178 ax-pre-lttri 11179 ax-pre-lttrn 11180 ax-pre-ltadd 11181 ax-pre-mulgt0 11182 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3776 df-csb 3892 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-pss 3965 df-nul 4321 df-if 4527 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4907 df-iun 4997 df-br 5147 df-opab 5209 df-mpt 5230 df-tr 5264 df-id 5572 df-eprel 5578 df-po 5586 df-so 5587 df-fr 5629 df-we 5631 df-xp 5680 df-rel 5681 df-cnv 5682 df-co 5683 df-dm 5684 df-rn 5685 df-res 5686 df-ima 5687 df-pred 6296 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6491 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-riota 7359 df-ov 7406 df-oprab 7407 df-mpo 7408 df-om 7850 df-2nd 7970 df-frecs 8260 df-wrecs 8291 df-recs 8365 df-rdg 8404 df-er 8698 df-en 8935 df-dom 8936 df-sdom 8937 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11441 df-neg 11442 df-nn 12208 df-2 12270 df-sets 17092 df-slot 17110 df-ndx 17122 df-base 17140 df-plusg 17205 df-0g 17382 df-mgm 18556 df-sgrp 18605 df-mnd 18621 df-grp 18817 df-minusg 18818 df-mgp 19979 df-ring 20048 |
This theorem is referenced by: ringsrg 20098 ring1eq0 20099 ringnegl 20103 mulgass2 20110 gsumdixp 20120 dvdsr01 20173 0unit 20198 irredn0 20225 drngmul0or 20331 isdrngd 20335 cntzsubr 20385 cntzsdrg 20405 isabvd 20415 domneq0 20899 frlmphllem 21318 psrlidm 21504 mplsubrglem 21544 mplmonmul 21572 evlslem4 21618 evlslem3 21624 evlslem6 21625 mhpmulcl 21673 coe1tmmul 21780 cply1mul 21799 mamulid 21924 dmatmul 21980 scmatscm 21996 1mavmul 22031 mdetdiaglem 22081 mdetr0 22088 mdegmullem 25577 coe1mul3 25598 fta1glem1 25664 dvdschrmulg 32354 rmfsupp2 32361 elrspunidl 32503 elrspunsn 32504 drngidl 32508 evls1fpws 32595 fedgmullem1 32658 lflsc0N 37890 hdmapinvlem3 40728 hdmapinvlem4 40729 fldhmf1 40892 ringlzd 41033 evlsbagval 41087 mnringmulrcld 42919 zrrnghm 46649 zlidlring 46727 rmsupp0 46945 ply1mulgsumlem2 46969 |
Copyright terms: Public domain | W3C validator |