Metamath Proof Explorer

Theorem ispridl

Description: The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010)

		Ref	Expression
	Hypotheses	pridlval.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
		pridlval.2	⊢ 𝐻 = ( 2^nd ‘ 𝑅 )
		pridlval.3	⊢ 𝑋 = ran 𝐺
	Assertion	ispridl	⊢ ( 𝑅 ∈ RingOps → ( 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ↔ ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pridlval.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
2		pridlval.2	⊢ 𝐻 = ( 2^nd ‘ 𝑅 )
3		pridlval.3	⊢ 𝑋 = ran 𝐺
4	1 2 3	pridlval	⊢ ( 𝑅 ∈ RingOps → ( PrIdl ‘ 𝑅 ) = { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝑋 ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) } )
5	4	eleq2d	⊢ ( 𝑅 ∈ RingOps → ( 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ↔ 𝑃 ∈ { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝑋 ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) } ) )
6		neeq1	⊢ ( 𝑖 = 𝑃 → ( 𝑖 ≠ 𝑋 ↔ 𝑃 ≠ 𝑋 ) )
7		eleq2	⊢ ( 𝑖 = 𝑃 → ( ( 𝑥 𝐻 𝑦 ) ∈ 𝑖 ↔ ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ) )
8	7	2ralbidv	⊢ ( 𝑖 = 𝑃 → ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑖 ↔ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ) )
9		sseq2	⊢ ( 𝑖 = 𝑃 → ( 𝑎 ⊆ 𝑖 ↔ 𝑎 ⊆ 𝑃 ) )
10		sseq2	⊢ ( 𝑖 = 𝑃 → ( 𝑏 ⊆ 𝑖 ↔ 𝑏 ⊆ 𝑃 ) )
11	9 10	orbi12d	⊢ ( 𝑖 = 𝑃 → ( ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ↔ ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) )
12	8 11	imbi12d	⊢ ( 𝑖 = 𝑃 → ( ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ↔ ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) )
13	12	2ralbidv	⊢ ( 𝑖 = 𝑃 → ( ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ↔ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) )
14	6 13	anbi12d	⊢ ( 𝑖 = 𝑃 → ( ( 𝑖 ≠ 𝑋 ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) ↔ ( 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ) )
15	14	elrab	⊢ ( 𝑃 ∈ { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝑋 ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) } ↔ ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ ( 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ) )
16		3anass	⊢ ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ↔ ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ ( 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ) )
17	15 16	bitr4i	⊢ ( 𝑃 ∈ { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝑋 ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) } ↔ ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) )
18	5 17	bitrdi	⊢ ( 𝑅 ∈ RingOps → ( 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ↔ ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ) )