drngidl

Description: A nonzero ring is a division ring if and only if its only left ideals are the zero ideal and the unit ideal. (Proposed by Gerard Lang, 13-Mar-2025.) (Contributed by Thierry Arnoux, 13-Mar-2025)

	Ref	Expression
Hypotheses	drngidl.b	$⊢ B = {Base}_{R}$
	drngidl.z	$⊢ \underset{˙}{0} = 0_{R}$
	drngidl.u	$⊢ U = LIdeal (R)$
Assertion	drngidl	$⊢ R \in NzRing \to (R \in DivRing \leftrightarrow U = \{\{\underset{˙}{0}\}, B\})$

Proof

Step	Hyp	Ref	Expression
1		drngidl.b	$⊢ B = {Base}_{R}$
2		drngidl.z	$⊢ \underset{˙}{0} = 0_{R}$
3		drngidl.u	$⊢ U = LIdeal (R)$
4	1 2 3	drngnidl	$⊢ R \in DivRing \to U = \{\{\underset{˙}{0}\}, B\}$
5	4	adantl	$⊢ (R \in NzRing \land R \in DivRing) \to U = \{\{\underset{˙}{0}\}, B\}$
6		eqid	$⊢ 1_{R} = 1_{R}$
7	6 2	nzrnz	$⊢ R \in NzRing \to 1_{R} \neq \underset{˙}{0}$
8	7	adantr	$⊢ (R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \to 1_{R} \neq \underset{˙}{0}$
9		eqid	$⊢ \cdot_{R} = \cdot_{R}$
10		eqid	$⊢ Unit (R) = Unit (R)$
11		nzrring	$⊢ R \in NzRing \to R \in Ring$
12	11	adantr	$⊢ (R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \to R \in Ring$
13	12	adantr	$⊢ ((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \to R \in Ring$
14	13	ad4antr	$⊢ ((((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \land z \in B) \land 1_{R} = z \cdot_{R} y) \to R \in Ring$
15		simp-4r	$⊢ ((((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \land z \in B) \land 1_{R} = z \cdot_{R} y) \to y \in B$
16		simplr	$⊢ ((((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \land z \in B) \land 1_{R} = z \cdot_{R} y) \to z \in B$
17		simpr	$⊢ ((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \to x \in (B ∖ \{\underset{˙}{0}\})$
18	17	eldifad	$⊢ ((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \to x \in B$
19	18	ad2antrr	$⊢ ((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \to x \in B$
20	19	ad2antrr	$⊢ ((((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \land z \in B) \land 1_{R} = z \cdot_{R} y) \to x \in B$
21		simpr	$⊢ ((((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \land z \in B) \land 1_{R} = z \cdot_{R} y) \to 1_{R} = z \cdot_{R} y$
22	21	eqcomd	$⊢ ((((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \land z \in B) \land 1_{R} = z \cdot_{R} y) \to z \cdot_{R} y = 1_{R}$
23		simpr	$⊢ ((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \to 1_{R} = y \cdot_{R} x$
24	23	eqcomd	$⊢ ((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \to y \cdot_{R} x = 1_{R}$
25	24	ad2antrr	$⊢ ((((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \land z \in B) \land 1_{R} = z \cdot_{R} y) \to y \cdot_{R} x = 1_{R}$
26	1 2 6 9 10 14 15 16 20 22 25	ringinveu	$⊢ ((((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \land z \in B) \land 1_{R} = z \cdot_{R} y) \to x = z$
27	26	oveq1d	$⊢ ((((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \land z \in B) \land 1_{R} = z \cdot_{R} y) \to x \cdot_{R} y = z \cdot_{R} y$
28	27 22	eqtrd	$⊢ ((((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \land z \in B) \land 1_{R} = z \cdot_{R} y) \to x \cdot_{R} y = 1_{R}$
29	13	ad2antrr	$⊢ ((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \to R \in Ring$
30		simplr	$⊢ ((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \to y \in B$
31	1 6	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
32	13 31	syl	$⊢ ((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \to 1_{R} \in B$
33	32	ad2antrr	$⊢ ((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \to 1_{R} \in B$
34	30	snssd	$⊢ ((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \to \{y\} \subseteq B$
35		eqid	$⊢ RSpan (R) = RSpan (R)$
36	35 1 3	rspcl	$⊢ (R \in Ring \land \{y\} \subseteq B) \to RSpan (R) (\{y\}) \in U$
37	29 34 36	syl2anc	$⊢ ((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \to RSpan (R) (\{y\}) \in U$
38		simp-4r	$⊢ ((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \to U = \{\{\underset{˙}{0}\}, B\}$
39	37 38	eleqtrd	$⊢ ((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \to RSpan (R) (\{y\}) \in \{\{\underset{˙}{0}\}, B\}$
40		elpri	$⊢ RSpan (R) (\{y\}) \in \{\{\underset{˙}{0}\}, B\} \to (RSpan (R) (\{y\}) = \{\underset{˙}{0}\} \lor RSpan (R) (\{y\}) = B)$
41	39 40	syl	$⊢ ((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \to (RSpan (R) (\{y\}) = \{\underset{˙}{0}\} \lor RSpan (R) (\{y\}) = B)$
42		simplr	$⊢ (((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \land y = \underset{˙}{0}) \to 1_{R} = y \cdot_{R} x$
43		simpr	$⊢ (((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \land y = \underset{˙}{0}) \to y = \underset{˙}{0}$
44	43	oveq1d	$⊢ (((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \land y = \underset{˙}{0}) \to y \cdot_{R} x = \underset{˙}{0} \cdot_{R} x$
45	1 9 2	ringlz	$⊢ (R \in Ring \land x \in B) \to \underset{˙}{0} \cdot_{R} x = \underset{˙}{0}$
46	13 18 45	syl2anc	$⊢ ((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \to \underset{˙}{0} \cdot_{R} x = \underset{˙}{0}$
47	46	ad3antrrr	$⊢ (((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \land y = \underset{˙}{0}) \to \underset{˙}{0} \cdot_{R} x = \underset{˙}{0}$
48	42 44 47	3eqtrd	$⊢ (((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \land y = \underset{˙}{0}) \to 1_{R} = \underset{˙}{0}$
49	8	ad4antr	$⊢ (((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \land y = \underset{˙}{0}) \to 1_{R} \neq \underset{˙}{0}$
50	49	neneqd	$⊢ (((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \land y = \underset{˙}{0}) \to \neg 1_{R} = \underset{˙}{0}$
51	48 50	pm2.65da	$⊢ ((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \to \neg y = \underset{˙}{0}$
52	51	neqned	$⊢ ((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \to y \neq \underset{˙}{0}$
53	1 2 35	pidlnz	$⊢ (R \in Ring \land y \in B \land y \neq \underset{˙}{0}) \to RSpan (R) (\{y\}) \neq \{\underset{˙}{0}\}$
54	29 30 52 53	syl3anc	$⊢ ((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \to RSpan (R) (\{y\}) \neq \{\underset{˙}{0}\}$
55	54	neneqd	$⊢ ((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \to \neg RSpan (R) (\{y\}) = \{\underset{˙}{0}\}$
56	41 55	orcnd	$⊢ ((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \to RSpan (R) (\{y\}) = B$
57	33 56	eleqtrrd	$⊢ ((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \to 1_{R} \in RSpan (R) (\{y\})$
58	1 9 35	elrspsn	$⊢ (R \in Ring \land y \in B) \to (1_{R} \in RSpan (R) (\{y\}) \leftrightarrow \exists z \in B 1_{R} = z \cdot_{R} y)$
59	58	biimpa	$⊢ ((R \in Ring \land y \in B) \land 1_{R} \in RSpan (R) (\{y\})) \to \exists z \in B 1_{R} = z \cdot_{R} y$
60	29 30 57 59	syl21anc	$⊢ ((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \to \exists z \in B 1_{R} = z \cdot_{R} y$
61	28 60	r19.29a	$⊢ ((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \to x \cdot_{R} y = 1_{R}$
62	61 24	jca	$⊢ ((((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land y \in B) \land 1_{R} = y \cdot_{R} x) \to (x \cdot_{R} y = 1_{R} \land y \cdot_{R} x = 1_{R})$
63	62	anasss	$⊢ (((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land (y \in B \land 1_{R} = y \cdot_{R} x)) \to (x \cdot_{R} y = 1_{R} \land y \cdot_{R} x = 1_{R})$
64	18	snssd	$⊢ ((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \to \{x\} \subseteq B$
65	35 1 3	rspcl	$⊢ (R \in Ring \land \{x\} \subseteq B) \to RSpan (R) (\{x\}) \in U$
66	13 64 65	syl2anc	$⊢ ((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \to RSpan (R) (\{x\}) \in U$
67		simplr	$⊢ ((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \to U = \{\{\underset{˙}{0}\}, B\}$
68	66 67	eleqtrd	$⊢ ((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \to RSpan (R) (\{x\}) \in \{\{\underset{˙}{0}\}, B\}$
69		elpri	$⊢ RSpan (R) (\{x\}) \in \{\{\underset{˙}{0}\}, B\} \to (RSpan (R) (\{x\}) = \{\underset{˙}{0}\} \lor RSpan (R) (\{x\}) = B)$
70	68 69	syl	$⊢ ((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \to (RSpan (R) (\{x\}) = \{\underset{˙}{0}\} \lor RSpan (R) (\{x\}) = B)$
71		eldifsni	$⊢ x \in (B ∖ \{\underset{˙}{0}\}) \to x \neq \underset{˙}{0}$
72	71	adantl	$⊢ ((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \to x \neq \underset{˙}{0}$
73	1 2 35	pidlnz	$⊢ (R \in Ring \land x \in B \land x \neq \underset{˙}{0}) \to RSpan (R) (\{x\}) \neq \{\underset{˙}{0}\}$
74	13 18 72 73	syl3anc	$⊢ ((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \to RSpan (R) (\{x\}) \neq \{\underset{˙}{0}\}$
75	74	neneqd	$⊢ ((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \to \neg RSpan (R) (\{x\}) = \{\underset{˙}{0}\}$
76	70 75	orcnd	$⊢ ((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \to RSpan (R) (\{x\}) = B$
77	32 76	eleqtrrd	$⊢ ((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \to 1_{R} \in RSpan (R) (\{x\})$
78	1 9 35	elrspsn	$⊢ (R \in Ring \land x \in B) \to (1_{R} \in RSpan (R) (\{x\}) \leftrightarrow \exists y \in B 1_{R} = y \cdot_{R} x)$
79	78	biimpa	$⊢ ((R \in Ring \land x \in B) \land 1_{R} \in RSpan (R) (\{x\})) \to \exists y \in B 1_{R} = y \cdot_{R} x$
80	13 18 77 79	syl21anc	$⊢ ((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \to \exists y \in B 1_{R} = y \cdot_{R} x$
81	63 80	reximddv	$⊢ ((R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \to \exists y \in B (x \cdot_{R} y = 1_{R} \land y \cdot_{R} x = 1_{R})$
82	81	ralrimiva	$⊢ (R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \to \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B (x \cdot_{R} y = 1_{R} \land y \cdot_{R} x = 1_{R})$
83	1 2 6 9 10 12	isdrng4	$⊢ (R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \to (R \in DivRing \leftrightarrow (1_{R} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B (x \cdot_{R} y = 1_{R} \land y \cdot_{R} x = 1_{R})))$
84	8 82 83	mpbir2and	$⊢ (R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \to R \in DivRing$
85	5 84	impbida	$⊢ R \in NzRing \to (R \in DivRing \leftrightarrow U = \{\{\underset{˙}{0}\}, B\})$

Metamath Proof Explorer

Theorem drngidl

Proof