Theorem zar0ring

Description: The Zariski Topology of the trivial ring. (Contributed by Thierry Arnoux, 1-Jul-2024)

	Ref	Expression
Hypotheses	zartop.1	No typesetting found for |- S = ( Spec ` R ) with typecode |-
	zartop.2	$$⊢J=\mathrm{TopOpen}\left(S\right)$$
	zar0ring.b	$$⊢B={\mathrm{Base}}_R$$
Assertion	zar0ring	$$⊢\left(R\in \mathrm{Ring}\wedge \left|B\right|=1\right)\to J=\left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		zartop.1	Could not format S = ( Spec ` R ) : No typesetting found for |- S = ( Spec ` R ) with typecode |-
2		zartop.2	$$⊢J=\mathrm{TopOpen}\left(S\right)$$
3		zar0ring.b	$$⊢B={\mathrm{Base}}_R$$
4		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
5		eqid	Could not format ( PrmIdeal ` R ) = ( PrmIdeal ` R ) : No typesetting found for |- ( PrmIdeal ` R ) = ( PrmIdeal ` R ) with typecode |-
6		eqid	Could not format ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) : No typesetting found for |- ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) with typecode |-
7	1 4 5 6	rspectopn	Could not format ( R e. Ring -> ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = ( TopOpen ` S ) ) : No typesetting found for |- ( R e. Ring -> ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = ( TopOpen ` S ) ) with typecode |-
8	7	adantr	Could not format ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = ( TopOpen ` S ) ) : No typesetting found for |- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = ( TopOpen ` S ) ) with typecode |-
9	2 8	eqtr4id	Could not format ( ( R e. Ring /\ ( # ` B ) = 1 ) -> J = ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) ) : No typesetting found for |- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> J = ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) ) with typecode |-
10		fvex	Could not format ( PrmIdeal ` R ) e. _V : No typesetting found for |- ( PrmIdeal ` R ) e. _V with typecode |-
11	10	rabex	Could not format { j e. ( PrmIdeal ` R ) | -. i C_ j } e. _V : No typesetting found for |- { j e. ( PrmIdeal ` R ) | -. i C_ j } e. _V with typecode |-
12		eqid	Could not format ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) : No typesetting found for |- ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) with typecode |-
13	11 12	fnmpti	Could not format ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) Fn ( LIdeal ` R ) : No typesetting found for |- ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) Fn ( LIdeal ` R ) with typecode |-
14	13	a1i	Could not format ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) Fn ( LIdeal ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) Fn ( LIdeal ` R ) ) with typecode |-
15		eqid	$$⊢0_R=0_R$$
16	3 15	0ringidl	$$⊢\left(R\in \mathrm{Ring}\wedge \left|B\right|=1\right)\to \mathrm{LIdeal}\left(R\right)=\left\{\left\{0_R\right\}\right\}$$
17		snex	$$⊢\left\{0_R\right\}\in \mathrm{V}$$
18	17	a1i	$$⊢\left(R\in \mathrm{Ring}\wedge \left|B\right|=1\right)\to \left\{0_R\right\}\in \mathrm{V}$$
19	18	snn0d	$$⊢\left(R\in \mathrm{Ring}\wedge \left|B\right|=1\right)\to \left\{\left\{0_R\right\}\right\}\ne \varnothing$$
20	16 19	eqnetrd	$$⊢\left(R\in \mathrm{Ring}\wedge \left|B\right|=1\right)\to \mathrm{LIdeal}\left(R\right)\ne \varnothing$$
21	3	0ringprmidl	Could not format ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( PrmIdeal ` R ) = (/) ) : No typesetting found for |- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( PrmIdeal ` R ) = (/) ) with typecode |-
22	21	rabeqdv	Could not format ( ( R e. Ring /\ ( # ` B ) = 1 ) -> { j e. ( PrmIdeal ` R ) | -. i C_ j } = { j e. (/) | -. i C_ j } ) : No typesetting found for |- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> { j e. ( PrmIdeal ` R ) | -. i C_ j } = { j e. (/) | -. i C_ j } ) with typecode |-
23		rab0	$$⊢\left\{j\in \varnothing |\neg i\subseteq j\right\}=\varnothing$$
24	22 23	eqtrdi	Could not format ( ( R e. Ring /\ ( # ` B ) = 1 ) -> { j e. ( PrmIdeal ` R ) | -. i C_ j } = (/) ) : No typesetting found for |- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> { j e. ( PrmIdeal ` R ) | -. i C_ j } = (/) ) with typecode |-
25	24	mpteq2dv	Could not format ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = ( i e. ( LIdeal ` R ) |-> (/) ) ) : No typesetting found for |- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = ( i e. ( LIdeal ` R ) |-> (/) ) ) with typecode |-
26		fconstmpt	$$⊢\mathrm{LIdeal}\left(R\right)\times \left\{\varnothing \right\}=\left(i\in \mathrm{LIdeal}\left(R\right)⟼\varnothing \right)$$
27	25 26	eqtr4di	Could not format ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = ( ( LIdeal ` R ) X. { (/) } ) ) : No typesetting found for |- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = ( ( LIdeal ` R ) X. { (/) } ) ) with typecode |-
28		fconst5	Could not format ( ( ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) Fn ( LIdeal ` R ) /\ ( LIdeal ` R ) =/= (/) ) -> ( ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = ( ( LIdeal ` R ) X. { (/) } ) <-> ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = { (/) } ) ) : No typesetting found for |- ( ( ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) Fn ( LIdeal ` R ) /\ ( LIdeal ` R ) =/= (/) ) -> ( ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = ( ( LIdeal ` R ) X. { (/) } ) <-> ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = { (/) } ) ) with typecode |-
29	28	biimpa	Could not format ( ( ( ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) Fn ( LIdeal ` R ) /\ ( LIdeal ` R ) =/= (/) ) /\ ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = ( ( LIdeal ` R ) X. { (/) } ) ) -> ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = { (/) } ) : No typesetting found for |- ( ( ( ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) Fn ( LIdeal ` R ) /\ ( LIdeal ` R ) =/= (/) ) /\ ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = ( ( LIdeal ` R ) X. { (/) } ) ) -> ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = { (/) } ) with typecode |-
30	14 20 27 29	syl21anc	Could not format ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = { (/) } ) : No typesetting found for |- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = { (/) } ) with typecode |-
31	9 30	eqtrd	$$⊢\left(R\in \mathrm{Ring}\wedge \left|B\right|=1\right)\to J=\left\{\varnothing \right\}$$