Metamath Proof Explorer

Theorem zar0ring

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

Ref Expression
Hypotheses zartop.1 
|- S = ( Spec ` R )
zartop.2 
|- J = ( TopOpen ` S )
zar0ring.b 
|- B = ( Base ` R )
Assertion zar0ring 
|- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> J = { (/) } )

Proof

Step Hyp Ref Expression
1 zartop.1 
 |-  S = ( Spec ` R )
2 zartop.2 
 |-  J = ( TopOpen ` S )
3 zar0ring.b 
 |-  B = ( Base ` R )
4 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
5 eqid 
 |-  ( PrmIdeal ` R ) = ( PrmIdeal ` R )
6 eqid 
 |-  ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } )
7 1 4 5 6 rspectopn 
 |-  ( R e. Ring -> ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = ( TopOpen ` S ) )
8 7 adantr 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = ( TopOpen ` S ) )
9 2 8 eqtr4id 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> J = ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) )
10 fvex 
 |-  ( PrmIdeal ` R ) e. _V
11 10 rabex 
 |-  { j e. ( PrmIdeal ` R ) | -. i C_ j } e. _V
12 eqid 
 |-  ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } )
13 11 12 fnmpti 
 |-  ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) Fn ( LIdeal ` R )
14 13 a1i 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) Fn ( LIdeal ` R ) )
15 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
16 3 15 0ringidl 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( LIdeal ` R ) = { { ( 0g ` R ) } } )
17 snex 
 |-  { ( 0g ` R ) } e. _V
18 17 a1i 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> { ( 0g ` R ) } e. _V )
19 18 snn0d 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> { { ( 0g ` R ) } } =/= (/) )
20 16 19 eqnetrd 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( LIdeal ` R ) =/= (/) )
21 3 0ringprmidl 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( PrmIdeal ` R ) = (/) )
22 21 rabeqdv 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> { j e. ( PrmIdeal ` R ) | -. i C_ j } = { j e. (/) | -. i C_ j } )
23 rab0 
 |-  { j e. (/) | -. i C_ j } = (/)
24 22 23 eqtrdi 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> { j e. ( PrmIdeal ` R ) | -. i C_ j } = (/) )
25 24 mpteq2dv 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = ( i e. ( LIdeal ` R ) |-> (/) ) )
26 fconstmpt 
 |-  ( ( LIdeal ` R ) X. { (/) } ) = ( i e. ( LIdeal ` R ) |-> (/) )
27 25 26 eqtr4di 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = ( ( LIdeal ` R ) X. { (/) } ) )
28 fconst5 
 |-  ( ( ( 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 } ) = { (/) } ) )
29 28 biimpa 
 |-  ( ( ( ( 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 } ) = { (/) } )
30 14 20 27 29 syl21anc 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | -. i C_ j } ) = { (/) } )
31 9 30 eqtrd 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> J = { (/) } )