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 ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ) ) ) )