Metamath Proof Explorer


Theorem maxidln1

Description: One is not contained in any maximal ideal. (Contributed by Jeff Madsen, 17-Jun-2011)

Ref Expression
Hypotheses maxidln1.1 H = 2 nd R
maxidln1.2 U = GId H
Assertion maxidln1 R RingOps M MaxIdl R ¬ U M

Proof

Step Hyp Ref Expression
1 maxidln1.1 H = 2 nd R
2 maxidln1.2 U = GId H
3 eqid 1 st R = 1 st R
4 eqid ran 1 st R = ran 1 st R
5 3 4 maxidlnr R RingOps M MaxIdl R M ran 1 st R
6 maxidlidl R RingOps M MaxIdl R M Idl R
7 3 1 4 2 1idl R RingOps M Idl R U M M = ran 1 st R
8 7 necon3bbid R RingOps M Idl R ¬ U M M ran 1 st R
9 6 8 syldan R RingOps M MaxIdl R ¬ U M M ran 1 st R
10 5 9 mpbird R RingOps M MaxIdl R ¬ U M