Theorem pridlval

Description: The class of prime ideals of a ring R . (Contributed by Jeff Madsen, 10-Jun-2010)

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

Proof

Step	Hyp	Ref	Expression
1		pridlval.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
2		pridlval.2	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3		pridlval.3	⊢ 𝑋 = ran 𝐺
4		fveq2	⊢ ( 𝑟 = 𝑅 → ( Idl ‘ 𝑟 ) = ( Idl ‘ 𝑅 ) )
5		fveq2	⊢ ( 𝑟 = 𝑅 → ( 1st ‘ 𝑟 ) = ( 1st ‘ 𝑅 ) )
6	5 1	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( 1st ‘ 𝑟 ) = 𝐺 )
7	6	rneqd	⊢ ( 𝑟 = 𝑅 → ran ( 1st ‘ 𝑟 ) = ran 𝐺 )
8	7 3	eqtr4di	⊢ ( 𝑟 = 𝑅 → ran ( 1st ‘ 𝑟 ) = 𝑋 )
9	8	neeq2d	⊢ ( 𝑟 = 𝑅 → ( 𝑖 ≠ ran ( 1st ‘ 𝑟 ) ↔ 𝑖 ≠ 𝑋 ) )
10		fveq2	⊢ ( 𝑟 = 𝑅 → ( 2nd ‘ 𝑟 ) = ( 2nd ‘ 𝑅 ) )
11	10 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( 2nd ‘ 𝑟 ) = 𝐻 )
12	11	oveqd	⊢ ( 𝑟 = 𝑅 → ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
13	12	eleq1d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ↔ ( 𝑥 𝐻 𝑦 ) ∈ 𝑖 ) )
14	13	2ralbidv	⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ↔ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑖 ) )
15	14	imbi1d	⊢ ( 𝑟 = 𝑅 → ( ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ↔ ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) )
16	4 15	raleqbidv	⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑏 ∈ ( Idl ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ↔ ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) )
17	4 16	raleqbidv	⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑎 ∈ ( Idl ‘ 𝑟 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ↔ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) )
18	9 17	anbi12d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑖 ≠ ran ( 1st ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑟 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) ↔ ( 𝑖 ≠ 𝑋 ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) ) )
19	4 18	rabeqbidv	⊢ ( 𝑟 = 𝑅 → { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1st ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑟 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) } = { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝑋 ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) } )
20		df-pridl	⊢ PrIdl = ( 𝑟 ∈ RingOps ↦ { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1st ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑟 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) } )
21		fvex	⊢ ( Idl ‘ 𝑅 ) ∈ V
22	21	rabex	⊢ { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝑋 ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) } ∈ V
23	19 20 22	fvmpt	⊢ ( 𝑅 ∈ RingOps → ( PrIdl ‘ 𝑅 ) = { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝑋 ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) } )