maxidlnr

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

	Ref	Expression
Hypotheses	maxidlnr.1	$⊢ G = 1^{st} (R)$
	maxidlnr.2	$⊢ X = ran G$
Assertion	maxidlnr	$⊢ (R \in RingOps \land M \in MaxIdl (R)) \to M \neq X$

Step	Hyp	Ref	Expression
1		maxidlnr.1	$⊢ G = 1^{st} (R)$
2		maxidlnr.2	$⊢ X = ran G$
3	1 2	ismaxidl	$⊢ R \in RingOps \to (M \in MaxIdl (R) \leftrightarrow (M \in Idl (R) \land M \neq X \land \forall j \in Idl (R) (M \subseteq j \to (j = M \lor j = X))))$
4	3	biimpa	$⊢ (R \in RingOps \land M \in MaxIdl (R)) \to (M \in Idl (R) \land M \neq X \land \forall j \in Idl (R) (M \subseteq j \to (j = M \lor j = X)))$
5	4	simp2d	$⊢ (R \in RingOps \land M \in MaxIdl (R)) \to M \neq X$

Metamath Proof Explorer