pridlc3

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

	Ref	Expression
Hypotheses	ispridlc.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
	ispridlc.2	⊢ 𝐻 = ( 2^nd ‘ 𝑅 )
	ispridlc.3	⊢ 𝑋 = ran 𝐺
Assertion	pridlc3	⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ ( 𝑋 ∖ 𝑃 ) ) ) → ( 𝐴 𝐻 𝐵 ) ∈ ( 𝑋 ∖ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		ispridlc.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
2		ispridlc.2	⊢ 𝐻 = ( 2^nd ‘ 𝑅 )
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 ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ ( 𝑋 ∖ 𝑃 ) ) ) → ( 𝐴 𝐻 𝐵 ) ∈ ( 𝑋 ∖ 𝑃 ) )

Metamath Proof Explorer

Theorem pridlc3

Proof