Theorem 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	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
Assertion	drngidlhash	⊢ ( 𝑅 ∈ Ring → ( 𝑅 ∈ DivRing ↔ ( ♯ ‘ 𝑈 ) = 2 ) )

Proof

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