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

Metamath Proof Explorer

Theorem ismaxidl

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

Ref Expression
Hypotheses ismaxidl.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
ismaxidl.2 ⊢ 𝑋 = ran 𝐺
Assertion ismaxidl ( 𝑅 ∈ RingOps → ( 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ↔ ( 𝑀 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑀 ≠ 𝑋 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ismaxidl.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 ismaxidl.2 ⊢ 𝑋 = ran 𝐺
3 1 2 maxidlval ⊢ ( 𝑅 ∈ RingOps → ( MaxIdl ‘ 𝑅 ) = { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝑋 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝑋 ) ) ) } )
4 3 eleq2d ⊢ ( 𝑅 ∈ RingOps → ( 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ↔ 𝑀 ∈ { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝑋 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝑋 ) ) ) } ) )
5 neeq1 ⊢ ( 𝑖 = 𝑀 → ( 𝑖 ≠ 𝑋 ↔ 𝑀 ≠ 𝑋 ) )
6 sseq1 ⊢ ( 𝑖 = 𝑀 → ( 𝑖 ⊆ 𝑗 ↔ 𝑀 ⊆ 𝑗 ) )
7 eqeq2 ⊢ ( 𝑖 = 𝑀 → ( 𝑗 = 𝑖 ↔ 𝑗 = 𝑀 ) )
8 7 orbi1d ⊢ ( 𝑖 = 𝑀 → ( ( 𝑗 = 𝑖 ∨ 𝑗 = 𝑋 ) ↔ ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ) )
9 6 8 imbi12d ⊢ ( 𝑖 = 𝑀 → ( ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝑋 ) ) ↔ ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ) ) )
10 9 ralbidv ⊢ ( 𝑖 = 𝑀 → ( ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝑋 ) ) ↔ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ) ) )
11 5 10 anbi12d ⊢ ( 𝑖 = 𝑀 → ( ( 𝑖 ≠ 𝑋 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝑋 ) ) ) ↔ ( 𝑀 ≠ 𝑋 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ) ) ) )
12 11 elrab ⊢ ( 𝑀 ∈ { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝑋 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝑋 ) ) ) } ↔ ( 𝑀 ∈ ( Idl ‘ 𝑅 ) ∧ ( 𝑀 ≠ 𝑋 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ) ) ) )
13 3anass ⊢ ( ( 𝑀 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑀 ≠ 𝑋 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ) ) ↔ ( 𝑀 ∈ ( Idl ‘ 𝑅 ) ∧ ( 𝑀 ≠ 𝑋 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ) ) ) )
14 12 13 bitr4i ⊢ ( 𝑀 ∈ { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝑋 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝑋 ) ) ) } ↔ ( 𝑀 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑀 ≠ 𝑋 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ) ) )
15 4 14 bitrdi ⊢ ( 𝑅 ∈ RingOps → ( 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ↔ ( 𝑀 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑀 ≠ 𝑋 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ) ) ) )