Metamath Proof Explorer

Theorem pridlc

Description: Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011)

Ref Expression
Hypotheses ispridlc.1 ⊢G=1st⁡R
ispridlc.2 ⊢H=2nd⁡R
ispridlc.3 ⊢X=ran⁡G
Assertion pridlc ⊢R∈CRingOps∧P∈PrIdl⁡R∧A∈X∧B∈X∧AHB∈P→A∈P∨B∈P

Proof

Step Hyp Ref Expression
1 ispridlc.1 ⊢G=1st⁡R
2 ispridlc.2 ⊢H=2nd⁡R
3 ispridlc.3 ⊢X=ran⁡G
4 1 2 3 ispridlc ⊢R∈CRingOps→P∈PrIdl⁡R↔P∈Idl⁡R∧P≠X∧∀a∈X∀b∈XaHb∈P→a∈P∨b∈P
5 4 biimpa ⊢R∈CRingOps∧P∈PrIdl⁡R→P∈Idl⁡R∧P≠X∧∀a∈X∀b∈XaHb∈P→a∈P∨b∈P
6 5 simp3d ⊢R∈CRingOps∧P∈PrIdl⁡R→∀a∈X∀b∈XaHb∈P→a∈P∨b∈P
7 oveq1 ⊢a=A→aHb=AHb
8 7 eleq1d ⊢a=A→aHb∈P↔AHb∈P
9 eleq1 ⊢a=A→a∈P↔A∈P
10 9 orbi1d ⊢a=A→a∈P∨b∈P↔A∈P∨b∈P
11 8 10 imbi12d ⊢a=A→aHb∈P→a∈P∨b∈P↔AHb∈P→A∈P∨b∈P
12 oveq2 ⊢b=B→AHb=AHB
13 12 eleq1d ⊢b=B→AHb∈P↔AHB∈P
14 eleq1 ⊢b=B→b∈P↔B∈P
15 14 orbi2d ⊢b=B→A∈P∨b∈P↔A∈P∨B∈P
16 13 15 imbi12d ⊢b=B→AHb∈P→A∈P∨b∈P↔AHB∈P→A∈P∨B∈P
17 11 16 rspc2v ⊢A∈X∧B∈X→∀a∈X∀b∈XaHb∈P→a∈P∨b∈P→AHB∈P→A∈P∨B∈P
18 17 com12 ⊢∀a∈X∀b∈XaHb∈P→a∈P∨b∈P→A∈X∧B∈X→AHB∈P→A∈P∨B∈P
19 18 expd ⊢∀a∈X∀b∈XaHb∈P→a∈P∨b∈P→A∈X→B∈X→AHB∈P→A∈P∨B∈P
20 19 3imp2 ⊢∀a∈X∀b∈XaHb∈P→a∈P∨b∈P∧A∈X∧B∈X∧AHB∈P→A∈P∨B∈P
21 6 20 sylan ⊢R∈CRingOps∧P∈PrIdl⁡R∧A∈X∧B∈X∧AHB∈P→A∈P∨B∈P