Theorem 0ringprmidl

Description: The trivial ring does not have any prime ideal. (Contributed by Thierry Arnoux, 30-Jun-2024)

	Ref	Expression
Hypothesis	0ringprmidl.1	$$⊢B={\mathrm{Base}}_R$$
Assertion	0ringprmidl	Could not format assertion : No typesetting found for |- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( PrmIdeal ` R ) = (/) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		0ringprmidl.1	$$⊢B={\mathrm{Base}}_R$$
2		prmidlssidl	Could not format ( R e. Ring -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) ) : No typesetting found for |- ( R e. Ring -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) ) with typecode |-
3	2	adantr	Could not format ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) ) with typecode |-
4		eqid	$$⊢0_R=0_R$$
5	1 4	0ringidl	$$⊢\left(R\in \mathrm{Ring}\wedge \left|B\right|=1\right)\to \mathrm{LIdeal}\left(R\right)=\left\{\left\{0_R\right\}\right\}$$
6	3 5	sseqtrd	Could not format ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( PrmIdeal ` R ) C_ { { ( 0g ` R ) } } ) : No typesetting found for |- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( PrmIdeal ` R ) C_ { { ( 0g ` R ) } } ) with typecode |-
7	6	sselda	Could not format ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> i e. { { ( 0g ` R ) } } ) : No typesetting found for |- ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> i e. { { ( 0g ` R ) } } ) with typecode |-
8		elsni	$$⊢i\in \left\{\left\{0_R\right\}\right\}\to i=\left\{0_R\right\}$$
9	7 8	syl	Could not format ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> i = { ( 0g ` R ) } ) : No typesetting found for |- ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> i = { ( 0g ` R ) } ) with typecode |-
10		eqid	$$⊢{\cdot }_R={\cdot }_R$$
11	1 10	prmidlnr	Could not format ( ( R e. Ring /\ i e. ( PrmIdeal ` R ) ) -> i =/= B ) : No typesetting found for |- ( ( R e. Ring /\ i e. ( PrmIdeal ` R ) ) -> i =/= B ) with typecode |-
12	11	adantlr	Could not format ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> i =/= B ) : No typesetting found for |- ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> i =/= B ) with typecode |-
13	1 4	0ring	$$⊢\left(R\in \mathrm{Ring}\wedge \left|B\right|=1\right)\to B=\left\{0_R\right\}$$
14	13	adantr	Could not format ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> B = { ( 0g ` R ) } ) : No typesetting found for |- ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> B = { ( 0g ` R ) } ) with typecode |-
15	12 14	neeqtrd	Could not format ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> i =/= { ( 0g ` R ) } ) : No typesetting found for |- ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> i =/= { ( 0g ` R ) } ) with typecode |-
16	15	neneqd	Could not format ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> -. i = { ( 0g ` R ) } ) : No typesetting found for |- ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> -. i = { ( 0g ` R ) } ) with typecode |-
17	9 16	pm2.65da	Could not format ( ( R e. Ring /\ ( # ` B ) = 1 ) -> -. i e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> -. i e. ( PrmIdeal ` R ) ) with typecode |-
18	17	eq0rdv	Could not format ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( PrmIdeal ` R ) = (/) ) : No typesetting found for |- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( PrmIdeal ` R ) = (/) ) with typecode |-