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

Theorem isidlc 34713
Description: The predicate "is an ideal of the commutative ring 𝑅". (Contributed by Jeff Madsen, 10-Jun-2010.)
Hypotheses
Ref Expression
idlval.1 𝐺 = (1st𝑅)
idlval.2 𝐻 = (2nd𝑅)
idlval.3 𝑋 = ran 𝐺
idlval.4 𝑍 = (GId‘𝐺)
Assertion
Ref Expression
isidlc (𝑅 ∈ CRingOps → (𝐼 ∈ (Idl‘𝑅) ↔ (𝐼𝑋𝑍𝐼 ∧ ∀𝑥𝐼 (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧𝑋 (𝑧𝐻𝑥) ∈ 𝐼))))
Distinct variable groups:   𝑥,𝑅,𝑦,𝑧   𝑧,𝑋   𝑥,𝐼,𝑦,𝑧   𝑥,𝑋
Allowed substitution hints:   𝐺(𝑥,𝑦,𝑧)   𝐻(𝑥,𝑦,𝑧)   𝑋(𝑦)   𝑍(𝑥,𝑦,𝑧)

Proof of Theorem isidlc
StepHypRef Expression
1 crngorngo 34698 . . 3 (𝑅 ∈ CRingOps → 𝑅 ∈ RingOps)
2 idlval.1 . . . 4 𝐺 = (1st𝑅)
3 idlval.2 . . . 4 𝐻 = (2nd𝑅)
4 idlval.3 . . . 4 𝑋 = ran 𝐺
5 idlval.4 . . . 4 𝑍 = (GId‘𝐺)
62, 3, 4, 5isidl 34712 . . 3 (𝑅 ∈ RingOps → (𝐼 ∈ (Idl‘𝑅) ↔ (𝐼𝑋𝑍𝐼 ∧ ∀𝑥𝐼 (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧𝑋 ((𝑧𝐻𝑥) ∈ 𝐼 ∧ (𝑥𝐻𝑧) ∈ 𝐼)))))
71, 6syl 17 . 2 (𝑅 ∈ CRingOps → (𝐼 ∈ (Idl‘𝑅) ↔ (𝐼𝑋𝑍𝐼 ∧ ∀𝑥𝐼 (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧𝑋 ((𝑧𝐻𝑥) ∈ 𝐼 ∧ (𝑥𝐻𝑧) ∈ 𝐼)))))
8 ssel2 3852 . . . . . . . 8 ((𝐼𝑋𝑥𝐼) → 𝑥𝑋)
92, 3, 4crngocom 34699 . . . . . . . . . . . . . . 15 ((𝑅 ∈ CRingOps ∧ 𝑥𝑋𝑧𝑋) → (𝑥𝐻𝑧) = (𝑧𝐻𝑥))
109eleq1d 2847 . . . . . . . . . . . . . 14 ((𝑅 ∈ CRingOps ∧ 𝑥𝑋𝑧𝑋) → ((𝑥𝐻𝑧) ∈ 𝐼 ↔ (𝑧𝐻𝑥) ∈ 𝐼))
1110biimprd 240 . . . . . . . . . . . . 13 ((𝑅 ∈ CRingOps ∧ 𝑥𝑋𝑧𝑋) → ((𝑧𝐻𝑥) ∈ 𝐼 → (𝑥𝐻𝑧) ∈ 𝐼))
12113expa 1098 . . . . . . . . . . . 12 (((𝑅 ∈ CRingOps ∧ 𝑥𝑋) ∧ 𝑧𝑋) → ((𝑧𝐻𝑥) ∈ 𝐼 → (𝑥𝐻𝑧) ∈ 𝐼))
1312pm4.71d 554 . . . . . . . . . . 11 (((𝑅 ∈ CRingOps ∧ 𝑥𝑋) ∧ 𝑧𝑋) → ((𝑧𝐻𝑥) ∈ 𝐼 ↔ ((𝑧𝐻𝑥) ∈ 𝐼 ∧ (𝑥𝐻𝑧) ∈ 𝐼)))
1413bicomd 215 . . . . . . . . . 10 (((𝑅 ∈ CRingOps ∧ 𝑥𝑋) ∧ 𝑧𝑋) → (((𝑧𝐻𝑥) ∈ 𝐼 ∧ (𝑥𝐻𝑧) ∈ 𝐼) ↔ (𝑧𝐻𝑥) ∈ 𝐼))
1514ralbidva 3143 . . . . . . . . 9 ((𝑅 ∈ CRingOps ∧ 𝑥𝑋) → (∀𝑧𝑋 ((𝑧𝐻𝑥) ∈ 𝐼 ∧ (𝑥𝐻𝑧) ∈ 𝐼) ↔ ∀𝑧𝑋 (𝑧𝐻𝑥) ∈ 𝐼))
1615anbi2d 619 . . . . . . . 8 ((𝑅 ∈ CRingOps ∧ 𝑥𝑋) → ((∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧𝑋 ((𝑧𝐻𝑥) ∈ 𝐼 ∧ (𝑥𝐻𝑧) ∈ 𝐼)) ↔ (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧𝑋 (𝑧𝐻𝑥) ∈ 𝐼)))
178, 16sylan2 583 . . . . . . 7 ((𝑅 ∈ CRingOps ∧ (𝐼𝑋𝑥𝐼)) → ((∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧𝑋 ((𝑧𝐻𝑥) ∈ 𝐼 ∧ (𝑥𝐻𝑧) ∈ 𝐼)) ↔ (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧𝑋 (𝑧𝐻𝑥) ∈ 𝐼)))
1817anassrs 460 . . . . . 6 (((𝑅 ∈ CRingOps ∧ 𝐼𝑋) ∧ 𝑥𝐼) → ((∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧𝑋 ((𝑧𝐻𝑥) ∈ 𝐼 ∧ (𝑥𝐻𝑧) ∈ 𝐼)) ↔ (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧𝑋 (𝑧𝐻𝑥) ∈ 𝐼)))
1918ralbidva 3143 . . . . 5 ((𝑅 ∈ CRingOps ∧ 𝐼𝑋) → (∀𝑥𝐼 (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧𝑋 ((𝑧𝐻𝑥) ∈ 𝐼 ∧ (𝑥𝐻𝑧) ∈ 𝐼)) ↔ ∀𝑥𝐼 (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧𝑋 (𝑧𝐻𝑥) ∈ 𝐼)))
2019adantrr 704 . . . 4 ((𝑅 ∈ CRingOps ∧ (𝐼𝑋𝑍𝐼)) → (∀𝑥𝐼 (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧𝑋 ((𝑧𝐻𝑥) ∈ 𝐼 ∧ (𝑥𝐻𝑧) ∈ 𝐼)) ↔ ∀𝑥𝐼 (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧𝑋 (𝑧𝐻𝑥) ∈ 𝐼)))
2120pm5.32da 571 . . 3 (𝑅 ∈ CRingOps → (((𝐼𝑋𝑍𝐼) ∧ ∀𝑥𝐼 (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧𝑋 ((𝑧𝐻𝑥) ∈ 𝐼 ∧ (𝑥𝐻𝑧) ∈ 𝐼))) ↔ ((𝐼𝑋𝑍𝐼) ∧ ∀𝑥𝐼 (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧𝑋 (𝑧𝐻𝑥) ∈ 𝐼))))
22 df-3an 1070 . . 3 ((𝐼𝑋𝑍𝐼 ∧ ∀𝑥𝐼 (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧𝑋 ((𝑧𝐻𝑥) ∈ 𝐼 ∧ (𝑥𝐻𝑧) ∈ 𝐼))) ↔ ((𝐼𝑋𝑍𝐼) ∧ ∀𝑥𝐼 (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧𝑋 ((𝑧𝐻𝑥) ∈ 𝐼 ∧ (𝑥𝐻𝑧) ∈ 𝐼))))
23 df-3an 1070 . . 3 ((𝐼𝑋𝑍𝐼 ∧ ∀𝑥𝐼 (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧𝑋 (𝑧𝐻𝑥) ∈ 𝐼)) ↔ ((𝐼𝑋𝑍𝐼) ∧ ∀𝑥𝐼 (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧𝑋 (𝑧𝐻𝑥) ∈ 𝐼)))
2421, 22, 233bitr4g 306 . 2 (𝑅 ∈ CRingOps → ((𝐼𝑋𝑍𝐼 ∧ ∀𝑥𝐼 (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧𝑋 ((𝑧𝐻𝑥) ∈ 𝐼 ∧ (𝑥𝐻𝑧) ∈ 𝐼))) ↔ (𝐼𝑋𝑍𝐼 ∧ ∀𝑥𝐼 (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧𝑋 (𝑧𝐻𝑥) ∈ 𝐼))))
257, 24bitrd 271 1 (𝑅 ∈ CRingOps → (𝐼 ∈ (Idl‘𝑅) ↔ (𝐼𝑋𝑍𝐼 ∧ ∀𝑥𝐼 (∀𝑦𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧𝑋 (𝑧𝐻𝑥) ∈ 𝐼))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387  w3a 1068   = wceq 1507  wcel 2048  wral 3085  wss 3828  ran crn 5405  cfv 6186  (class class class)co 6974  1st c1st 7496  2nd c2nd 7497  GIdcgi 28038  RingOpscrngo 34592  CRingOpsccring 34691  Idlcidl 34705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-sep 5058  ax-nul 5065  ax-pow 5117  ax-pr 5184  ax-un 7277
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ral 3090  df-rex 3091  df-rab 3094  df-v 3414  df-sbc 3681  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-nul 4178  df-if 4349  df-pw 4422  df-sn 4440  df-pr 4442  df-op 4446  df-uni 4711  df-br 4928  df-opab 4990  df-mpt 5007  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-iota 6150  df-fun 6188  df-fv 6194  df-ov 6977  df-1st 7498  df-2nd 7499  df-rngo 34593  df-com2 34688  df-crngo 34692  df-idl 34708
This theorem is referenced by:  prnc  34765
  Copyright terms: Public domain W3C validator