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

Theorem ispridlc 32837
Description: The predicate "is a prime ideal". Alternate definition for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.)
Hypotheses
Ref Expression
ispridlc.1 𝐺 = (1st𝑅)
ispridlc.2 𝐻 = (2nd𝑅)
ispridlc.3 𝑋 = ran 𝐺
Assertion
Ref Expression
ispridlc (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))))
Distinct variable groups:   𝑅,𝑎,𝑏   𝑃,𝑎,𝑏   𝑋,𝑎,𝑏   𝐻,𝑎,𝑏
Allowed substitution hints:   𝐺(𝑎,𝑏)

Proof of Theorem ispridlc
Dummy variables 𝑥 𝑦 𝑟 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 crngorngo 32767 . . . 4 (𝑅 ∈ CRingOps → 𝑅 ∈ RingOps)
2 ispridlc.1 . . . . 5 𝐺 = (1st𝑅)
3 ispridlc.2 . . . . 5 𝐻 = (2nd𝑅)
4 ispridlc.3 . . . . 5 𝑋 = ran 𝐺
52, 3, 4ispridl 32801 . . . 4 (𝑅 ∈ RingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))))
61, 5syl 17 . . 3 (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))))
7 snssi 4274 . . . . . . . . . . . . 13 (𝑎𝑋 → {𝑎} ⊆ 𝑋)
82, 4igenidl 32830 . . . . . . . . . . . . 13 ((𝑅 ∈ RingOps ∧ {𝑎} ⊆ 𝑋) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
91, 7, 8syl2an 492 . . . . . . . . . . . 12 ((𝑅 ∈ CRingOps ∧ 𝑎𝑋) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
109adantrr 748 . . . . . . . . . . 11 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
11 snssi 4274 . . . . . . . . . . . . 13 (𝑏𝑋 → {𝑏} ⊆ 𝑋)
122, 4igenidl 32830 . . . . . . . . . . . . 13 ((𝑅 ∈ RingOps ∧ {𝑏} ⊆ 𝑋) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
131, 11, 12syl2an 492 . . . . . . . . . . . 12 ((𝑅 ∈ CRingOps ∧ 𝑏𝑋) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
1413adantrl 747 . . . . . . . . . . 11 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
15 raleq 3109 . . . . . . . . . . . . 13 (𝑟 = (𝑅 IdlGen {𝑎}) → (∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃))
16 sseq1 3583 . . . . . . . . . . . . . 14 (𝑟 = (𝑅 IdlGen {𝑎}) → (𝑟𝑃 ↔ (𝑅 IdlGen {𝑎}) ⊆ 𝑃))
1716orbi1d 734 . . . . . . . . . . . . 13 (𝑟 = (𝑅 IdlGen {𝑎}) → ((𝑟𝑃𝑠𝑃) ↔ ((𝑅 IdlGen {𝑎}) ⊆ 𝑃𝑠𝑃)))
1815, 17imbi12d 332 . . . . . . . . . . . 12 (𝑟 = (𝑅 IdlGen {𝑎}) → ((∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) ↔ (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃𝑠𝑃))))
19 raleq 3109 . . . . . . . . . . . . . 14 (𝑠 = (𝑅 IdlGen {𝑏}) → (∀𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
2019ralbidv 2963 . . . . . . . . . . . . 13 (𝑠 = (𝑅 IdlGen {𝑏}) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
21 sseq1 3583 . . . . . . . . . . . . . 14 (𝑠 = (𝑅 IdlGen {𝑏}) → (𝑠𝑃 ↔ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))
2221orbi2d 733 . . . . . . . . . . . . 13 (𝑠 = (𝑅 IdlGen {𝑏}) → (((𝑅 IdlGen {𝑎}) ⊆ 𝑃𝑠𝑃) ↔ ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃)))
2320, 22imbi12d 332 . . . . . . . . . . . 12 (𝑠 = (𝑅 IdlGen {𝑏}) → ((∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃𝑠𝑃)) ↔ (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
2418, 23rspc2v 3287 . . . . . . . . . . 11 (((𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅) ∧ (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
2510, 14, 24syl2anc 690 . . . . . . . . . 10 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
2625adantlr 746 . . . . . . . . 9 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
272, 3, 4prnc 32834 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ CRingOps ∧ 𝑎𝑋) → (𝑅 IdlGen {𝑎}) = {𝑥𝑋 ∣ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)})
28 df-rab 2899 . . . . . . . . . . . . . . . . . . 19 {𝑥𝑋 ∣ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)} = {𝑥 ∣ (𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎))}
2927, 28syl6eq 2654 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ CRingOps ∧ 𝑎𝑋) → (𝑅 IdlGen {𝑎}) = {𝑥 ∣ (𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎))})
3029abeq2d 2715 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ CRingOps ∧ 𝑎𝑋) → (𝑥 ∈ (𝑅 IdlGen {𝑎}) ↔ (𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎))))
3130adantrr 748 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → (𝑥 ∈ (𝑅 IdlGen {𝑎}) ↔ (𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎))))
322, 3, 4prnc 32834 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ CRingOps ∧ 𝑏𝑋) → (𝑅 IdlGen {𝑏}) = {𝑦𝑋 ∣ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏)})
33 df-rab 2899 . . . . . . . . . . . . . . . . . . 19 {𝑦𝑋 ∣ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏)} = {𝑦 ∣ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))}
3432, 33syl6eq 2654 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ CRingOps ∧ 𝑏𝑋) → (𝑅 IdlGen {𝑏}) = {𝑦 ∣ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))})
3534abeq2d 2715 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ CRingOps ∧ 𝑏𝑋) → (𝑦 ∈ (𝑅 IdlGen {𝑏}) ↔ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))))
3635adantrl 747 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → (𝑦 ∈ (𝑅 IdlGen {𝑏}) ↔ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))))
3731, 36anbi12d 742 . . . . . . . . . . . . . . 15 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) ↔ ((𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏)))))
3837adantlr 746 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) ↔ ((𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏)))))
3938adantr 479 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) ↔ ((𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏)))))
40 reeanv 3080 . . . . . . . . . . . . . . . 16 (∃𝑟𝑋𝑠𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) ↔ (∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏)))
4140anbi2i 725 . . . . . . . . . . . . . . 15 (((𝑥𝑋𝑦𝑋) ∧ ∃𝑟𝑋𝑠𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥𝑋𝑦𝑋) ∧ (∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))))
42 an4 860 . . . . . . . . . . . . . . 15 (((𝑥𝑋𝑦𝑋) ∧ (∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))))
4341, 42bitri 262 . . . . . . . . . . . . . 14 (((𝑥𝑋𝑦𝑋) ∧ ∃𝑟𝑋𝑠𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))))
442, 3, 4crngm4 32770 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ CRingOps ∧ (𝑟𝑋𝑠𝑋) ∧ (𝑎𝑋𝑏𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
45443com23 1262 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
46453expa 1256 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
4746adantllr 750 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
4847adantlr 746 . . . . . . . . . . . . . . . . . 18 (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
492, 3, 4rngocl 32668 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 ∈ RingOps ∧ 𝑟𝑋𝑠𝑋) → (𝑟𝐻𝑠) ∈ 𝑋)
501, 49syl3an1 1350 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ CRingOps ∧ 𝑟𝑋𝑠𝑋) → (𝑟𝐻𝑠) ∈ 𝑋)
51503expb 1257 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ CRingOps ∧ (𝑟𝑋𝑠𝑋)) → (𝑟𝐻𝑠) ∈ 𝑋)
5251adantlr 746 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑟𝑋𝑠𝑋)) → (𝑟𝐻𝑠) ∈ 𝑋)
5352adantlr 746 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝑋𝑠𝑋)) → (𝑟𝐻𝑠) ∈ 𝑋)
542, 3, 4idllmulcl 32787 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 ∈ RingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ ((𝑎𝐻𝑏) ∈ 𝑃 ∧ (𝑟𝐻𝑠) ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
551, 54sylanl1 679 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ ((𝑎𝐻𝑏) ∈ 𝑃 ∧ (𝑟𝐻𝑠) ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
5655anassrs 677 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝐻𝑠) ∈ 𝑋) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
5753, 56syldan 485 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
5857adantllr 750 . . . . . . . . . . . . . . . . . 18 (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
5948, 58eqeltrrd 2683 . . . . . . . . . . . . . . . . 17 (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)) ∈ 𝑃)
60 oveq12 6531 . . . . . . . . . . . . . . . . . 18 ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → (𝑥𝐻𝑦) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
6160eleq1d 2666 . . . . . . . . . . . . . . . . 17 ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → ((𝑥𝐻𝑦) ∈ 𝑃 ↔ ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)) ∈ 𝑃))
6259, 61syl5ibrcom 235 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → (𝑥𝐻𝑦) ∈ 𝑃))
6362rexlimdvva 3014 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → (∃𝑟𝑋𝑠𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → (𝑥𝐻𝑦) ∈ 𝑃))
6463adantld 481 . . . . . . . . . . . . . 14 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → (((𝑥𝑋𝑦𝑋) ∧ ∃𝑟𝑋𝑠𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏))) → (𝑥𝐻𝑦) ∈ 𝑃))
6543, 64syl5bir 231 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → (((𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))) → (𝑥𝐻𝑦) ∈ 𝑃))
6639, 65sylbid 228 . . . . . . . . . . . 12 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) → (𝑥𝐻𝑦) ∈ 𝑃))
6766ralrimivv 2947 . . . . . . . . . . 11 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃)
6867ex 448 . . . . . . . . . 10 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) → ((𝑎𝐻𝑏) ∈ 𝑃 → ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
692, 4igenss 32829 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ RingOps ∧ {𝑎} ⊆ 𝑋) → {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
701, 7, 69syl2an 492 . . . . . . . . . . . . . . 15 ((𝑅 ∈ CRingOps ∧ 𝑎𝑋) → {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
71 vex 3170 . . . . . . . . . . . . . . . 16 𝑎 ∈ V
7271snss 4253 . . . . . . . . . . . . . . 15 (𝑎 ∈ (𝑅 IdlGen {𝑎}) ↔ {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
7370, 72sylibr 222 . . . . . . . . . . . . . 14 ((𝑅 ∈ CRingOps ∧ 𝑎𝑋) → 𝑎 ∈ (𝑅 IdlGen {𝑎}))
7473adantrr 748 . . . . . . . . . . . . 13 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → 𝑎 ∈ (𝑅 IdlGen {𝑎}))
75 ssel 3556 . . . . . . . . . . . . 13 ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 → (𝑎 ∈ (𝑅 IdlGen {𝑎}) → 𝑎𝑃))
7674, 75syl5com 31 . . . . . . . . . . . 12 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃𝑎𝑃))
772, 4igenss 32829 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ RingOps ∧ {𝑏} ⊆ 𝑋) → {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
781, 11, 77syl2an 492 . . . . . . . . . . . . . . 15 ((𝑅 ∈ CRingOps ∧ 𝑏𝑋) → {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
79 vex 3170 . . . . . . . . . . . . . . . 16 𝑏 ∈ V
8079snss 4253 . . . . . . . . . . . . . . 15 (𝑏 ∈ (𝑅 IdlGen {𝑏}) ↔ {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
8178, 80sylibr 222 . . . . . . . . . . . . . 14 ((𝑅 ∈ CRingOps ∧ 𝑏𝑋) → 𝑏 ∈ (𝑅 IdlGen {𝑏}))
8281adantrl 747 . . . . . . . . . . . . 13 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → 𝑏 ∈ (𝑅 IdlGen {𝑏}))
83 ssel 3556 . . . . . . . . . . . . 13 ((𝑅 IdlGen {𝑏}) ⊆ 𝑃 → (𝑏 ∈ (𝑅 IdlGen {𝑏}) → 𝑏𝑃))
8482, 83syl5com 31 . . . . . . . . . . . 12 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → ((𝑅 IdlGen {𝑏}) ⊆ 𝑃𝑏𝑃))
8576, 84orim12d 878 . . . . . . . . . . 11 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → (((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃) → (𝑎𝑃𝑏𝑃)))
8685adantlr 746 . . . . . . . . . 10 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) → (((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃) → (𝑎𝑃𝑏𝑃)))
8768, 86imim12d 78 . . . . . . . . 9 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) → ((∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃)) → ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
8826, 87syld 45 . . . . . . . 8 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) → ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
8988ralrimdvva 2951 . . . . . . 7 ((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) → ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
9089ex 448 . . . . . 6 (𝑅 ∈ CRingOps → (𝑃 ∈ (Idl‘𝑅) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) → ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))))
9190adantrd 482 . . . . 5 (𝑅 ∈ CRingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) → ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))))
9291imdistand 723 . . . 4 (𝑅 ∈ CRingOps → (((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))) → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))))
93 df-3an 1032 . . . 4 ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))) ↔ ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))))
94 df-3an 1032 . . . 4 ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) ↔ ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
9592, 93, 943imtr4g 283 . . 3 (𝑅 ∈ CRingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))) → (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))))
966, 95sylbid 228 . 2 (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) → (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))))
972, 3, 4ispridl2 32805 . . . 4 ((𝑅 ∈ RingOps ∧ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))) → 𝑃 ∈ (PrIdl‘𝑅))
9897ex 448 . . 3 (𝑅 ∈ RingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → 𝑃 ∈ (PrIdl‘𝑅)))
991, 98syl 17 . 2 (𝑅 ∈ CRingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → 𝑃 ∈ (PrIdl‘𝑅)))
10096, 99impbid 200 1 (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wcel 1975  {cab 2590  wne 2774  wral 2890  wrex 2891  {crab 2894  wss 3534  {csn 4119  ran crn 5024  cfv 5785  (class class class)co 6522  1st c1st 7029  2nd c2nd 7030  RingOpscrngo 32661  CRingOpsccring 32760  Idlcidl 32774  PrIdlcpridl 32775   IdlGen cigen 32826
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584  ax-rep 4688  ax-sep 4698  ax-nul 4707  ax-pow 4759  ax-pr 4823  ax-un 6819
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2456  df-mo 2457  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-ne 2776  df-ral 2895  df-rex 2896  df-reu 2897  df-rmo 2898  df-rab 2899  df-v 3169  df-sbc 3397  df-csb 3494  df-dif 3537  df-un 3539  df-in 3541  df-ss 3548  df-nul 3869  df-if 4031  df-pw 4104  df-sn 4120  df-pr 4122  df-op 4126  df-uni 4362  df-int 4400  df-iun 4446  df-br 4573  df-opab 4633  df-mpt 4634  df-id 4938  df-xp 5029  df-rel 5030  df-cnv 5031  df-co 5032  df-dm 5033  df-rn 5034  df-res 5035  df-ima 5036  df-iota 5749  df-fun 5787  df-fn 5788  df-f 5789  df-f1 5790  df-fo 5791  df-f1o 5792  df-fv 5793  df-riota 6484  df-ov 6525  df-oprab 6526  df-mpt2 6527  df-1st 7031  df-2nd 7032  df-grpo 26492  df-gid 26493  df-ginv 26494  df-ablo 26547  df-ass 32610  df-exid 32612  df-mgmOLD 32616  df-sgrOLD 32628  df-mndo 32634  df-rngo 32662  df-com2 32757  df-crngo 32761  df-idl 32777  df-pridl 32778  df-igen 32827
This theorem is referenced by:  pridlc  32838  isdmn3  32841
  Copyright terms: Public domain W3C validator