Metamath Proof Explorer

Theorem maxidln0

Description: Obsolete theorem, use mxidlnzr instead. A ring with a maximal ideal is not the zero ring. (Contributed by Jeff Madsen, 17-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	maxidln0.1	$⊢ G = 1^{st} (R)$
		maxidln0.2	$⊢ H = 2^{nd} (R)$
		maxidln0.3	$⊢ Z = GId (G)$
		maxidln0.4	$⊢ U = GId (H)$
	Assertion	maxidln0	$⊢ (R \in RingOps \land M \in MaxIdl (R)) \to U \neq Z$

Proof

Step	Hyp	Ref	Expression
1		maxidln0.1	$⊢ G = 1^{st} (R)$
2		maxidln0.2	$⊢ H = 2^{nd} (R)$
3		maxidln0.3	$⊢ Z = GId (G)$
4		maxidln0.4	$⊢ U = GId (H)$
5		maxidlidl	$⊢ (R \in RingOps \land M \in MaxIdl (R)) \to M \in Idl (R)$
6	1 3	idl0cl	$⊢ (R \in RingOps \land M \in Idl (R)) \to Z \in M$
7	5 6	syldan	$⊢ (R \in RingOps \land M \in MaxIdl (R)) \to Z \in M$
8	2 4	maxidln1	$⊢ (R \in RingOps \land M \in MaxIdl (R)) \to \neg U \in M$
9		nelneq	$⊢ (Z \in M \land \neg U \in M) \to \neg Z = U$
10	7 8 9	syl2anc	$⊢ (R \in RingOps \land M \in MaxIdl (R)) \to \neg Z = U$
11	10	neqned	$⊢ (R \in RingOps \land M \in MaxIdl (R)) \to Z \neq U$
12	11	necomd	$⊢ (R \in RingOps \land M \in MaxIdl (R)) \to U \neq Z$