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

Metamath Proof Explorer

Theorem mxidlval

Description: The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011) (Revised by Thierry Arnoux, 19-Jan-2024)

Ref Expression
Hypothesis mxidlval.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion mxidlval ( 𝑅 ∈ Ring → ( MaxIdeal ‘ 𝑅 ) = { 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝐵 ) ) ) } )

Proof

Step Hyp Ref Expression
1 mxidlval.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 fveq2 ⊢ ( 𝑟 = 𝑅 → ( LIdeal ‘ 𝑟 ) = ( LIdeal ‘ 𝑅 ) )
3 fveq2 ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
4 3 1 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = 𝐵 )
5 4 neeq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑖 ≠ ( Base ‘ 𝑟 ) ↔ 𝑖 ≠ 𝐵 ) )
6 4 eqeq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑗 = ( Base ‘ 𝑟 ) ↔ 𝑗 = 𝐵 ) )
7 6 orbi2d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑗 = 𝑖 ∨ 𝑗 = ( Base ‘ 𝑟 ) ) ↔ ( 𝑗 = 𝑖 ∨ 𝑗 = 𝐵 ) ) )
8 7 imbi2d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ( Base ‘ 𝑟 ) ) ) ↔ ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝐵 ) ) ) )
9 2 8 raleqbidv ⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑗 ∈ ( LIdeal ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ( Base ‘ 𝑟 ) ) ) ↔ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝐵 ) ) ) )
10 5 9 anbi12d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑖 ≠ ( Base ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ( Base ‘ 𝑟 ) ) ) ) ↔ ( 𝑖 ≠ 𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝐵 ) ) ) ) )
11 2 10 rabeqbidv ⊢ ( 𝑟 = 𝑅 → { 𝑖 ∈ ( LIdeal ‘ 𝑟 ) ∣ ( 𝑖 ≠ ( Base ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ( Base ‘ 𝑟 ) ) ) ) } = { 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝐵 ) ) ) } )
12 df-mxidl ⊢ MaxIdeal = ( 𝑟 ∈ Ring ↦ { 𝑖 ∈ ( LIdeal ‘ 𝑟 ) ∣ ( 𝑖 ≠ ( Base ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ( Base ‘ 𝑟 ) ) ) ) } )
13 fvex ⊢ ( LIdeal ‘ 𝑅 ) ∈ V
14 13 rabex ⊢ { 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝐵 ) ) ) } ∈ V
15 11 12 14 fvmpt ⊢ ( 𝑅 ∈ Ring → ( MaxIdeal ‘ 𝑅 ) = { 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝐵 ) ) ) } )