This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) } )