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 = 1 st ⁡ R
ispridlc.2 ⊢ H = 2 nd ⁡ R
ispridlc.3 ⊢ X = ran ⁡ G
Assertion pridlc3 ⊢ R ∈ CRingOps ∧ P ∈ PrIdl ⁡ R ∧ A ∈ X ∖ P ∧ B ∈ X ∖ P → A H B ∈ X ∖ P

Proof

Step Hyp Ref Expression
1 ispridlc.1 ⊢ G = 1 st ⁡ R
2 ispridlc.2 ⊢ H = 2 nd ⁡ 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 → A H B ∈ X
9 8 3expb ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X → A H B ∈ X
10 4 7 9 syl2an ⊢ R ∈ CRingOps ∧ A ∈ X ∖ P ∧ B ∈ X ∖ P → A H B ∈ X
11 10 adantlr ⊢ R ∈ CRingOps ∧ P ∈ PrIdl ⁡ R ∧ A ∈ X ∖ P ∧ B ∈ X ∖ P → A H B ∈ 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 ∧ A H B ∈ P → B ∈ P
15 14 3exp2 ⊢ R ∈ CRingOps ∧ P ∈ PrIdl ⁡ R → A ∈ X ∖ P → B ∈ X → A H B ∈ P → B ∈ P
16 15 imp32 ⊢ R ∈ CRingOps ∧ P ∈ PrIdl ⁡ R ∧ A ∈ X ∖ P ∧ B ∈ X → A H B ∈ P → B ∈ P
17 16 con3d ⊢ R ∈ CRingOps ∧ P ∈ PrIdl ⁡ R ∧ A ∈ X ∖ P ∧ B ∈ X → ¬ B ∈ P → ¬ A H B ∈ P
18 6 17 sylanr2 ⊢ R ∈ CRingOps ∧ P ∈ PrIdl ⁡ R ∧ A ∈ X ∖ P ∧ B ∈ X ∖ P → ¬ B ∈ P → ¬ A H B ∈ P
19 13 18 mpd ⊢ R ∈ CRingOps ∧ P ∈ PrIdl ⁡ R ∧ A ∈ X ∖ P ∧ B ∈ X ∖ P → ¬ A H B ∈ P
20 11 19 eldifd ⊢ R ∈ CRingOps ∧ P ∈ PrIdl ⁡ R ∧ A ∈ X ∖ P ∧ B ∈ X ∖ P → A H B ∈ X ∖ P