This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )