Theorem 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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	drngnidl.z	⊢ 0 = ( 0g ‘ 𝑅 )
	drngnidl.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
Assertion	drngnidl	⊢ ( 𝑅 ∈ DivRing → 𝑈 = { { 0 } , 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		drngnidl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		drngnidl.z	⊢ 0 = ( 0g ‘ 𝑅 )
3		drngnidl.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
4		animorrl	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑎 = { 0 } ) → ( 𝑎 = { 0 } ∨ 𝑎 = 𝐵 ) )
5		drngring	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
6	5	ad2antrr	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑎 ≠ { 0 } ) → 𝑅 ∈ Ring )
7		simplr	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑎 ≠ { 0 } ) → 𝑎 ∈ 𝑈 )
8		simpr	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑎 ≠ { 0 } ) → 𝑎 ≠ { 0 } )
9	3 2	lidlnz	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝑈 ∧ 𝑎 ≠ { 0 } ) → ∃ 𝑏 ∈ 𝑎 𝑏 ≠ 0 )
10	6 7 8 9	syl3anc	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑎 ≠ { 0 } ) → ∃ 𝑏 ∈ 𝑎 𝑏 ≠ 0 )
11		simpll	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ ( 𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 ) ) → 𝑅 ∈ DivRing )
12	1 3	lidlss	⊢ ( 𝑎 ∈ 𝑈 → 𝑎 ⊆ 𝐵 )
13	12	adantl	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) → 𝑎 ⊆ 𝐵 )
14	13	sselda	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑎 ) → 𝑏 ∈ 𝐵 )
15	14	adantrr	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ ( 𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 ) ) → 𝑏 ∈ 𝐵 )
16		simprr	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ ( 𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 ) ) → 𝑏 ≠ 0 )
17		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
18		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
19		eqid	⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
20	1 2 17 18 19	drnginvrl	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑏 ∈ 𝐵 ∧ 𝑏 ≠ 0 ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑏 ) ( .r ‘ 𝑅 ) 𝑏 ) = ( 1r ‘ 𝑅 ) )
21	11 15 16 20	syl3anc	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ ( 𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑏 ) ( .r ‘ 𝑅 ) 𝑏 ) = ( 1r ‘ 𝑅 ) )
22	5	ad2antrr	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ ( 𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 ) ) → 𝑅 ∈ Ring )
23		simplr	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ ( 𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 ) ) → 𝑎 ∈ 𝑈 )
24	1 2 19	drnginvrcl	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑏 ∈ 𝐵 ∧ 𝑏 ≠ 0 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑏 ) ∈ 𝐵 )
25	11 15 16 24	syl3anc	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ ( 𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝑏 ) ∈ 𝐵 )
26		simprl	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ ( 𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 ) ) → 𝑏 ∈ 𝑎 )
27	3 1 17	lidlmcl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝑈 ) ∧ ( ( ( invr ‘ 𝑅 ) ‘ 𝑏 ) ∈ 𝐵 ∧ 𝑏 ∈ 𝑎 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑏 ) ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑎 )
28	22 23 25 26 27	syl22anc	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ ( 𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑏 ) ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑎 )
29	21 28	eqeltrrd	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ ( 𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 ) ) → ( 1r ‘ 𝑅 ) ∈ 𝑎 )
30	29	rexlimdvaa	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) → ( ∃ 𝑏 ∈ 𝑎 𝑏 ≠ 0 → ( 1r ‘ 𝑅 ) ∈ 𝑎 ) )
31	30	imp	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ ∃ 𝑏 ∈ 𝑎 𝑏 ≠ 0 ) → ( 1r ‘ 𝑅 ) ∈ 𝑎 )
32	10 31	syldan	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑎 ≠ { 0 } ) → ( 1r ‘ 𝑅 ) ∈ 𝑎 )
33	3 1 18	lidl1el	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝑈 ) → ( ( 1r ‘ 𝑅 ) ∈ 𝑎 ↔ 𝑎 = 𝐵 ) )
34	5 33	sylan	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) → ( ( 1r ‘ 𝑅 ) ∈ 𝑎 ↔ 𝑎 = 𝐵 ) )
35	34	adantr	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑎 ≠ { 0 } ) → ( ( 1r ‘ 𝑅 ) ∈ 𝑎 ↔ 𝑎 = 𝐵 ) )
36	32 35	mpbid	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑎 ≠ { 0 } ) → 𝑎 = 𝐵 )
37	36	olcd	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑎 ≠ { 0 } ) → ( 𝑎 = { 0 } ∨ 𝑎 = 𝐵 ) )
38	4 37	pm2.61dane	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) → ( 𝑎 = { 0 } ∨ 𝑎 = 𝐵 ) )
39		vex	⊢ 𝑎 ∈ V
40	39	elpr	⊢ ( 𝑎 ∈ { { 0 } , 𝐵 } ↔ ( 𝑎 = { 0 } ∨ 𝑎 = 𝐵 ) )
41	38 40	sylibr	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) → 𝑎 ∈ { { 0 } , 𝐵 } )
42	41	ex	⊢ ( 𝑅 ∈ DivRing → ( 𝑎 ∈ 𝑈 → 𝑎 ∈ { { 0 } , 𝐵 } ) )
43	42	ssrdv	⊢ ( 𝑅 ∈ DivRing → 𝑈 ⊆ { { 0 } , 𝐵 } )
44	3 2	lidl0	⊢ ( 𝑅 ∈ Ring → { 0 } ∈ 𝑈 )
45	3 1	lidl1	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ 𝑈 )
46	44 45	prssd	⊢ ( 𝑅 ∈ Ring → { { 0 } , 𝐵 } ⊆ 𝑈 )
47	5 46	syl	⊢ ( 𝑅 ∈ DivRing → { { 0 } , 𝐵 } ⊆ 𝑈 )
48	43 47	eqssd	⊢ ( 𝑅 ∈ DivRing → 𝑈 = { { 0 } , 𝐵 } )