drngnidl

Description: A division ring has only the two trivial ideals. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Wolf Lammen, 6-Sep-2020)

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

Proof

Step	Hyp	Ref	Expression
1		drngnidl.b	$⊢ B = {Base}_{R}$
2		drngnidl.z	$⊢ \underset{˙}{0} = 0_{R}$
3		drngnidl.u	$⊢ U = LIdeal (R)$
4		animorrl	$⊢ ((R \in DivRing \land a \in U) \land a = \{\underset{˙}{0}\}) \to (a = \{\underset{˙}{0}\} \lor a = B)$
5		drngring	$⊢ R \in DivRing \to R \in Ring$
6	5	ad2antrr	$⊢ ((R \in DivRing \land a \in U) \land a \neq \{\underset{˙}{0}\}) \to R \in Ring$
7		simplr	$⊢ ((R \in DivRing \land a \in U) \land a \neq \{\underset{˙}{0}\}) \to a \in U$
8		simpr	$⊢ ((R \in DivRing \land a \in U) \land a \neq \{\underset{˙}{0}\}) \to a \neq \{\underset{˙}{0}\}$
9	3 2	lidlnz	$⊢ (R \in Ring \land a \in U \land a \neq \{\underset{˙}{0}\}) \to \exists b \in a b \neq \underset{˙}{0}$
10	6 7 8 9	syl3anc	$⊢ ((R \in DivRing \land a \in U) \land a \neq \{\underset{˙}{0}\}) \to \exists b \in a b \neq \underset{˙}{0}$
11		simpll	$⊢ ((R \in DivRing \land a \in U) \land (b \in a \land b \neq \underset{˙}{0})) \to R \in DivRing$
12	1 3	lidlss	$⊢ a \in U \to a \subseteq B$
13	12	adantl	$⊢ (R \in DivRing \land a \in U) \to a \subseteq B$
14	13	sselda	$⊢ ((R \in DivRing \land a \in U) \land b \in a) \to b \in B$
15	14	adantrr	$⊢ ((R \in DivRing \land a \in U) \land (b \in a \land b \neq \underset{˙}{0})) \to b \in B$
16		simprr	$⊢ ((R \in DivRing \land a \in U) \land (b \in a \land b \neq \underset{˙}{0})) \to b \neq \underset{˙}{0}$
17		eqid	$⊢ \cdot_{R} = \cdot_{R}$
18		eqid	$⊢ 1_{R} = 1_{R}$
19		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
20	1 2 17 18 19	drnginvrl	$⊢ (R \in DivRing \land b \in B \land b \neq \underset{˙}{0}) \to {inv}_{r} (R) (b) \cdot_{R} b = 1_{R}$
21	11 15 16 20	syl3anc	$⊢ ((R \in DivRing \land a \in U) \land (b \in a \land b \neq \underset{˙}{0})) \to {inv}_{r} (R) (b) \cdot_{R} b = 1_{R}$
22	5	ad2antrr	$⊢ ((R \in DivRing \land a \in U) \land (b \in a \land b \neq \underset{˙}{0})) \to R \in Ring$
23		simplr	$⊢ ((R \in DivRing \land a \in U) \land (b \in a \land b \neq \underset{˙}{0})) \to a \in U$
24	1 2 19	drnginvrcl	$⊢ (R \in DivRing \land b \in B \land b \neq \underset{˙}{0}) \to {inv}_{r} (R) (b) \in B$
25	11 15 16 24	syl3anc	$⊢ ((R \in DivRing \land a \in U) \land (b \in a \land b \neq \underset{˙}{0})) \to {inv}_{r} (R) (b) \in B$
26		simprl	$⊢ ((R \in DivRing \land a \in U) \land (b \in a \land b \neq \underset{˙}{0})) \to b \in a$
27	3 1 17	lidlmcl	$⊢ ((R \in Ring \land a \in U) \land ({inv}_{r} (R) (b) \in B \land b \in a)) \to {inv}_{r} (R) (b) \cdot_{R} b \in a$
28	22 23 25 26 27	syl22anc	$⊢ ((R \in DivRing \land a \in U) \land (b \in a \land b \neq \underset{˙}{0})) \to {inv}_{r} (R) (b) \cdot_{R} b \in a$
29	21 28	eqeltrrd	$⊢ ((R \in DivRing \land a \in U) \land (b \in a \land b \neq \underset{˙}{0})) \to 1_{R} \in a$
30	29	rexlimdvaa	$⊢ (R \in DivRing \land a \in U) \to (\exists b \in a b \neq \underset{˙}{0} \to 1_{R} \in a)$
31	30	imp	$⊢ ((R \in DivRing \land a \in U) \land \exists b \in a b \neq \underset{˙}{0}) \to 1_{R} \in a$
32	10 31	syldan	$⊢ ((R \in DivRing \land a \in U) \land a \neq \{\underset{˙}{0}\}) \to 1_{R} \in a$
33	3 1 18	lidl1el	$⊢ (R \in Ring \land a \in U) \to (1_{R} \in a \leftrightarrow a = B)$
34	5 33	sylan	$⊢ (R \in DivRing \land a \in U) \to (1_{R} \in a \leftrightarrow a = B)$
35	34	adantr	$⊢ ((R \in DivRing \land a \in U) \land a \neq \{\underset{˙}{0}\}) \to (1_{R} \in a \leftrightarrow a = B)$
36	32 35	mpbid	$⊢ ((R \in DivRing \land a \in U) \land a \neq \{\underset{˙}{0}\}) \to a = B$
37	36	olcd	$⊢ ((R \in DivRing \land a \in U) \land a \neq \{\underset{˙}{0}\}) \to (a = \{\underset{˙}{0}\} \lor a = B)$
38	4 37	pm2.61dane	$⊢ (R \in DivRing \land a \in U) \to (a = \{\underset{˙}{0}\} \lor a = B)$
39		vex	$⊢ a \in V$
40	39	elpr	$⊢ a \in \{\{\underset{˙}{0}\}, B\} \leftrightarrow (a = \{\underset{˙}{0}\} \lor a = B)$
41	38 40	sylibr	$⊢ (R \in DivRing \land a \in U) \to a \in \{\{\underset{˙}{0}\}, B\}$
42	41	ex	$⊢ R \in DivRing \to (a \in U \to a \in \{\{\underset{˙}{0}\}, B\})$
43	42	ssrdv	$⊢ R \in DivRing \to U \subseteq \{\{\underset{˙}{0}\}, B\}$
44	3 2	lidl0	$⊢ R \in Ring \to \{\underset{˙}{0}\} \in U$
45	3 1	lidl1	$⊢ R \in Ring \to B \in U$
46	44 45	prssd	$⊢ R \in Ring \to \{\{\underset{˙}{0}\}, B\} \subseteq U$
47	5 46	syl	$⊢ R \in DivRing \to \{\{\underset{˙}{0}\}, B\} \subseteq U$
48	43 47	eqssd	$⊢ R \in DivRing \to U = \{\{\underset{˙}{0}\}, B\}$

Metamath Proof Explorer

Theorem drngnidl

Proof