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 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
ispridlc.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
ispridlc.3 ⊢ 𝑋 = ran 𝐺
Assertion pridlc3 ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ ( 𝑋 ∖ 𝑃 ) ) ) → ( 𝐴 𝐻 𝐵 ) ∈ ( 𝑋 ∖ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 ispridlc.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 ispridlc.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 ispridlc.3 ⊢ 𝑋 = ran 𝐺
4 crngorngo ⊢ ( 𝑅 ∈ CRingOps → 𝑅 ∈ RingOps )
5 eldifi ⊢ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) → 𝐴 ∈ 𝑋 )
6 eldifi ⊢ ( 𝐵 ∈ ( 𝑋 ∖ 𝑃 ) → 𝐵 ∈ 𝑋 )
7 5 6 anim12i ⊢ ( ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ ( 𝑋 ∖ 𝑃 ) ) → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) )
8 1 2 3 rngocl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐻 𝐵 ) ∈ 𝑋 )
9 8 3expb ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐻 𝐵 ) ∈ 𝑋 )
10 4 7 9 syl2an ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ ( 𝑋 ∖ 𝑃 ) ) ) → ( 𝐴 𝐻 𝐵 ) ∈ 𝑋 )
11 10 adantlr ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ ( 𝑋 ∖ 𝑃 ) ) ) → ( 𝐴 𝐻 𝐵 ) ∈ 𝑋 )
12 eldifn ⊢ ( 𝐵 ∈ ( 𝑋 ∖ 𝑃 ) → ¬ 𝐵 ∈ 𝑃 )
13 12 ad2antll ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ ( 𝑋 ∖ 𝑃 ) ) ) → ¬ 𝐵 ∈ 𝑃 )
14 1 2 3 pridlc2 ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 ) ) → 𝐵 ∈ 𝑃 )
15 14 3exp2 ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) → ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) → ( 𝐵 ∈ 𝑋 → ( ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 → 𝐵 ∈ 𝑃 ) ) ) )
16 15 imp32 ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 → 𝐵 ∈ 𝑃 ) )
17 16 con3d ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ 𝑋 ) ) → ( ¬ 𝐵 ∈ 𝑃 → ¬ ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 ) )
18 6 17 sylanr2 ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ ( 𝑋 ∖ 𝑃 ) ) ) → ( ¬ 𝐵 ∈ 𝑃 → ¬ ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 ) )
19 13 18 mpd ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ ( 𝑋 ∖ 𝑃 ) ) ) → ¬ ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 )
20 11 19 eldifd ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ ( 𝑋 ∖ 𝑃 ) ) ) → ( 𝐴 𝐻 𝐵 ) ∈ ( 𝑋 ∖ 𝑃 ) )