Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  idladdcl Structured version   Visualization version   GIF version

Theorem idladdcl 38004
Description: An ideal is closed under addition. (Contributed by Jeff Madsen, 10-Jun-2010.)
Hypothesis
Ref Expression
idladdcl.1 𝐺 = (1st𝑅)
Assertion
Ref Expression
idladdcl (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴𝐼𝐵𝐼)) → (𝐴𝐺𝐵) ∈ 𝐼)

Proof of Theorem idladdcl
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 idladdcl.1 . . . . . 6 𝐺 = (1st𝑅)
2 eqid 2736 . . . . . 6 (2nd𝑅) = (2nd𝑅)
3 eqid 2736 . . . . . 6 ran 𝐺 = ran 𝐺
4 eqid 2736 . . . . . 6 (GId‘𝐺) = (GId‘𝐺)
51, 2, 3, 4isidl 37999 . . . . 5 (𝑅 ∈ RingOps → (𝐼 ∈ (Idl‘𝑅) ↔ (𝐼 ⊆ ran 𝐺 ∧ (GId‘𝐺) ∈ 𝐼 ∧ ∀𝑥𝐼 (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧 ∈ ran 𝐺((𝑧(2nd𝑅)𝑥) ∈ 𝐼 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐼)))))
65biimpa 476 . . . 4 ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → (𝐼 ⊆ ran 𝐺 ∧ (GId‘𝐺) ∈ 𝐼 ∧ ∀𝑥𝐼 (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧 ∈ ran 𝐺((𝑧(2nd𝑅)𝑥) ∈ 𝐼 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐼))))
76simp3d 1145 . . 3 ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → ∀𝑥𝐼 (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧 ∈ ran 𝐺((𝑧(2nd𝑅)𝑥) ∈ 𝐼 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐼)))
8 simpl 482 . . . 4 ((∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧 ∈ ran 𝐺((𝑧(2nd𝑅)𝑥) ∈ 𝐼 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐼)) → ∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼)
98ralimi 3082 . . 3 (∀𝑥𝐼 (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧 ∈ ran 𝐺((𝑧(2nd𝑅)𝑥) ∈ 𝐼 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐼)) → ∀𝑥𝐼𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼)
107, 9syl 17 . 2 ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → ∀𝑥𝐼𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼)
11 oveq1 7436 . . . 4 (𝑥 = 𝐴 → (𝑥𝐺𝑦) = (𝐴𝐺𝑦))
1211eleq1d 2825 . . 3 (𝑥 = 𝐴 → ((𝑥𝐺𝑦) ∈ 𝐼 ↔ (𝐴𝐺𝑦) ∈ 𝐼))
13 oveq2 7437 . . . 4 (𝑦 = 𝐵 → (𝐴𝐺𝑦) = (𝐴𝐺𝐵))
1413eleq1d 2825 . . 3 (𝑦 = 𝐵 → ((𝐴𝐺𝑦) ∈ 𝐼 ↔ (𝐴𝐺𝐵) ∈ 𝐼))
1512, 14rspc2v 3632 . 2 ((𝐴𝐼𝐵𝐼) → (∀𝑥𝐼𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 → (𝐴𝐺𝐵) ∈ 𝐼))
1610, 15mpan9 506 1 (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴𝐼𝐵𝐼)) → (𝐴𝐺𝐵) ∈ 𝐼)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087   = wceq 1540  wcel 2108  wral 3060  wss 3950  ran crn 5684  cfv 6559  (class class class)co 7429  1st c1st 8008  2nd c2nd 8009  GIdcgi 30499  RingOpscrngo 37879  Idlcidl 37992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5294  ax-nul 5304  ax-pow 5363  ax-pr 5430  ax-un 7751
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4906  df-br 5142  df-opab 5204  df-mpt 5224  df-id 5576  df-xp 5689  df-rel 5690  df-cnv 5691  df-co 5692  df-dm 5693  df-rn 5694  df-iota 6512  df-fun 6561  df-fv 6567  df-ov 7432  df-idl 37995
This theorem is referenced by:  idlsubcl  38008  intidl  38014  unichnidl  38016
  Copyright terms: Public domain W3C validator