Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lidlrng Structured version   Visualization version   GIF version

Theorem lidlrng 41698
Description: A (left) ideal of a ring is a non-unital ring. (Contributed by AV, 17-Feb-2020.)
Hypotheses
Ref Expression
lidlabl.l 𝐿 = (LIdeal‘𝑅)
lidlabl.i 𝐼 = (𝑅s 𝑈)
Assertion
Ref Expression
lidlrng ((𝑅 ∈ Ring ∧ 𝑈𝐿) → 𝐼 ∈ Rng)

Proof of Theorem lidlrng
Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lidlabl.l . . 3 𝐿 = (LIdeal‘𝑅)
2 lidlabl.i . . 3 𝐼 = (𝑅s 𝑈)
31, 2lidlabl 41695 . 2 ((𝑅 ∈ Ring ∧ 𝑈𝐿) → 𝐼 ∈ Abel)
41, 2lidlmsgrp 41697 . 2 ((𝑅 ∈ Ring ∧ 𝑈𝐿) → (mulGrp‘𝐼) ∈ SGrp)
5 simpll 790 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝑈𝐿) ∧ (𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼))) → 𝑅 ∈ Ring)
61, 2lidlssbas 41693 . . . . . . . . . 10 (𝑈𝐿 → (Base‘𝐼) ⊆ (Base‘𝑅))
76sseld 3600 . . . . . . . . 9 (𝑈𝐿 → (𝑎 ∈ (Base‘𝐼) → 𝑎 ∈ (Base‘𝑅)))
86sseld 3600 . . . . . . . . 9 (𝑈𝐿 → (𝑏 ∈ (Base‘𝐼) → 𝑏 ∈ (Base‘𝑅)))
96sseld 3600 . . . . . . . . 9 (𝑈𝐿 → (𝑐 ∈ (Base‘𝐼) → 𝑐 ∈ (Base‘𝑅)))
107, 8, 93anim123d 1405 . . . . . . . 8 (𝑈𝐿 → ((𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼)) → (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑐 ∈ (Base‘𝑅))))
1110adantl 482 . . . . . . 7 ((𝑅 ∈ Ring ∧ 𝑈𝐿) → ((𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼)) → (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑐 ∈ (Base‘𝑅))))
1211imp 445 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝑈𝐿) ∧ (𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼))) → (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑐 ∈ (Base‘𝑅)))
13 eqid 2621 . . . . . . 7 (Base‘𝑅) = (Base‘𝑅)
14 eqid 2621 . . . . . . 7 (+g𝑅) = (+g𝑅)
15 eqid 2621 . . . . . . 7 (.r𝑅) = (.r𝑅)
1613, 14, 15ringdi 18560 . . . . . 6 ((𝑅 ∈ Ring ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑐 ∈ (Base‘𝑅))) → (𝑎(.r𝑅)(𝑏(+g𝑅)𝑐)) = ((𝑎(.r𝑅)𝑏)(+g𝑅)(𝑎(.r𝑅)𝑐)))
175, 12, 16syl2anc 693 . . . . 5 (((𝑅 ∈ Ring ∧ 𝑈𝐿) ∧ (𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼))) → (𝑎(.r𝑅)(𝑏(+g𝑅)𝑐)) = ((𝑎(.r𝑅)𝑏)(+g𝑅)(𝑎(.r𝑅)𝑐)))
1813, 14, 15ringdir 18561 . . . . . 6 ((𝑅 ∈ Ring ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑐 ∈ (Base‘𝑅))) → ((𝑎(+g𝑅)𝑏)(.r𝑅)𝑐) = ((𝑎(.r𝑅)𝑐)(+g𝑅)(𝑏(.r𝑅)𝑐)))
195, 12, 18syl2anc 693 . . . . 5 (((𝑅 ∈ Ring ∧ 𝑈𝐿) ∧ (𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼))) → ((𝑎(+g𝑅)𝑏)(.r𝑅)𝑐) = ((𝑎(.r𝑅)𝑐)(+g𝑅)(𝑏(.r𝑅)𝑐)))
2017, 19jca 554 . . . 4 (((𝑅 ∈ Ring ∧ 𝑈𝐿) ∧ (𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼))) → ((𝑎(.r𝑅)(𝑏(+g𝑅)𝑐)) = ((𝑎(.r𝑅)𝑏)(+g𝑅)(𝑎(.r𝑅)𝑐)) ∧ ((𝑎(+g𝑅)𝑏)(.r𝑅)𝑐) = ((𝑎(.r𝑅)𝑐)(+g𝑅)(𝑏(.r𝑅)𝑐))))
2120ralrimivvva 2971 . . 3 ((𝑅 ∈ Ring ∧ 𝑈𝐿) → ∀𝑎 ∈ (Base‘𝐼)∀𝑏 ∈ (Base‘𝐼)∀𝑐 ∈ (Base‘𝐼)((𝑎(.r𝑅)(𝑏(+g𝑅)𝑐)) = ((𝑎(.r𝑅)𝑏)(+g𝑅)(𝑎(.r𝑅)𝑐)) ∧ ((𝑎(+g𝑅)𝑏)(.r𝑅)𝑐) = ((𝑎(.r𝑅)𝑐)(+g𝑅)(𝑏(.r𝑅)𝑐))))
222, 15ressmulr 16000 . . . . . . . . . 10 (𝑈𝐿 → (.r𝑅) = (.r𝐼))
2322eqcomd 2627 . . . . . . . . 9 (𝑈𝐿 → (.r𝐼) = (.r𝑅))
24 eqidd 2622 . . . . . . . . 9 (𝑈𝐿𝑎 = 𝑎)
252, 14ressplusg 15987 . . . . . . . . . . 11 (𝑈𝐿 → (+g𝑅) = (+g𝐼))
2625eqcomd 2627 . . . . . . . . . 10 (𝑈𝐿 → (+g𝐼) = (+g𝑅))
2726oveqd 6664 . . . . . . . . 9 (𝑈𝐿 → (𝑏(+g𝐼)𝑐) = (𝑏(+g𝑅)𝑐))
2823, 24, 27oveq123d 6668 . . . . . . . 8 (𝑈𝐿 → (𝑎(.r𝐼)(𝑏(+g𝐼)𝑐)) = (𝑎(.r𝑅)(𝑏(+g𝑅)𝑐)))
2923oveqd 6664 . . . . . . . . 9 (𝑈𝐿 → (𝑎(.r𝐼)𝑏) = (𝑎(.r𝑅)𝑏))
3023oveqd 6664 . . . . . . . . 9 (𝑈𝐿 → (𝑎(.r𝐼)𝑐) = (𝑎(.r𝑅)𝑐))
3126, 29, 30oveq123d 6668 . . . . . . . 8 (𝑈𝐿 → ((𝑎(.r𝐼)𝑏)(+g𝐼)(𝑎(.r𝐼)𝑐)) = ((𝑎(.r𝑅)𝑏)(+g𝑅)(𝑎(.r𝑅)𝑐)))
3228, 31eqeq12d 2636 . . . . . . 7 (𝑈𝐿 → ((𝑎(.r𝐼)(𝑏(+g𝐼)𝑐)) = ((𝑎(.r𝐼)𝑏)(+g𝐼)(𝑎(.r𝐼)𝑐)) ↔ (𝑎(.r𝑅)(𝑏(+g𝑅)𝑐)) = ((𝑎(.r𝑅)𝑏)(+g𝑅)(𝑎(.r𝑅)𝑐))))
3326oveqd 6664 . . . . . . . . 9 (𝑈𝐿 → (𝑎(+g𝐼)𝑏) = (𝑎(+g𝑅)𝑏))
34 eqidd 2622 . . . . . . . . 9 (𝑈𝐿𝑐 = 𝑐)
3523, 33, 34oveq123d 6668 . . . . . . . 8 (𝑈𝐿 → ((𝑎(+g𝐼)𝑏)(.r𝐼)𝑐) = ((𝑎(+g𝑅)𝑏)(.r𝑅)𝑐))
3623oveqd 6664 . . . . . . . . 9 (𝑈𝐿 → (𝑏(.r𝐼)𝑐) = (𝑏(.r𝑅)𝑐))
3726, 30, 36oveq123d 6668 . . . . . . . 8 (𝑈𝐿 → ((𝑎(.r𝐼)𝑐)(+g𝐼)(𝑏(.r𝐼)𝑐)) = ((𝑎(.r𝑅)𝑐)(+g𝑅)(𝑏(.r𝑅)𝑐)))
3835, 37eqeq12d 2636 . . . . . . 7 (𝑈𝐿 → (((𝑎(+g𝐼)𝑏)(.r𝐼)𝑐) = ((𝑎(.r𝐼)𝑐)(+g𝐼)(𝑏(.r𝐼)𝑐)) ↔ ((𝑎(+g𝑅)𝑏)(.r𝑅)𝑐) = ((𝑎(.r𝑅)𝑐)(+g𝑅)(𝑏(.r𝑅)𝑐))))
3932, 38anbi12d 747 . . . . . 6 (𝑈𝐿 → (((𝑎(.r𝐼)(𝑏(+g𝐼)𝑐)) = ((𝑎(.r𝐼)𝑏)(+g𝐼)(𝑎(.r𝐼)𝑐)) ∧ ((𝑎(+g𝐼)𝑏)(.r𝐼)𝑐) = ((𝑎(.r𝐼)𝑐)(+g𝐼)(𝑏(.r𝐼)𝑐))) ↔ ((𝑎(.r𝑅)(𝑏(+g𝑅)𝑐)) = ((𝑎(.r𝑅)𝑏)(+g𝑅)(𝑎(.r𝑅)𝑐)) ∧ ((𝑎(+g𝑅)𝑏)(.r𝑅)𝑐) = ((𝑎(.r𝑅)𝑐)(+g𝑅)(𝑏(.r𝑅)𝑐)))))
4039adantl 482 . . . . 5 ((𝑅 ∈ Ring ∧ 𝑈𝐿) → (((𝑎(.r𝐼)(𝑏(+g𝐼)𝑐)) = ((𝑎(.r𝐼)𝑏)(+g𝐼)(𝑎(.r𝐼)𝑐)) ∧ ((𝑎(+g𝐼)𝑏)(.r𝐼)𝑐) = ((𝑎(.r𝐼)𝑐)(+g𝐼)(𝑏(.r𝐼)𝑐))) ↔ ((𝑎(.r𝑅)(𝑏(+g𝑅)𝑐)) = ((𝑎(.r𝑅)𝑏)(+g𝑅)(𝑎(.r𝑅)𝑐)) ∧ ((𝑎(+g𝑅)𝑏)(.r𝑅)𝑐) = ((𝑎(.r𝑅)𝑐)(+g𝑅)(𝑏(.r𝑅)𝑐)))))
4140ralbidv 2985 . . . 4 ((𝑅 ∈ Ring ∧ 𝑈𝐿) → (∀𝑐 ∈ (Base‘𝐼)((𝑎(.r𝐼)(𝑏(+g𝐼)𝑐)) = ((𝑎(.r𝐼)𝑏)(+g𝐼)(𝑎(.r𝐼)𝑐)) ∧ ((𝑎(+g𝐼)𝑏)(.r𝐼)𝑐) = ((𝑎(.r𝐼)𝑐)(+g𝐼)(𝑏(.r𝐼)𝑐))) ↔ ∀𝑐 ∈ (Base‘𝐼)((𝑎(.r𝑅)(𝑏(+g𝑅)𝑐)) = ((𝑎(.r𝑅)𝑏)(+g𝑅)(𝑎(.r𝑅)𝑐)) ∧ ((𝑎(+g𝑅)𝑏)(.r𝑅)𝑐) = ((𝑎(.r𝑅)𝑐)(+g𝑅)(𝑏(.r𝑅)𝑐)))))
42412ralbidv 2988 . . 3 ((𝑅 ∈ Ring ∧ 𝑈𝐿) → (∀𝑎 ∈ (Base‘𝐼)∀𝑏 ∈ (Base‘𝐼)∀𝑐 ∈ (Base‘𝐼)((𝑎(.r𝐼)(𝑏(+g𝐼)𝑐)) = ((𝑎(.r𝐼)𝑏)(+g𝐼)(𝑎(.r𝐼)𝑐)) ∧ ((𝑎(+g𝐼)𝑏)(.r𝐼)𝑐) = ((𝑎(.r𝐼)𝑐)(+g𝐼)(𝑏(.r𝐼)𝑐))) ↔ ∀𝑎 ∈ (Base‘𝐼)∀𝑏 ∈ (Base‘𝐼)∀𝑐 ∈ (Base‘𝐼)((𝑎(.r𝑅)(𝑏(+g𝑅)𝑐)) = ((𝑎(.r𝑅)𝑏)(+g𝑅)(𝑎(.r𝑅)𝑐)) ∧ ((𝑎(+g𝑅)𝑏)(.r𝑅)𝑐) = ((𝑎(.r𝑅)𝑐)(+g𝑅)(𝑏(.r𝑅)𝑐)))))
4321, 42mpbird 247 . 2 ((𝑅 ∈ Ring ∧ 𝑈𝐿) → ∀𝑎 ∈ (Base‘𝐼)∀𝑏 ∈ (Base‘𝐼)∀𝑐 ∈ (Base‘𝐼)((𝑎(.r𝐼)(𝑏(+g𝐼)𝑐)) = ((𝑎(.r𝐼)𝑏)(+g𝐼)(𝑎(.r𝐼)𝑐)) ∧ ((𝑎(+g𝐼)𝑏)(.r𝐼)𝑐) = ((𝑎(.r𝐼)𝑐)(+g𝐼)(𝑏(.r𝐼)𝑐))))
44 eqid 2621 . . 3 (Base‘𝐼) = (Base‘𝐼)
45 eqid 2621 . . 3 (mulGrp‘𝐼) = (mulGrp‘𝐼)
46 eqid 2621 . . 3 (+g𝐼) = (+g𝐼)
47 eqid 2621 . . 3 (.r𝐼) = (.r𝐼)
4844, 45, 46, 47isrng 41647 . 2 (𝐼 ∈ Rng ↔ (𝐼 ∈ Abel ∧ (mulGrp‘𝐼) ∈ SGrp ∧ ∀𝑎 ∈ (Base‘𝐼)∀𝑏 ∈ (Base‘𝐼)∀𝑐 ∈ (Base‘𝐼)((𝑎(.r𝐼)(𝑏(+g𝐼)𝑐)) = ((𝑎(.r𝐼)𝑏)(+g𝐼)(𝑎(.r𝐼)𝑐)) ∧ ((𝑎(+g𝐼)𝑏)(.r𝐼)𝑐) = ((𝑎(.r𝐼)𝑐)(+g𝐼)(𝑏(.r𝐼)𝑐)))))
493, 4, 43, 48syl3anbrc 1245 1 ((𝑅 ∈ Ring ∧ 𝑈𝐿) → 𝐼 ∈ Rng)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1037   = wceq 1482  wcel 1989  wral 2911  cfv 5886  (class class class)co 6647  Basecbs 15851  s cress 15852  +gcplusg 15935  .rcmulr 15936  SGrpcsgrp 17277  Abelcabl 18188  mulGrpcmgp 18483  Ringcrg 18541  LIdealclidl 19164  Rngcrng 41645
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-rep 4769  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946  ax-cnex 9989  ax-resscn 9990  ax-1cn 9991  ax-icn 9992  ax-addcl 9993  ax-addrcl 9994  ax-mulcl 9995  ax-mulrcl 9996  ax-mulcom 9997  ax-addass 9998  ax-mulass 9999  ax-distr 10000  ax-i2m1 10001  ax-1ne0 10002  ax-1rid 10003  ax-rnegex 10004  ax-rrecex 10005  ax-cnre 10006  ax-pre-lttri 10007  ax-pre-lttrn 10008  ax-pre-ltadd 10009  ax-pre-mulgt0 10010
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-nel 2897  df-ral 2916  df-rex 2917  df-reu 2918  df-rmo 2919  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-riota 6608  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-om 7063  df-1st 7165  df-2nd 7166  df-wrecs 7404  df-recs 7465  df-rdg 7503  df-er 7739  df-en 7953  df-dom 7954  df-sdom 7955  df-pnf 10073  df-mnf 10074  df-xr 10075  df-ltxr 10076  df-le 10077  df-sub 10265  df-neg 10266  df-nn 11018  df-2 11076  df-3 11077  df-4 11078  df-5 11079  df-6 11080  df-7 11081  df-8 11082  df-ndx 15854  df-slot 15855  df-base 15857  df-sets 15858  df-ress 15859  df-plusg 15948  df-mulr 15949  df-sca 15951  df-vsca 15952  df-ip 15953  df-0g 16096  df-mgm 17236  df-sgrp 17278  df-mnd 17289  df-grp 17419  df-minusg 17420  df-sbg 17421  df-subg 17585  df-cmn 18189  df-abl 18190  df-mgp 18484  df-ur 18496  df-ring 18543  df-subrg 18772  df-lmod 18859  df-lss 18927  df-sra 19166  df-rgmod 19167  df-lidl 19168  df-rng0 41646
This theorem is referenced by:  zlidlring  41699  uzlidlring  41700  2zrng  41706
  Copyright terms: Public domain W3C validator