Theorem drngmxidl

Description: The zero ideal is the only ideal of a division ring. (Contributed by Thierry Arnoux, 16-Mar-2025)

	Ref	Expression
Hypothesis	drngmxidl.1	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	drngmxidl	Could not format assertion : No typesetting found for |- ( R e. DivRing -> ( MaxIdeal ` R ) = { { .0. } } ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		drngmxidl.1	$$⊢\underset{\dot{}}{0}=0_R$$
2		drngring	$$⊢R\in \mathrm{DivRing}\to R\in \mathrm{Ring}$$
3		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
4	3	mxidlidl	Could not format ( ( R e. Ring /\ i e. ( MaxIdeal ` R ) ) -> i e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ i e. ( MaxIdeal ` R ) ) -> i e. ( LIdeal ` R ) ) with typecode |-
5	4	ex	Could not format ( R e. Ring -> ( i e. ( MaxIdeal ` R ) -> i e. ( LIdeal ` R ) ) ) : No typesetting found for |- ( R e. Ring -> ( i e. ( MaxIdeal ` R ) -> i e. ( LIdeal ` R ) ) ) with typecode |-
6	5	ssrdv	Could not format ( R e. Ring -> ( MaxIdeal ` R ) C_ ( LIdeal ` R ) ) : No typesetting found for |- ( R e. Ring -> ( MaxIdeal ` R ) C_ ( LIdeal ` R ) ) with typecode |-
7	2 6	syl	Could not format ( R e. DivRing -> ( MaxIdeal ` R ) C_ ( LIdeal ` R ) ) : No typesetting found for |- ( R e. DivRing -> ( MaxIdeal ` R ) C_ ( LIdeal ` R ) ) with typecode |-
8		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
9	3 1 8	drngnidl	$$⊢R\in \mathrm{DivRing}\to \mathrm{LIdeal}\left(R\right)=\left\{\left\{\underset{\dot{}}{0}\right\},{\mathrm{Base}}_R\right\}$$
10	7 9	sseqtrd	Could not format ( R e. DivRing -> ( MaxIdeal ` R ) C_ { { .0. } , ( Base ` R ) } ) : No typesetting found for |- ( R e. DivRing -> ( MaxIdeal ` R ) C_ { { .0. } , ( Base ` R ) } ) with typecode |-
11	3	mxidlnr	Could not format ( ( R e. Ring /\ i e. ( MaxIdeal ` R ) ) -> i =/= ( Base ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ i e. ( MaxIdeal ` R ) ) -> i =/= ( Base ` R ) ) with typecode |-
12	2 11	sylan	Could not format ( ( R e. DivRing /\ i e. ( MaxIdeal ` R ) ) -> i =/= ( Base ` R ) ) : No typesetting found for |- ( ( R e. DivRing /\ i e. ( MaxIdeal ` R ) ) -> i =/= ( Base ` R ) ) with typecode |-
13	12	nelrdva	Could not format ( R e. DivRing -> -. ( Base ` R ) e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( R e. DivRing -> -. ( Base ` R ) e. ( MaxIdeal ` R ) ) with typecode |-
14		ssdifsn	Could not format ( ( MaxIdeal ` R ) C_ ( { { .0. } , ( Base ` R ) } \ { ( Base ` R ) } ) <-> ( ( MaxIdeal ` R ) C_ { { .0. } , ( Base ` R ) } /\ -. ( Base ` R ) e. ( MaxIdeal ` R ) ) ) : No typesetting found for |- ( ( MaxIdeal ` R ) C_ ( { { .0. } , ( Base ` R ) } \ { ( Base ` R ) } ) <-> ( ( MaxIdeal ` R ) C_ { { .0. } , ( Base ` R ) } /\ -. ( Base ` R ) e. ( MaxIdeal ` R ) ) ) with typecode |-
15	10 13 14	sylanbrc	Could not format ( R e. DivRing -> ( MaxIdeal ` R ) C_ ( { { .0. } , ( Base ` R ) } \ { ( Base ` R ) } ) ) : No typesetting found for |- ( R e. DivRing -> ( MaxIdeal ` R ) C_ ( { { .0. } , ( Base ` R ) } \ { ( Base ` R ) } ) ) with typecode |-
16		drngnzr	$$⊢R\in \mathrm{DivRing}\to R\in \mathrm{NzRing}$$
17	1 3	drnglidl1ne0	$$⊢R\in \mathrm{NzRing}\to {\mathrm{Base}}_R\ne \left\{\underset{\dot{}}{0}\right\}$$
18	17	necomd	$$⊢R\in \mathrm{NzRing}\to \left\{\underset{\dot{}}{0}\right\}\ne {\mathrm{Base}}_R$$
19		difprsn2	$$⊢\left\{\underset{\dot{}}{0}\right\}\ne {\mathrm{Base}}_R\to \left\{\left\{\underset{\dot{}}{0}\right\},{\mathrm{Base}}_R\right\}\setminus \left\{{\mathrm{Base}}_R\right\}=\left\{\left\{\underset{\dot{}}{0}\right\}\right\}$$
20	16 18 19	3syl	$$⊢R\in \mathrm{DivRing}\to \left\{\left\{\underset{\dot{}}{0}\right\},{\mathrm{Base}}_R\right\}\setminus \left\{{\mathrm{Base}}_R\right\}=\left\{\left\{\underset{\dot{}}{0}\right\}\right\}$$
21	15 20	sseqtrd	Could not format ( R e. DivRing -> ( MaxIdeal ` R ) C_ { { .0. } } ) : No typesetting found for |- ( R e. DivRing -> ( MaxIdeal ` R ) C_ { { .0. } } ) with typecode |-
22	1	drng0mxidl	Could not format ( R e. DivRing -> { .0. } e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( R e. DivRing -> { .0. } e. ( MaxIdeal ` R ) ) with typecode |-
23	22	snssd	Could not format ( R e. DivRing -> { { .0. } } C_ ( MaxIdeal ` R ) ) : No typesetting found for |- ( R e. DivRing -> { { .0. } } C_ ( MaxIdeal ` R ) ) with typecode |-
24	21 23	eqssd	Could not format ( R e. DivRing -> ( MaxIdeal ` R ) = { { .0. } } ) : No typesetting found for |- ( R e. DivRing -> ( MaxIdeal ` R ) = { { .0. } } ) with typecode |-