Theorem maxidlmax

Description: A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011)

	Ref	Expression
Hypotheses	maxidlnr.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
	maxidlnr.2	⊢ 𝑋 = ran 𝐺
Assertion	maxidlmax	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑀 ⊆ 𝐼 ) ) → ( 𝐼 = 𝑀 ∨ 𝐼 = 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		maxidlnr.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
2		maxidlnr.2	⊢ 𝑋 = ran 𝐺
3	1 2	ismaxidl	⊢ ( 𝑅 ∈ RingOps → ( 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ↔ ( 𝑀 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑀 ≠ 𝑋 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ) ) ) )
4	3	biimpa	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) → ( 𝑀 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑀 ≠ 𝑋 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ) ) )
5	4	simp3d	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) → ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ) )
6		sseq2	⊢ ( 𝑗 = 𝐼 → ( 𝑀 ⊆ 𝑗 ↔ 𝑀 ⊆ 𝐼 ) )
7		eqeq1	⊢ ( 𝑗 = 𝐼 → ( 𝑗 = 𝑀 ↔ 𝐼 = 𝑀 ) )
8		eqeq1	⊢ ( 𝑗 = 𝐼 → ( 𝑗 = 𝑋 ↔ 𝐼 = 𝑋 ) )
9	7 8	orbi12d	⊢ ( 𝑗 = 𝐼 → ( ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ↔ ( 𝐼 = 𝑀 ∨ 𝐼 = 𝑋 ) ) )
10	6 9	imbi12d	⊢ ( 𝑗 = 𝐼 → ( ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ) ↔ ( 𝑀 ⊆ 𝐼 → ( 𝐼 = 𝑀 ∨ 𝐼 = 𝑋 ) ) ) )
11	10	rspcva	⊢ ( ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ) ) → ( 𝑀 ⊆ 𝐼 → ( 𝐼 = 𝑀 ∨ 𝐼 = 𝑋 ) ) )
12	5 11	sylan2	⊢ ( ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) ) → ( 𝑀 ⊆ 𝐼 → ( 𝐼 = 𝑀 ∨ 𝐼 = 𝑋 ) ) )
13	12	ancoms	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝑀 ⊆ 𝐼 → ( 𝐼 = 𝑀 ∨ 𝐼 = 𝑋 ) ) )
14	13	impr	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑀 ⊆ 𝐼 ) ) → ( 𝐼 = 𝑀 ∨ 𝐼 = 𝑋 ) )