drngidlhash

Description: A ring is a division ring if and only if it admits exactly two ideals. (Proposed by Gerard Lang, 13-Mar-2025.) (Contributed by Thierry Arnoux, 13-Mar-2025)

		Ref	Expression
	Hypothesis	drngidlhash.u	$⊢ U = LIdeal (R)$
	Assertion	drngidlhash	$⊢ R \in Ring \to (R \in DivRing \leftrightarrow \|U\| = 2)$

Proof

Step	Hyp	Ref	Expression
1		drngidlhash.u	$⊢ U = LIdeal (R)$
2		eqid	$⊢ {Base}_{R} = {Base}_{R}$
3		eqid	$⊢ 0_{R} = 0_{R}$
4	2 3 1	drngnidl	$⊢ R \in DivRing \to U = \{\{0_{R}\}, {Base}_{R}\}$
5	4	fveq2d	$⊢ R \in DivRing \to \|U\| = \|\{\{0_{R}\}, {Base}_{R}\}\|$
6		drngnzr	$⊢ R \in DivRing \to R \in NzRing$
7		nzrring	$⊢ R \in NzRing \to R \in Ring$
8		eqid	$⊢ 1_{R} = 1_{R}$
9	2 8	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
10	7 9	syl	$⊢ R \in NzRing \to 1_{R} \in {Base}_{R}$
11	8 3	nzrnz	$⊢ R \in NzRing \to 1_{R} \neq 0_{R}$
12		nelsn	$⊢ 1_{R} \neq 0_{R} \to \neg 1_{R} \in \{0_{R}\}$
13	11 12	syl	$⊢ R \in NzRing \to \neg 1_{R} \in \{0_{R}\}$
14		nelne1	$⊢ (1_{R} \in {Base}_{R} \land \neg 1_{R} \in \{0_{R}\}) \to {Base}_{R} \neq \{0_{R}\}$
15	10 13 14	syl2anc	$⊢ R \in NzRing \to {Base}_{R} \neq \{0_{R}\}$
16	15	necomd	$⊢ R \in NzRing \to \{0_{R}\} \neq {Base}_{R}$
17	6 16	syl	$⊢ R \in DivRing \to \{0_{R}\} \neq {Base}_{R}$
18		snex	$⊢ \{0_{R}\} \in V$
19		fvex	$⊢ {Base}_{R} \in V$
20		hashprg	$⊢ (\{0_{R}\} \in V \land {Base}_{R} \in V) \to (\{0_{R}\} \neq {Base}_{R} \leftrightarrow \|\{\{0_{R}\}, {Base}_{R}\}\| = 2)$
21	18 19 20	mp2an	$⊢ \{0_{R}\} \neq {Base}_{R} \leftrightarrow \|\{\{0_{R}\}, {Base}_{R}\}\| = 2$
22	17 21	sylib	$⊢ R \in DivRing \to \|\{\{0_{R}\}, {Base}_{R}\}\| = 2$
23	5 22	eqtrd	$⊢ R \in DivRing \to \|U\| = 2$
24	23	adantl	$⊢ (R \in Ring \land R \in DivRing) \to \|U\| = 2$
25		simpl	$⊢ (R \in Ring \land \|U\| = 2) \to R \in Ring$
26		simplr	$⊢ ((R \in Ring \land \|U\| = 2) \land \{0_{R}\} = {Base}_{R}) \to \|U\| = 2$
27		2re	$⊢ 2 \in ℝ$
28	26 27	eqeltrdi	$⊢ ((R \in Ring \land \|U\| = 2) \land \{0_{R}\} = {Base}_{R}) \to \|U\| \in ℝ$
29		simpl	$⊢ (R \in Ring \land \{0_{R}\} = {Base}_{R}) \to R \in Ring$
30		simpr	$⊢ (R \in Ring \land \{0_{R}\} = {Base}_{R}) \to \{0_{R}\} = {Base}_{R}$
31	30	fveq2d	$⊢ (R \in Ring \land \{0_{R}\} = {Base}_{R}) \to \|\{0_{R}\}\| = \|{Base}_{R}\|$
32		fvex	$⊢ 0_{R} \in V$
33		hashsng	$⊢ 0_{R} \in V \to \|\{0_{R}\}\| = 1$
34	32 33	ax-mp	$⊢ \|\{0_{R}\}\| = 1$
35	31 34	eqtr3di	$⊢ (R \in Ring \land \{0_{R}\} = {Base}_{R}) \to \|{Base}_{R}\| = 1$
36	2 3	0ringidl	$⊢ (R \in Ring \land \|{Base}_{R}\| = 1) \to LIdeal (R) = \{\{0_{R}\}\}$
37	29 35 36	syl2anc	$⊢ (R \in Ring \land \{0_{R}\} = {Base}_{R}) \to LIdeal (R) = \{\{0_{R}\}\}$
38	1 37	eqtrid	$⊢ (R \in Ring \land \{0_{R}\} = {Base}_{R}) \to U = \{\{0_{R}\}\}$
39	38	fveq2d	$⊢ (R \in Ring \land \{0_{R}\} = {Base}_{R}) \to \|U\| = \|\{\{0_{R}\}\}\|$
40		hashsng	$⊢ \{0_{R}\} \in V \to \|\{\{0_{R}\}\}\| = 1$
41	18 40	ax-mp	$⊢ \|\{\{0_{R}\}\}\| = 1$
42	39 41	eqtrdi	$⊢ (R \in Ring \land \{0_{R}\} = {Base}_{R}) \to \|U\| = 1$
43	42	adantlr	$⊢ ((R \in Ring \land \|U\| = 2) \land \{0_{R}\} = {Base}_{R}) \to \|U\| = 1$
44		1lt2	$⊢ 1 < 2$
45	43 44	eqbrtrdi	$⊢ ((R \in Ring \land \|U\| = 2) \land \{0_{R}\} = {Base}_{R}) \to \|U\| < 2$
46	28 45	ltned	$⊢ ((R \in Ring \land \|U\| = 2) \land \{0_{R}\} = {Base}_{R}) \to \|U\| \neq 2$
47	46	neneqd	$⊢ ((R \in Ring \land \|U\| = 2) \land \{0_{R}\} = {Base}_{R}) \to \neg \|U\| = 2$
48	26 47	pm2.65da	$⊢ (R \in Ring \land \|U\| = 2) \to \neg \{0_{R}\} = {Base}_{R}$
49	48	neqned	$⊢ (R \in Ring \land \|U\| = 2) \to \{0_{R}\} \neq {Base}_{R}$
50	2 3 8	01eq0ring	$⊢ (R \in Ring \land 0_{R} = 1_{R}) \to {Base}_{R} = \{0_{R}\}$
51	50	eqcomd	$⊢ (R \in Ring \land 0_{R} = 1_{R}) \to \{0_{R}\} = {Base}_{R}$
52	51	ex	$⊢ R \in Ring \to (0_{R} = 1_{R} \to \{0_{R}\} = {Base}_{R})$
53	52	necon3d	$⊢ R \in Ring \to (\{0_{R}\} \neq {Base}_{R} \to 0_{R} \neq 1_{R})$
54	25 49 53	sylc	$⊢ (R \in Ring \land \|U\| = 2) \to 0_{R} \neq 1_{R}$
55	54	necomd	$⊢ (R \in Ring \land \|U\| = 2) \to 1_{R} \neq 0_{R}$
56	8 3	isnzr	$⊢ R \in NzRing \leftrightarrow (R \in Ring \land 1_{R} \neq 0_{R})$
57	25 55 56	sylanbrc	$⊢ (R \in Ring \land \|U\| = 2) \to R \in NzRing$
58	1	fvexi	$⊢ U \in V$
59	58	a1i	$⊢ (R \in Ring \land \|U\| = 2) \to U \in V$
60		simpr	$⊢ (R \in Ring \land \|U\| = 2) \to \|U\| = 2$
61	1 3	lidl0	$⊢ R \in Ring \to \{0_{R}\} \in U$
62	25 61	syl	$⊢ (R \in Ring \land \|U\| = 2) \to \{0_{R}\} \in U$
63	1 2	lidl1	$⊢ R \in Ring \to {Base}_{R} \in U$
64	25 63	syl	$⊢ (R \in Ring \land \|U\| = 2) \to {Base}_{R} \in U$
65		hash2prd	$⊢ (U \in V \land \|U\| = 2) \to ((\{0_{R}\} \in U \land {Base}_{R} \in U \land \{0_{R}\} \neq {Base}_{R}) \to U = \{\{0_{R}\}, {Base}_{R}\})$
66	65	imp	$⊢ ((U \in V \land \|U\| = 2) \land (\{0_{R}\} \in U \land {Base}_{R} \in U \land \{0_{R}\} \neq {Base}_{R})) \to U = \{\{0_{R}\}, {Base}_{R}\}$
67	59 60 62 64 49 66	syl23anc	$⊢ (R \in Ring \land \|U\| = 2) \to U = \{\{0_{R}\}, {Base}_{R}\}$
68	2 3 1	drngidl	$⊢ R \in NzRing \to (R \in DivRing \leftrightarrow U = \{\{0_{R}\}, {Base}_{R}\})$
69	68	biimpar	$⊢ (R \in NzRing \land U = \{\{0_{R}\}, {Base}_{R}\}) \to R \in DivRing$
70	57 67 69	syl2anc	$⊢ (R \in Ring \land \|U\| = 2) \to R \in DivRing$
71	24 70	impbida	$⊢ R \in Ring \to (R \in DivRing \leftrightarrow \|U\| = 2)$

Metamath Proof Explorer

Theorem drngidlhash

Proof