Metamath Proof Explorer


Theorem ismxidl

Description: The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011) (Revised by Thierry Arnoux, 19-Jan-2024)

Ref Expression
Hypothesis mxidlval.1 𝐵 = ( Base ‘ 𝑅 )
Assertion ismxidl ( 𝑅 ∈ Ring → ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀𝑗 → ( 𝑗 = 𝑀𝑗 = 𝐵 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mxidlval.1 𝐵 = ( Base ‘ 𝑅 )
2 1 mxidlval ( 𝑅 ∈ Ring → ( MaxIdeal ‘ 𝑅 ) = { 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑖𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑖𝑗 → ( 𝑗 = 𝑖𝑗 = 𝐵 ) ) ) } )
3 2 eleq2d ( 𝑅 ∈ Ring → ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ 𝑀 ∈ { 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑖𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑖𝑗 → ( 𝑗 = 𝑖𝑗 = 𝐵 ) ) ) } ) )
4 neeq1 ( 𝑖 = 𝑀 → ( 𝑖𝐵𝑀𝐵 ) )
5 sseq1 ( 𝑖 = 𝑀 → ( 𝑖𝑗𝑀𝑗 ) )
6 eqeq2 ( 𝑖 = 𝑀 → ( 𝑗 = 𝑖𝑗 = 𝑀 ) )
7 6 orbi1d ( 𝑖 = 𝑀 → ( ( 𝑗 = 𝑖𝑗 = 𝐵 ) ↔ ( 𝑗 = 𝑀𝑗 = 𝐵 ) ) )
8 5 7 imbi12d ( 𝑖 = 𝑀 → ( ( 𝑖𝑗 → ( 𝑗 = 𝑖𝑗 = 𝐵 ) ) ↔ ( 𝑀𝑗 → ( 𝑗 = 𝑀𝑗 = 𝐵 ) ) ) )
9 8 ralbidv ( 𝑖 = 𝑀 → ( ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑖𝑗 → ( 𝑗 = 𝑖𝑗 = 𝐵 ) ) ↔ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀𝑗 → ( 𝑗 = 𝑀𝑗 = 𝐵 ) ) ) )
10 4 9 anbi12d ( 𝑖 = 𝑀 → ( ( 𝑖𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑖𝑗 → ( 𝑗 = 𝑖𝑗 = 𝐵 ) ) ) ↔ ( 𝑀𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀𝑗 → ( 𝑗 = 𝑀𝑗 = 𝐵 ) ) ) ) )
11 10 elrab ( 𝑀 ∈ { 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑖𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑖𝑗 → ( 𝑗 = 𝑖𝑗 = 𝐵 ) ) ) } ↔ ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑀𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀𝑗 → ( 𝑗 = 𝑀𝑗 = 𝐵 ) ) ) ) )
12 3anass ( ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀𝑗 → ( 𝑗 = 𝑀𝑗 = 𝐵 ) ) ) ↔ ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑀𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀𝑗 → ( 𝑗 = 𝑀𝑗 = 𝐵 ) ) ) ) )
13 11 12 bitr4i ( 𝑀 ∈ { 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑖𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑖𝑗 → ( 𝑗 = 𝑖𝑗 = 𝐵 ) ) ) } ↔ ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀𝑗 → ( 𝑗 = 𝑀𝑗 = 𝐵 ) ) ) )
14 3 13 bitrdi ( 𝑅 ∈ Ring → ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀𝑗 → ( 𝑗 = 𝑀𝑗 = 𝐵 ) ) ) ) )