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 38057
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 37987 . . . 4 (𝑅 ∈ CRingOps → 𝑅 ∈ RingOps)
2 ispridlc.1 . . . . 5 𝐺 = (1st𝑅)
3 ispridlc.2 . . . . 5 𝐻 = (2nd𝑅)
4 ispridlc.3 . . . . 5 𝑋 = ran 𝐺
52, 3, 4ispridl 38021 . . . 4 (𝑅 ∈ RingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))))
61, 5syl 17 . . 3 (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))))
7 snssi 4813 . . . . . . . . . . . . 13 (𝑎𝑋 → {𝑎} ⊆ 𝑋)
82, 4igenidl 38050 . . . . . . . . . . . . 13 ((𝑅 ∈ RingOps ∧ {𝑎} ⊆ 𝑋) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
91, 7, 8syl2an 596 . . . . . . . . . . . 12 ((𝑅 ∈ CRingOps ∧ 𝑎𝑋) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
109adantrr 717 . . . . . . . . . . 11 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
11 snssi 4813 . . . . . . . . . . . . 13 (𝑏𝑋 → {𝑏} ⊆ 𝑋)
122, 4igenidl 38050 . . . . . . . . . . . . 13 ((𝑅 ∈ RingOps ∧ {𝑏} ⊆ 𝑋) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
131, 11, 12syl2an 596 . . . . . . . . . . . 12 ((𝑅 ∈ CRingOps ∧ 𝑏𝑋) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
1413adantrl 716 . . . . . . . . . . 11 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
15 raleq 3321 . . . . . . . . . . . . 13 (𝑟 = (𝑅 IdlGen {𝑎}) → (∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃))
16 sseq1 4021 . . . . . . . . . . . . . 14 (𝑟 = (𝑅 IdlGen {𝑎}) → (𝑟𝑃 ↔ (𝑅 IdlGen {𝑎}) ⊆ 𝑃))
1716orbi1d 916 . . . . . . . . . . . . 13 (𝑟 = (𝑅 IdlGen {𝑎}) → ((𝑟𝑃𝑠𝑃) ↔ ((𝑅 IdlGen {𝑎}) ⊆ 𝑃𝑠𝑃)))
1815, 17imbi12d 344 . . . . . . . . . . . 12 (𝑟 = (𝑅 IdlGen {𝑎}) → ((∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) ↔ (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃𝑠𝑃))))
19 raleq 3321 . . . . . . . . . . . . . 14 (𝑠 = (𝑅 IdlGen {𝑏}) → (∀𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
2019ralbidv 3176 . . . . . . . . . . . . 13 (𝑠 = (𝑅 IdlGen {𝑏}) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
21 sseq1 4021 . . . . . . . . . . . . . 14 (𝑠 = (𝑅 IdlGen {𝑏}) → (𝑠𝑃 ↔ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))
2221orbi2d 915 . . . . . . . . . . . . 13 (𝑠 = (𝑅 IdlGen {𝑏}) → (((𝑅 IdlGen {𝑎}) ⊆ 𝑃𝑠𝑃) ↔ ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃)))
2320, 22imbi12d 344 . . . . . . . . . . . 12 (𝑠 = (𝑅 IdlGen {𝑏}) → ((∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃𝑠𝑃)) ↔ (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
2418, 23rspc2v 3633 . . . . . . . . . . 11 (((𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅) ∧ (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
2510, 14, 24syl2anc 584 . . . . . . . . . 10 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
2625adantlr 715 . . . . . . . . 9 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
272, 3, 4prnc 38054 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ CRingOps ∧ 𝑎𝑋) → (𝑅 IdlGen {𝑎}) = {𝑥𝑋 ∣ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)})
28 df-rab 3434 . . . . . . . . . . . . . . . . . . 19 {𝑥𝑋 ∣ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)} = {𝑥 ∣ (𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎))}
2927, 28eqtrdi 2791 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ CRingOps ∧ 𝑎𝑋) → (𝑅 IdlGen {𝑎}) = {𝑥 ∣ (𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎))})
3029eqabrd 2882 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ CRingOps ∧ 𝑎𝑋) → (𝑥 ∈ (𝑅 IdlGen {𝑎}) ↔ (𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎))))
3130adantrr 717 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → (𝑥 ∈ (𝑅 IdlGen {𝑎}) ↔ (𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎))))
322, 3, 4prnc 38054 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ CRingOps ∧ 𝑏𝑋) → (𝑅 IdlGen {𝑏}) = {𝑦𝑋 ∣ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏)})
33 df-rab 3434 . . . . . . . . . . . . . . . . . . 19 {𝑦𝑋 ∣ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏)} = {𝑦 ∣ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))}
3432, 33eqtrdi 2791 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ CRingOps ∧ 𝑏𝑋) → (𝑅 IdlGen {𝑏}) = {𝑦 ∣ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))})
3534eqabrd 2882 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ CRingOps ∧ 𝑏𝑋) → (𝑦 ∈ (𝑅 IdlGen {𝑏}) ↔ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))))
3635adantrl 716 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → (𝑦 ∈ (𝑅 IdlGen {𝑏}) ↔ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))))
3731, 36anbi12d 632 . . . . . . . . . . . . . . 15 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) ↔ ((𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏)))))
3837adantlr 715 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) ↔ ((𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏)))))
3938adantr 480 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) ↔ ((𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏)))))
40 reeanv 3227 . . . . . . . . . . . . . . . 16 (∃𝑟𝑋𝑠𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) ↔ (∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏)))
4140anbi2i 623 . . . . . . . . . . . . . . 15 (((𝑥𝑋𝑦𝑋) ∧ ∃𝑟𝑋𝑠𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥𝑋𝑦𝑋) ∧ (∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))))
42 an4 656 . . . . . . . . . . . . . . 15 (((𝑥𝑋𝑦𝑋) ∧ (∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))))
4341, 42bitri 275 . . . . . . . . . . . . . 14 (((𝑥𝑋𝑦𝑋) ∧ ∃𝑟𝑋𝑠𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))))
442, 3, 4crngm4 37990 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ CRingOps ∧ (𝑟𝑋𝑠𝑋) ∧ (𝑎𝑋𝑏𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
45443com23 1125 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
46453expa 1117 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
4746adantllr 719 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
4847adantlr 715 . . . . . . . . . . . . . . . . . 18 (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
492, 3, 4rngocl 37888 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 ∈ RingOps ∧ 𝑟𝑋𝑠𝑋) → (𝑟𝐻𝑠) ∈ 𝑋)
501, 49syl3an1 1162 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ CRingOps ∧ 𝑟𝑋𝑠𝑋) → (𝑟𝐻𝑠) ∈ 𝑋)
51503expb 1119 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ CRingOps ∧ (𝑟𝑋𝑠𝑋)) → (𝑟𝐻𝑠) ∈ 𝑋)
5251adantlr 715 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑟𝑋𝑠𝑋)) → (𝑟𝐻𝑠) ∈ 𝑋)
5352adantlr 715 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝑋𝑠𝑋)) → (𝑟𝐻𝑠) ∈ 𝑋)
542, 3, 4idllmulcl 38007 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 ∈ RingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ ((𝑎𝐻𝑏) ∈ 𝑃 ∧ (𝑟𝐻𝑠) ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
551, 54sylanl1 680 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ ((𝑎𝐻𝑏) ∈ 𝑃 ∧ (𝑟𝐻𝑠) ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
5655anassrs 467 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝐻𝑠) ∈ 𝑋) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
5753, 56syldan 591 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
5857adantllr 719 . . . . . . . . . . . . . . . . . 18 (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
5948, 58eqeltrrd 2840 . . . . . . . . . . . . . . . . 17 (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)) ∈ 𝑃)
60 oveq12 7440 . . . . . . . . . . . . . . . . . 18 ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → (𝑥𝐻𝑦) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
6160eleq1d 2824 . . . . . . . . . . . . . . . . 17 ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → ((𝑥𝐻𝑦) ∈ 𝑃 ↔ ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)) ∈ 𝑃))
6259, 61syl5ibrcom 247 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → (𝑥𝐻𝑦) ∈ 𝑃))
6362rexlimdvva 3211 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → (∃𝑟𝑋𝑠𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → (𝑥𝐻𝑦) ∈ 𝑃))
6463adantld 490 . . . . . . . . . . . . . 14 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → (((𝑥𝑋𝑦𝑋) ∧ ∃𝑟𝑋𝑠𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏))) → (𝑥𝐻𝑦) ∈ 𝑃))
6543, 64biimtrrid 243 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → (((𝑥𝑋 ∧ ∃𝑟𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦𝑋 ∧ ∃𝑠𝑋 𝑦 = (𝑠𝐻𝑏))) → (𝑥𝐻𝑦) ∈ 𝑃))
6639, 65sylbid 240 . . . . . . . . . . . 12 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) → (𝑥𝐻𝑦) ∈ 𝑃))
6766ralrimivv 3198 . . . . . . . . . . 11 ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃)
6867ex 412 . . . . . . . . . 10 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) → ((𝑎𝐻𝑏) ∈ 𝑃 → ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
692, 4igenss 38049 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ RingOps ∧ {𝑎} ⊆ 𝑋) → {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
701, 7, 69syl2an 596 . . . . . . . . . . . . . . 15 ((𝑅 ∈ CRingOps ∧ 𝑎𝑋) → {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
71 vex 3482 . . . . . . . . . . . . . . . 16 𝑎 ∈ V
7271snss 4790 . . . . . . . . . . . . . . 15 (𝑎 ∈ (𝑅 IdlGen {𝑎}) ↔ {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
7370, 72sylibr 234 . . . . . . . . . . . . . 14 ((𝑅 ∈ CRingOps ∧ 𝑎𝑋) → 𝑎 ∈ (𝑅 IdlGen {𝑎}))
7473adantrr 717 . . . . . . . . . . . . 13 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → 𝑎 ∈ (𝑅 IdlGen {𝑎}))
75 ssel 3989 . . . . . . . . . . . . 13 ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 → (𝑎 ∈ (𝑅 IdlGen {𝑎}) → 𝑎𝑃))
7674, 75syl5com 31 . . . . . . . . . . . 12 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃𝑎𝑃))
772, 4igenss 38049 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ RingOps ∧ {𝑏} ⊆ 𝑋) → {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
781, 11, 77syl2an 596 . . . . . . . . . . . . . . 15 ((𝑅 ∈ CRingOps ∧ 𝑏𝑋) → {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
79 vex 3482 . . . . . . . . . . . . . . . 16 𝑏 ∈ V
8079snss 4790 . . . . . . . . . . . . . . 15 (𝑏 ∈ (𝑅 IdlGen {𝑏}) ↔ {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
8178, 80sylibr 234 . . . . . . . . . . . . . 14 ((𝑅 ∈ CRingOps ∧ 𝑏𝑋) → 𝑏 ∈ (𝑅 IdlGen {𝑏}))
8281adantrl 716 . . . . . . . . . . . . 13 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → 𝑏 ∈ (𝑅 IdlGen {𝑏}))
83 ssel 3989 . . . . . . . . . . . . 13 ((𝑅 IdlGen {𝑏}) ⊆ 𝑃 → (𝑏 ∈ (𝑅 IdlGen {𝑏}) → 𝑏𝑃))
8482, 83syl5com 31 . . . . . . . . . . . 12 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → ((𝑅 IdlGen {𝑏}) ⊆ 𝑃𝑏𝑃))
8576, 84orim12d 966 . . . . . . . . . . 11 ((𝑅 ∈ CRingOps ∧ (𝑎𝑋𝑏𝑋)) → (((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃) → (𝑎𝑃𝑏𝑃)))
8685adantlr 715 . . . . . . . . . 10 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) → (((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃) → (𝑎𝑃𝑏𝑃)))
8768, 86imim12d 81 . . . . . . . . 9 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) → ((∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃)) → ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
8826, 87syld 47 . . . . . . . 8 (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝑋𝑏𝑋)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) → ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
8988ralrimdvva 3209 . . . . . . 7 ((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) → ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
9089ex 412 . . . . . 6 (𝑅 ∈ CRingOps → (𝑃 ∈ (Idl‘𝑅) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) → ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))))
9190adantrd 491 . . . . 5 (𝑅 ∈ CRingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)) → ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))))
9291imdistand 570 . . . 4 (𝑅 ∈ CRingOps → (((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))) → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))))
93 df-3an 1088 . . . 4 ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))) ↔ ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))))
94 df-3an 1088 . . . 4 ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) ↔ ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
9592, 93, 943imtr4g 296 . . 3 (𝑅 ∈ CRingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥𝑟𝑦𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))) → (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))))
966, 95sylbid 240 . 2 (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) → (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))))
972, 3, 4ispridl2 38025 . . . 4 ((𝑅 ∈ RingOps ∧ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))) → 𝑃 ∈ (PrIdl‘𝑅))
9897ex 412 . . 3 (𝑅 ∈ RingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → 𝑃 ∈ (PrIdl‘𝑅)))
991, 98syl 17 . 2 (𝑅 ∈ CRingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → 𝑃 ∈ (PrIdl‘𝑅)))
10096, 99impbid 212 1 (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 847  w3a 1086   = wceq 1537  wcel 2106  {cab 2712  wne 2938  wral 3059  wrex 3068  {crab 3433  wss 3963  {csn 4631  ran crn 5690  cfv 6563  (class class class)co 7431  1st c1st 8011  2nd c2nd 8012  RingOpscrngo 37881  CRingOpsccring 37980  Idlcidl 37994  PrIdlcpridl 37995   IdlGen cigen 38046
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014  df-grpo 30522  df-gid 30523  df-ginv 30524  df-ablo 30574  df-ass 37830  df-exid 37832  df-mgmOLD 37836  df-sgrOLD 37848  df-mndo 37854  df-rngo 37882  df-com2 37977  df-crngo 37981  df-idl 37997  df-pridl 37998  df-igen 38047
This theorem is referenced by:  pridlc  38058  isdmn3  38061
  Copyright terms: Public domain W3C validator