Metamath Proof Explorer


Theorem maxidlidl

Description: A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011)

Ref Expression
Assertion maxidlidl R RingOps M MaxIdl R M Idl R

Proof

Step Hyp Ref Expression
1 eqid 1 st R = 1 st R
2 eqid ran 1 st R = ran 1 st R
3 1 2 ismaxidl R RingOps M MaxIdl R M Idl R M ran 1 st R j Idl R M j j = M j = ran 1 st R
4 3anass M Idl R M ran 1 st R j Idl R M j j = M j = ran 1 st R M Idl R M ran 1 st R j Idl R M j j = M j = ran 1 st R
5 3 4 bitrdi R RingOps M MaxIdl R M Idl R M ran 1 st R j Idl R M j j = M j = ran 1 st R
6 5 simprbda R RingOps M MaxIdl R M Idl R