Metamath Proof Explorer

Theorem pridlc3

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 pridlc3 ⊢R∈CRingOps∧P∈PrIdl⁡R∧A∈X∖P∧B∈X∖P→AHB∈X∖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 crngorngo ⊢R∈CRingOps→R∈RingOps
5 eldifi ⊢A∈X∖P→A∈X
6 eldifi ⊢B∈X∖P→B∈X
7 5 6 anim12i ⊢A∈X∖P∧B∈X∖P→A∈X∧B∈X
8 1 2 3 rngocl ⊢R∈RingOps∧A∈X∧B∈X→AHB∈X
9 8 3expb ⊢R∈RingOps∧A∈X∧B∈X→AHB∈X
10 4 7 9 syl2an ⊢R∈CRingOps∧A∈X∖P∧B∈X∖P→AHB∈X
11 10 adantlr ⊢R∈CRingOps∧P∈PrIdl⁡R∧A∈X∖P∧B∈X∖P→AHB∈X
12 eldifn ⊢B∈X∖P→¬B∈P
13 12 ad2antll ⊢R∈CRingOps∧P∈PrIdl⁡R∧A∈X∖P∧B∈X∖P→¬B∈P
14 1 2 3 pridlc2 ⊢R∈CRingOps∧P∈PrIdl⁡R∧A∈X∖P∧B∈X∧AHB∈P→B∈P
15 14 3exp2 ⊢R∈CRingOps∧P∈PrIdl⁡R→A∈X∖P→B∈X→AHB∈P→B∈P
16 15 imp32 ⊢R∈CRingOps∧P∈PrIdl⁡R∧A∈X∖P∧B∈X→AHB∈P→B∈P
17 16 con3d ⊢R∈CRingOps∧P∈PrIdl⁡R∧A∈X∖P∧B∈X→¬B∈P→¬AHB∈P
18 6 17 sylanr2 ⊢R∈CRingOps∧P∈PrIdl⁡R∧A∈X∖P∧B∈X∖P→¬B∈P→¬AHB∈P
19 13 18 mpd ⊢R∈CRingOps∧P∈PrIdl⁡R∧A∈X∖P∧B∈X∖P→¬AHB∈P
20 11 19 eldifd ⊢R∈CRingOps∧P∈PrIdl⁡R∧A∈X∖P∧B∈X∖P→AHB∈X∖P