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 \in RingOps \land M \in MaxIdl (R)) \to \neg U \in M$

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 \in RingOps \land M \in MaxIdl (R)) \to M \neq ran 1^{st} (R)$
6		maxidlidl	$⊢ (R \in RingOps \land M \in MaxIdl (R)) \to M \in Idl (R)$
7	3 1 4 2	1idl	$⊢ (R \in RingOps \land M \in Idl (R)) \to (U \in M \leftrightarrow M = ran 1^{st} (R))$
8	7	necon3bbid	$⊢ (R \in RingOps \land M \in Idl (R)) \to (\neg U \in M \leftrightarrow M \neq ran 1^{st} (R))$
9	6 8	syldan	$⊢ (R \in RingOps \land M \in MaxIdl (R)) \to (\neg U \in M \leftrightarrow M \neq ran 1^{st} (R))$
10	5 9	mpbird	$⊢ (R \in RingOps \land M \in MaxIdl (R)) \to \neg U \in M$

Metamath Proof Explorer