Theorem pridlc2

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	pridlc2	⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 ) ) → 𝐵 ∈ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		ispridlc.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
2		ispridlc.2	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3		ispridlc.3	⊢ 𝑋 = ran 𝐺
4		eldifn	⊢ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) → ¬ 𝐴 ∈ 𝑃 )
5	4	3ad2ant1	⊢ ( ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 ) → ¬ 𝐴 ∈ 𝑃 )
6	5	adantl	⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 ) ) → ¬ 𝐴 ∈ 𝑃 )
7		eldifi	⊢ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) → 𝐴 ∈ 𝑋 )
8	1 2 3	pridlc	⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 ) ) → ( 𝐴 ∈ 𝑃 ∨ 𝐵 ∈ 𝑃 ) )
9	8	ord	⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 ) ) → ( ¬ 𝐴 ∈ 𝑃 → 𝐵 ∈ 𝑃 ) )
10	7 9	syl3anr1	⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 ) ) → ( ¬ 𝐴 ∈ 𝑃 → 𝐵 ∈ 𝑃 ) )
11	6 10	mpd	⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 ) ) → 𝐵 ∈ 𝑃 )