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

Theorem zlidlring 42355
Description: The zero (left) ideal of a non-unital ring is a unital ring (the zero ring). (Contributed by AV, 16-Feb-2020.)
Hypotheses
Ref Expression
lidlabl.l 𝐿 = (LIdeal‘𝑅)
lidlabl.i 𝐼 = (𝑅s 𝑈)
zlidlring.b 𝐵 = (Base‘𝑅)
zlidlring.0 0 = (0g𝑅)
Assertion
Ref Expression
zlidlring ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → 𝐼 ∈ Ring)

Proof of Theorem zlidlring
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 474 . . . . 5 ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → 𝑅 ∈ Ring)
2 lidlabl.l . . . . . . . 8 𝐿 = (LIdeal‘𝑅)
3 zlidlring.0 . . . . . . . 8 0 = (0g𝑅)
42, 3lidl0 19342 . . . . . . 7 (𝑅 ∈ Ring → { 0 } ∈ 𝐿)
54adantr 472 . . . . . 6 ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → { 0 } ∈ 𝐿)
6 eleq1 2791 . . . . . . 7 (𝑈 = { 0 } → (𝑈𝐿 ↔ { 0 } ∈ 𝐿))
76adantl 473 . . . . . 6 ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → (𝑈𝐿 ↔ { 0 } ∈ 𝐿))
85, 7mpbird 247 . . . . 5 ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → 𝑈𝐿)
91, 8jca 555 . . . 4 ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → (𝑅 ∈ Ring ∧ 𝑈𝐿))
10 lidlabl.i . . . . 5 𝐼 = (𝑅s 𝑈)
112, 10lidlrng 42354 . . . 4 ((𝑅 ∈ Ring ∧ 𝑈𝐿) → 𝐼 ∈ Rng)
129, 11syl 17 . . 3 ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → 𝐼 ∈ Rng)
13 eleq1 2791 . . . . . . 7 ({ 0 } = 𝑈 → ({ 0 } ∈ 𝐿𝑈𝐿))
1413eqcoms 2732 . . . . . 6 (𝑈 = { 0 } → ({ 0 } ∈ 𝐿𝑈𝐿))
1514adantl 473 . . . . 5 ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → ({ 0 } ∈ 𝐿𝑈𝐿))
16 id 22 . . . . . . . . . . . . 13 (𝑅 ∈ Ring → 𝑅 ∈ Ring)
17 eqid 2724 . . . . . . . . . . . . . 14 (Base‘𝑅) = (Base‘𝑅)
1817, 3ring0cl 18690 . . . . . . . . . . . . 13 (𝑅 ∈ Ring → 0 ∈ (Base‘𝑅))
1916, 18jca 555 . . . . . . . . . . . 12 (𝑅 ∈ Ring → (𝑅 ∈ Ring ∧ 0 ∈ (Base‘𝑅)))
20 eqid 2724 . . . . . . . . . . . . . 14 (.r𝑅) = (.r𝑅)
2117, 20, 3ringlz 18708 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ 0 ∈ (Base‘𝑅)) → ( 0 (.r𝑅) 0 ) = 0 )
2221, 21jca 555 . . . . . . . . . . . 12 ((𝑅 ∈ Ring ∧ 0 ∈ (Base‘𝑅)) → (( 0 (.r𝑅) 0 ) = 0 ∧ ( 0 (.r𝑅) 0 ) = 0 ))
2319, 22syl 17 . . . . . . . . . . 11 (𝑅 ∈ Ring → (( 0 (.r𝑅) 0 ) = 0 ∧ ( 0 (.r𝑅) 0 ) = 0 ))
24 fvex 6314 . . . . . . . . . . . . . 14 (0g𝑅) ∈ V
253, 24eqeltri 2799 . . . . . . . . . . . . 13 0 ∈ V
2625a1i 11 . . . . . . . . . . . 12 (𝑅 ∈ Ring → 0 ∈ V)
27 oveq2 6773 . . . . . . . . . . . . . . 15 (𝑦 = 0 → ( 0 (.r𝑅)𝑦) = ( 0 (.r𝑅) 0 ))
28 id 22 . . . . . . . . . . . . . . 15 (𝑦 = 0𝑦 = 0 )
2927, 28eqeq12d 2739 . . . . . . . . . . . . . 14 (𝑦 = 0 → (( 0 (.r𝑅)𝑦) = 𝑦 ↔ ( 0 (.r𝑅) 0 ) = 0 ))
30 oveq1 6772 . . . . . . . . . . . . . . 15 (𝑦 = 0 → (𝑦(.r𝑅) 0 ) = ( 0 (.r𝑅) 0 ))
3130, 28eqeq12d 2739 . . . . . . . . . . . . . 14 (𝑦 = 0 → ((𝑦(.r𝑅) 0 ) = 𝑦 ↔ ( 0 (.r𝑅) 0 ) = 0 ))
3229, 31anbi12d 749 . . . . . . . . . . . . 13 (𝑦 = 0 → ((( 0 (.r𝑅)𝑦) = 𝑦 ∧ (𝑦(.r𝑅) 0 ) = 𝑦) ↔ (( 0 (.r𝑅) 0 ) = 0 ∧ ( 0 (.r𝑅) 0 ) = 0 )))
3332ralsng 4325 . . . . . . . . . . . 12 ( 0 ∈ V → (∀𝑦 ∈ { 0 } (( 0 (.r𝑅)𝑦) = 𝑦 ∧ (𝑦(.r𝑅) 0 ) = 𝑦) ↔ (( 0 (.r𝑅) 0 ) = 0 ∧ ( 0 (.r𝑅) 0 ) = 0 )))
3426, 33syl 17 . . . . . . . . . . 11 (𝑅 ∈ Ring → (∀𝑦 ∈ { 0 } (( 0 (.r𝑅)𝑦) = 𝑦 ∧ (𝑦(.r𝑅) 0 ) = 𝑦) ↔ (( 0 (.r𝑅) 0 ) = 0 ∧ ( 0 (.r𝑅) 0 ) = 0 )))
3523, 34mpbird 247 . . . . . . . . . 10 (𝑅 ∈ Ring → ∀𝑦 ∈ { 0 } (( 0 (.r𝑅)𝑦) = 𝑦 ∧ (𝑦(.r𝑅) 0 ) = 𝑦))
36 oveq1 6772 . . . . . . . . . . . . . . 15 (𝑥 = 0 → (𝑥(.r𝑅)𝑦) = ( 0 (.r𝑅)𝑦))
3736eqeq1d 2726 . . . . . . . . . . . . . 14 (𝑥 = 0 → ((𝑥(.r𝑅)𝑦) = 𝑦 ↔ ( 0 (.r𝑅)𝑦) = 𝑦))
38 oveq2 6773 . . . . . . . . . . . . . . 15 (𝑥 = 0 → (𝑦(.r𝑅)𝑥) = (𝑦(.r𝑅) 0 ))
3938eqeq1d 2726 . . . . . . . . . . . . . 14 (𝑥 = 0 → ((𝑦(.r𝑅)𝑥) = 𝑦 ↔ (𝑦(.r𝑅) 0 ) = 𝑦))
4037, 39anbi12d 749 . . . . . . . . . . . . 13 (𝑥 = 0 → (((𝑥(.r𝑅)𝑦) = 𝑦 ∧ (𝑦(.r𝑅)𝑥) = 𝑦) ↔ (( 0 (.r𝑅)𝑦) = 𝑦 ∧ (𝑦(.r𝑅) 0 ) = 𝑦)))
4140ralbidv 3088 . . . . . . . . . . . 12 (𝑥 = 0 → (∀𝑦 ∈ { 0 } ((𝑥(.r𝑅)𝑦) = 𝑦 ∧ (𝑦(.r𝑅)𝑥) = 𝑦) ↔ ∀𝑦 ∈ { 0 } (( 0 (.r𝑅)𝑦) = 𝑦 ∧ (𝑦(.r𝑅) 0 ) = 𝑦)))
4241rexsng 4326 . . . . . . . . . . 11 ( 0 ∈ V → (∃𝑥 ∈ { 0 }∀𝑦 ∈ { 0 } ((𝑥(.r𝑅)𝑦) = 𝑦 ∧ (𝑦(.r𝑅)𝑥) = 𝑦) ↔ ∀𝑦 ∈ { 0 } (( 0 (.r𝑅)𝑦) = 𝑦 ∧ (𝑦(.r𝑅) 0 ) = 𝑦)))
4326, 42syl 17 . . . . . . . . . 10 (𝑅 ∈ Ring → (∃𝑥 ∈ { 0 }∀𝑦 ∈ { 0 } ((𝑥(.r𝑅)𝑦) = 𝑦 ∧ (𝑦(.r𝑅)𝑥) = 𝑦) ↔ ∀𝑦 ∈ { 0 } (( 0 (.r𝑅)𝑦) = 𝑦 ∧ (𝑦(.r𝑅) 0 ) = 𝑦)))
4435, 43mpbird 247 . . . . . . . . 9 (𝑅 ∈ Ring → ∃𝑥 ∈ { 0 }∀𝑦 ∈ { 0 } ((𝑥(.r𝑅)𝑦) = 𝑦 ∧ (𝑦(.r𝑅)𝑥) = 𝑦))
4544adantr 472 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → ∃𝑥 ∈ { 0 }∀𝑦 ∈ { 0 } ((𝑥(.r𝑅)𝑦) = 𝑦 ∧ (𝑦(.r𝑅)𝑥) = 𝑦))
4645adantr 472 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈𝐿) → ∃𝑥 ∈ { 0 }∀𝑦 ∈ { 0 } ((𝑥(.r𝑅)𝑦) = 𝑦 ∧ (𝑦(.r𝑅)𝑥) = 𝑦))
47 simpr 479 . . . . . . . . . 10 (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈𝐿) → 𝑈𝐿)
482, 10lidlbas 42350 . . . . . . . . . 10 (𝑈𝐿 → (Base‘𝐼) = 𝑈)
4947, 48syl 17 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈𝐿) → (Base‘𝐼) = 𝑈)
50 simpr 479 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → 𝑈 = { 0 })
5150adantr 472 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈𝐿) → 𝑈 = { 0 })
5249, 51eqtrd 2758 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈𝐿) → (Base‘𝐼) = { 0 })
5310, 20ressmulr 16129 . . . . . . . . . . . . . 14 (𝑈𝐿 → (.r𝑅) = (.r𝐼))
5453eqcomd 2730 . . . . . . . . . . . . 13 (𝑈𝐿 → (.r𝐼) = (.r𝑅))
5554adantl 473 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈𝐿) → (.r𝐼) = (.r𝑅))
5655oveqd 6782 . . . . . . . . . . 11 (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈𝐿) → (𝑥(.r𝐼)𝑦) = (𝑥(.r𝑅)𝑦))
5756eqeq1d 2726 . . . . . . . . . 10 (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈𝐿) → ((𝑥(.r𝐼)𝑦) = 𝑦 ↔ (𝑥(.r𝑅)𝑦) = 𝑦))
5855oveqd 6782 . . . . . . . . . . 11 (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈𝐿) → (𝑦(.r𝐼)𝑥) = (𝑦(.r𝑅)𝑥))
5958eqeq1d 2726 . . . . . . . . . 10 (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈𝐿) → ((𝑦(.r𝐼)𝑥) = 𝑦 ↔ (𝑦(.r𝑅)𝑥) = 𝑦))
6057, 59anbi12d 749 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈𝐿) → (((𝑥(.r𝐼)𝑦) = 𝑦 ∧ (𝑦(.r𝐼)𝑥) = 𝑦) ↔ ((𝑥(.r𝑅)𝑦) = 𝑦 ∧ (𝑦(.r𝑅)𝑥) = 𝑦)))
6152, 60raleqbidv 3255 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈𝐿) → (∀𝑦 ∈ (Base‘𝐼)((𝑥(.r𝐼)𝑦) = 𝑦 ∧ (𝑦(.r𝐼)𝑥) = 𝑦) ↔ ∀𝑦 ∈ { 0 } ((𝑥(.r𝑅)𝑦) = 𝑦 ∧ (𝑦(.r𝑅)𝑥) = 𝑦)))
6252, 61rexeqbidv 3256 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈𝐿) → (∃𝑥 ∈ (Base‘𝐼)∀𝑦 ∈ (Base‘𝐼)((𝑥(.r𝐼)𝑦) = 𝑦 ∧ (𝑦(.r𝐼)𝑥) = 𝑦) ↔ ∃𝑥 ∈ { 0 }∀𝑦 ∈ { 0 } ((𝑥(.r𝑅)𝑦) = 𝑦 ∧ (𝑦(.r𝑅)𝑥) = 𝑦)))
6346, 62mpbird 247 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈𝐿) → ∃𝑥 ∈ (Base‘𝐼)∀𝑦 ∈ (Base‘𝐼)((𝑥(.r𝐼)𝑦) = 𝑦 ∧ (𝑦(.r𝐼)𝑥) = 𝑦))
6463ex 449 . . . . 5 ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → (𝑈𝐿 → ∃𝑥 ∈ (Base‘𝐼)∀𝑦 ∈ (Base‘𝐼)((𝑥(.r𝐼)𝑦) = 𝑦 ∧ (𝑦(.r𝐼)𝑥) = 𝑦)))
6515, 64sylbid 230 . . . 4 ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → ({ 0 } ∈ 𝐿 → ∃𝑥 ∈ (Base‘𝐼)∀𝑦 ∈ (Base‘𝐼)((𝑥(.r𝐼)𝑦) = 𝑦 ∧ (𝑦(.r𝐼)𝑥) = 𝑦)))
665, 65mpd 15 . . 3 ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → ∃𝑥 ∈ (Base‘𝐼)∀𝑦 ∈ (Base‘𝐼)((𝑥(.r𝐼)𝑦) = 𝑦 ∧ (𝑦(.r𝐼)𝑥) = 𝑦))
6712, 66jca 555 . 2 ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → (𝐼 ∈ Rng ∧ ∃𝑥 ∈ (Base‘𝐼)∀𝑦 ∈ (Base‘𝐼)((𝑥(.r𝐼)𝑦) = 𝑦 ∧ (𝑦(.r𝐼)𝑥) = 𝑦)))
68 eqid 2724 . . 3 (Base‘𝐼) = (Base‘𝐼)
69 eqid 2724 . . 3 (.r𝐼) = (.r𝐼)
7068, 69isringrng 42308 . 2 (𝐼 ∈ Ring ↔ (𝐼 ∈ Rng ∧ ∃𝑥 ∈ (Base‘𝐼)∀𝑦 ∈ (Base‘𝐼)((𝑥(.r𝐼)𝑦) = 𝑦 ∧ (𝑦(.r𝐼)𝑥) = 𝑦)))
7167, 70sylibr 224 1 ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → 𝐼 ∈ Ring)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1596  wcel 2103  wral 3014  wrex 3015  Vcvv 3304  {csn 4285  cfv 6001  (class class class)co 6765  Basecbs 15980  s cress 15981  .rcmulr 16065  0gc0g 16223  Ringcrg 18668  LIdealclidl 19293  Rngcrng 42301
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-rep 4879  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-cnex 10105  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-om 7183  df-1st 7285  df-2nd 7286  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-er 7862  df-en 8073  df-dom 8074  df-sdom 8075  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-nn 11134  df-2 11192  df-3 11193  df-4 11194  df-5 11195  df-6 11196  df-7 11197  df-8 11198  df-ndx 15983  df-slot 15984  df-base 15986  df-sets 15987  df-ress 15988  df-plusg 16077  df-mulr 16078  df-sca 16080  df-vsca 16081  df-ip 16082  df-0g 16225  df-mgm 17364  df-sgrp 17406  df-mnd 17417  df-grp 17547  df-minusg 17548  df-sbg 17549  df-subg 17713  df-cmn 18316  df-abl 18317  df-mgp 18611  df-ur 18623  df-ring 18670  df-subrg 18901  df-lmod 18988  df-lss 19056  df-sra 19295  df-rgmod 19296  df-lidl 19297  df-rng0 42302
This theorem is referenced by:  uzlidlring  42356
  Copyright terms: Public domain W3C validator