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 35507
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 35437 . . . 4 (𝑅 ∈ CRingOps → 𝑅 ∈ RingOps)
2 ispridlc.1 . . . . 5 𝐺 = (1st𝑅)
3 ispridlc.2 . . . . 5 𝐻 = (2nd𝑅)
4 ispridlc.3 . . . . 5 𝑋 = ran 𝐺
52, 3, 4ispridl 35471 . . . 4 (𝑅 ∈ RingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))))
61, 5syl 17 . . 3 (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))))
7 snssi 4704 . . . . . . . . . . . . 13 (𝑎𝑋 → {𝑎} ⊆ 𝑋)
82, 4igenidl 35500 . . . . . . . . . . . . 13 ((𝑅 ∈ RingOps ∧ {𝑎} ⊆ 𝑋) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
91, 7, 8syl2an 598 . . . . . . . . . . . 12 ((𝑅 ∈ CRingOps ∧ 𝑎𝑋) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
109adantrr 716 . . . . . . . . . . 11 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
11 snssi 4704 . . . . . . . . . . . . 13 (𝑏𝑋 → {𝑏} ⊆ 𝑋)
122, 4igenidl 35500 . . . . . . . . . . . . 13 ((𝑅 ∈ RingOps ∧ {𝑏} ⊆ 𝑋) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
131, 11, 12syl2an 598 . . . . . . . . . . . 12 ((𝑅 ∈ CRingOps ∧ 𝑏𝑋) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
1413adantrl 715 . . . . . . . . . . 11 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
15 raleq 3361 . . . . . . . . . . . . 13 (𝑟 = (𝑅 IdlGen {𝑎}) → (∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃))
16 sseq1 3943 . . . . . . . . . . . . . 14 (𝑟 = (𝑅 IdlGen {𝑎}) → (𝑟𝑃 ↔ (𝑅 IdlGen {𝑎}) ⊆ 𝑃))
1716orbi1d 914 . . . . . . . . . . . . 13 (𝑟 = (𝑅 IdlGen {𝑎}) → ((𝑟𝑃𝑠𝑃) ↔ ((𝑅 IdlGen {𝑎}) ⊆ 𝑃𝑠𝑃)))
1815, 17imbi12d 348 . . . . . . . . . . . 12 (𝑟 = (𝑅 IdlGen {𝑎}) → ((∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) ↔ (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃𝑠𝑃))))
19 raleq 3361 . . . . . . . . . . . . . 14 (𝑠 = (𝑅 IdlGen {𝑏}) → (∀𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
2019ralbidv 3165 . . . . . . . . . . . . 13 (𝑠 = (𝑅 IdlGen {𝑏}) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
21 sseq1 3943 . . . . . . . . . . . . . 14 (𝑠 = (𝑅 IdlGen {𝑏}) → (𝑠𝑃 ↔ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))
2221orbi2d 913 . . . . . . . . . . . . 13 (𝑠 = (𝑅 IdlGen {𝑏}) → (((𝑅 IdlGen {𝑎}) ⊆ 𝑃𝑠𝑃) ↔ ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃)))
2320, 22imbi12d 348 . . . . . . . . . . . 12 (𝑠 = (𝑅 IdlGen {𝑏}) → ((∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃𝑠𝑃)) ↔ (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
2418, 23rspc2v 3584 . . . . . . . . . . 11 (((𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅) ∧ (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
2510, 14, 24syl2anc 587 . . . . . . . . . 10 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
2625adantlr 714 . . . . . . . . 9 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
272, 3, 4prnc 35504 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ CRingOps ∧ 𝑎𝑋) → (𝑅 IdlGen {𝑎}) = {𝑥𝑋 ∣ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)})
28 df-rab 3118 . . . . . . . . . . . . . . . . . . 19 {𝑥𝑋 ∣ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)} = {𝑥 ∣ (𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎))}
2927, 28eqtrdi 2852 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ CRingOps ∧ 𝑎𝑋) → (𝑅 IdlGen {𝑎}) = {𝑥 ∣ (𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎))})
3029abeq2d 2927 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ CRingOps ∧ 𝑎𝑋) → (𝑥 ∈ (𝑅 IdlGen {𝑎}) ↔ (𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎))))
3130adantrr 716 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → (𝑥 ∈ (𝑅 IdlGen {𝑎}) ↔ (𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎))))
322, 3, 4prnc 35504 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ CRingOps ∧ 𝑏𝑋) → (𝑅 IdlGen {𝑏}) = {𝑦𝑋 ∣ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏)})
33 df-rab 3118 . . . . . . . . . . . . . . . . . . 19 {𝑦𝑋 ∣ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏)} = {𝑦 ∣ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))}
3432, 33eqtrdi 2852 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ CRingOps ∧ 𝑏𝑋) → (𝑅 IdlGen {𝑏}) = {𝑦 ∣ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))})
3534abeq2d 2927 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ CRingOps ∧ 𝑏𝑋) → (𝑦 ∈ (𝑅 IdlGen {𝑏}) ↔ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))))
3635adantrl 715 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → (𝑦 ∈ (𝑅 IdlGen {𝑏}) ↔ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))))
3731, 36anbi12d 633 . . . . . . . . . . . . . . 15 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) ↔ ((𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏)))))
3837adantlr 714 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) ↔ ((𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏)))))
3938adantr 484 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) ↔ ((𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏)))))
40 reeanv 3323 . . . . . . . . . . . . . . . 16 (∃𝑟𝑋𝑠𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) ↔ (∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏)))
4140anbi2i 625 . . . . . . . . . . . . . . 15 (((𝑥𝑋𝑦𝑋) ∧ ∃𝑟𝑋𝑠𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥𝑋𝑦𝑋) ∧ (∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))))
42 an4 655 . . . . . . . . . . . . . . 15 (((𝑥𝑋𝑦𝑋) ∧ (∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))))
4341, 42bitri 278 . . . . . . . . . . . . . 14 (((𝑥𝑋𝑦𝑋) ∧ ∃𝑟𝑋𝑠𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))))
442, 3, 4crngm4 35440 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ CRingOps ∧ (𝑟𝑋𝑠𝑋) ∧ (𝑎𝑋𝑏𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
45443com23 1123 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
46453expa 1115 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
4746adantllr 718 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
4847adantlr 714 . . . . . . . . . . . . . . . . . 18 (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
492, 3, 4rngocl 35338 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 ∈ RingOps ∧ 𝑟𝑋𝑠𝑋) → (𝑟𝐻𝑠) ∈ 𝑋)
501, 49syl3an1 1160 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ CRingOps ∧ 𝑟𝑋𝑠𝑋) → (𝑟𝐻𝑠) ∈ 𝑋)
51503expb 1117 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ CRingOps ∧ (𝑟𝑋𝑠𝑋)) → (𝑟𝐻𝑠) ∈ 𝑋)
5251adantlr 714 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑟𝑋𝑠𝑋)) → (𝑟𝐻𝑠) ∈ 𝑋)
5352adantlr 714 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝑋𝑠𝑋)) → (𝑟𝐻𝑠) ∈ 𝑋)
542, 3, 4idllmulcl 35457 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 ∈ RingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ ((𝑎𝐻𝑏) ∈ 𝑃 ∧ (𝑟𝐻𝑠) ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
551, 54sylanl1 679 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ ((𝑎𝐻𝑏) ∈ 𝑃 ∧ (𝑟𝐻𝑠) ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
5655anassrs 471 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝐻𝑠) ∈ 𝑋) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
5753, 56syldan 594 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
5857adantllr 718 . . . . . . . . . . . . . . . . . 18 (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
5948, 58eqeltrrd 2894 . . . . . . . . . . . . . . . . 17 (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)) ∈ 𝑃)
60 oveq12 7148 . . . . . . . . . . . . . . . . . 18 ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → (𝑥𝐻𝑦) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
6160eleq1d 2877 . . . . . . . . . . . . . . . . 17 ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → ((𝑥𝐻𝑦) ∈ 𝑃 ↔ ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)) ∈ 𝑃))
6259, 61syl5ibrcom 250 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → (𝑥𝐻𝑦) ∈ 𝑃))
6362rexlimdvva 3256 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → (∃𝑟𝑋𝑠𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → (𝑥𝐻𝑦) ∈ 𝑃))
6463adantld 494 . . . . . . . . . . . . . 14 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → (((𝑥𝑋𝑦𝑋) ∧ ∃𝑟𝑋𝑠𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏))) → (𝑥𝐻𝑦) ∈ 𝑃))
6543, 64syl5bir 246 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → (((𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))) → (𝑥𝐻𝑦) ∈ 𝑃))
6639, 65sylbid 243 . . . . . . . . . . . 12 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) → (𝑥𝐻𝑦) ∈ 𝑃))
6766ralrimivv 3158 . . . . . . . . . . 11 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃)
6867ex 416 . . . . . . . . . 10 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) → ((𝑎𝐻𝑏) ∈ 𝑃 → ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
692, 4igenss 35499 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ RingOps ∧ {𝑎} ⊆ 𝑋) → {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
701, 7, 69syl2an 598 . . . . . . . . . . . . . . 15 ((𝑅 ∈ CRingOps ∧ 𝑎𝑋) → {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
71 vex 3447 . . . . . . . . . . . . . . . 16 𝑎 ∈ V
7271snss 4682 . . . . . . . . . . . . . . 15 (𝑎 ∈ (𝑅 IdlGen {𝑎}) ↔ {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
7370, 72sylibr 237 . . . . . . . . . . . . . 14 ((𝑅 ∈ CRingOps ∧ 𝑎𝑋) → 𝑎 ∈ (𝑅 IdlGen {𝑎}))
7473adantrr 716 . . . . . . . . . . . . 13 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → 𝑎 ∈ (𝑅 IdlGen {𝑎}))
75 ssel 3911 . . . . . . . . . . . . 13 ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 → (𝑎 ∈ (𝑅 IdlGen {𝑎}) → 𝑎𝑃))
7674, 75syl5com 31 . . . . . . . . . . . 12 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃𝑎𝑃))
772, 4igenss 35499 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ RingOps ∧ {𝑏} ⊆ 𝑋) → {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
781, 11, 77syl2an 598 . . . . . . . . . . . . . . 15 ((𝑅 ∈ CRingOps ∧ 𝑏𝑋) → {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
79 vex 3447 . . . . . . . . . . . . . . . 16 𝑏 ∈ V
8079snss 4682 . . . . . . . . . . . . . . 15 (𝑏 ∈ (𝑅 IdlGen {𝑏}) ↔ {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
8178, 80sylibr 237 . . . . . . . . . . . . . 14 ((𝑅 ∈ CRingOps ∧ 𝑏𝑋) → 𝑏 ∈ (𝑅 IdlGen {𝑏}))
8281adantrl 715 . . . . . . . . . . . . 13 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → 𝑏 ∈ (𝑅 IdlGen {𝑏}))
83 ssel 3911 . . . . . . . . . . . . 13 ((𝑅 IdlGen {𝑏}) ⊆ 𝑃 → (𝑏 ∈ (𝑅 IdlGen {𝑏}) → 𝑏𝑃))
8482, 83syl5com 31 . . . . . . . . . . . 12 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → ((𝑅 IdlGen {𝑏}) ⊆ 𝑃𝑏𝑃))
8576, 84orim12d 962 . . . . . . . . . . 11 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → (((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃) → (𝑎𝑃𝑏𝑃)))
8685adantlr 714 . . . . . . . . . 10 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) → (((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃) → (𝑎𝑃𝑏𝑃)))
8768, 86imim12d 81 . . . . . . . . 9 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) → ((∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃)) → ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
8826, 87syld 47 . . . . . . . 8 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) → ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
8988ralrimdvva 3162 . . . . . . 7 ((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) → ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
9089ex 416 . . . . . 6 (𝑅 ∈ CRingOps → (𝑃 ∈ (Idl‘𝑅) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) → ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))))
9190adantrd 495 . . . . 5 (𝑅 ∈ CRingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) → ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))))
9291imdistand 574 . . . 4 (𝑅 ∈ CRingOps → (((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))) → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))))
93 df-3an 1086 . . . 4 ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))) ↔ ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))))
94 df-3an 1086 . . . 4 ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) ↔ ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
9592, 93, 943imtr4g 299 . . 3 (𝑅 ∈ CRingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))) → (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))))
966, 95sylbid 243 . 2 (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) → (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))))
972, 3, 4ispridl2 35475 . . . 4 ((𝑅 ∈ RingOps ∧ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))) → 𝑃 ∈ (PrIdl‘𝑅))
9897ex 416 . . 3 (𝑅 ∈ RingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → 𝑃 ∈ (PrIdl‘𝑅)))
991, 98syl 17 . 2 (𝑅 ∈ CRingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → 𝑃 ∈ (PrIdl‘𝑅)))
10096, 99impbid 215 1 (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wo 844  w3a 1084   = wceq 1538  wcel 2112  {cab 2779  wne 2990  wral 3109  wrex 3110  {crab 3113  wss 3884  {csn 4528  ran crn 5524  cfv 6328  (class class class)co 7139  1st c1st 7673  2nd c2nd 7674  RingOpscrngo 35331  CRingOpsccring 35430  Idlcidl 35444  PrIdlcpridl 35445   IdlGen cigen 35496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-1st 7675  df-2nd 7676  df-grpo 28280  df-gid 28281  df-ginv 28282  df-ablo 28332  df-ass 35280  df-exid 35282  df-mgmOLD 35286  df-sgrOLD 35298  df-mndo 35304  df-rngo 35332  df-com2 35427  df-crngo 35431  df-idl 35447  df-pridl 35448  df-igen 35497
This theorem is referenced by:  pridlc  35508  isdmn3  35511
  Copyright terms: Public domain W3C validator