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	|- B = ( Base ` R )
	drngnidl.z	|- .0. = ( 0g ` R )
	drngnidl.u	|- U = ( LIdeal ` R )
Assertion	drngnidl	|- ( R e. DivRing -> U = { { .0. } , B } )

Proof

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