dflringlem

Description: Lemma for dflring3 . If a ring R has a single maximal ideal M , then any element X outside of M is a unit. (Contributed by Thierry Arnoux, 2-Jun-2026)

	Ref	Expression
Hypotheses	dflringlem.b	$⊢ B = {Base}_{R}$
	dflringlem.u	$⊢ U = Unit (R)$
	dflringlem.r	$⊢ φ \to R \in CRing$
	dflringlem.m	$⊢ φ \to M \in MaxIdeal (R)$
	dflringlem.1	$⊢ φ \to MaxIdeal (R) = \{M\}$
	dflringlem.x	$⊢ φ \to X \in (B ∖ M)$
Assertion	dflringlem	$⊢ φ \to X \in U$

Proof

Step	Hyp	Ref	Expression
1		dflringlem.b	$⊢ B = {Base}_{R}$
2		dflringlem.u	$⊢ U = Unit (R)$
3		dflringlem.r	$⊢ φ \to R \in CRing$
4		dflringlem.m	$⊢ φ \to M \in MaxIdeal (R)$
5		dflringlem.1	$⊢ φ \to MaxIdeal (R) = \{M\}$
6		dflringlem.x	$⊢ φ \to X \in (B ∖ M)$
7	4	adantr	$⊢ (φ \land \neg X \in U) \to M \in MaxIdeal (R)$
8	3	crngringd	$⊢ φ \to R \in Ring$
9	8	adantr	$⊢ (φ \land \neg X \in U) \to R \in Ring$
10	6	eldifad	$⊢ φ \to X \in B$
11	10	snssd	$⊢ φ \to \{X\} \subseteq B$
12		eqid	$⊢ RSpan (R) = RSpan (R)$
13		eqid	$⊢ LIdeal (R) = LIdeal (R)$
14	12 1 13	rspcl	$⊢ (R \in Ring \land \{X\} \subseteq B) \to RSpan (R) (\{X\}) \in LIdeal (R)$
15	8 11 14	syl2anc	$⊢ φ \to RSpan (R) (\{X\}) \in LIdeal (R)$
16	15	adantr	$⊢ (φ \land \neg X \in U) \to RSpan (R) (\{X\}) \in LIdeal (R)$
17		eqid	$⊢ RSpan (R) (\{X\}) = RSpan (R) (\{X\})$
18	2 12 17 1 10 3	unitpidl1	$⊢ φ \to (RSpan (R) (\{X\}) = B \leftrightarrow X \in U)$
19	18	notbid	$⊢ φ \to (\neg RSpan (R) (\{X\}) = B \leftrightarrow \neg X \in U)$
20	19	biimpar	$⊢ (φ \land \neg X \in U) \to \neg RSpan (R) (\{X\}) = B$
21	20	neqned	$⊢ (φ \land \neg X \in U) \to RSpan (R) (\{X\}) \neq B$
22	1	ssmxidl	$⊢ (R \in Ring \land RSpan (R) (\{X\}) \in LIdeal (R) \land RSpan (R) (\{X\}) \neq B) \to \exists m \in MaxIdeal (R) RSpan (R) (\{X\}) \subseteq m$
23	9 16 21 22	syl3anc	$⊢ (φ \land \neg X \in U) \to \exists m \in MaxIdeal (R) RSpan (R) (\{X\}) \subseteq m$
24	5	adantr	$⊢ (φ \land \neg X \in U) \to MaxIdeal (R) = \{M\}$
25	23 24	rexeqtrdv	$⊢ (φ \land \neg X \in U) \to \exists m \in \{M\} RSpan (R) (\{X\}) \subseteq m$
26		sseq2	$⊢ m = M \to (RSpan (R) (\{X\}) \subseteq m \leftrightarrow RSpan (R) (\{X\}) \subseteq M)$
27	26	rexsng	$⊢ M \in MaxIdeal (R) \to (\exists m \in \{M\} RSpan (R) (\{X\}) \subseteq m \leftrightarrow RSpan (R) (\{X\}) \subseteq M)$
28	27	biimpa	$⊢ (M \in MaxIdeal (R) \land \exists m \in \{M\} RSpan (R) (\{X\}) \subseteq m) \to RSpan (R) (\{X\}) \subseteq M$
29	7 25 28	syl2anc	$⊢ (φ \land \neg X \in U) \to RSpan (R) (\{X\}) \subseteq M$
30	1 12	rspsnid	$⊢ (R \in Ring \land X \in B) \to X \in RSpan (R) (\{X\})$
31	8 10 30	syl2anc	$⊢ φ \to X \in RSpan (R) (\{X\})$
32	6	eldifbd	$⊢ φ \to \neg X \in M$
33		nelss	$⊢ (X \in RSpan (R) (\{X\}) \land \neg X \in M) \to \neg RSpan (R) (\{X\}) \subseteq M$
34	31 32 33	syl2anc	$⊢ φ \to \neg RSpan (R) (\{X\}) \subseteq M$
35	34	adantr	$⊢ (φ \land \neg X \in U) \to \neg RSpan (R) (\{X\}) \subseteq M$
36	29 35	condan	$⊢ φ \to X \in U$

Metamath Proof Explorer

Theorem dflringlem

Proof