Metamath Proof Explorer

Theorem 0ringufd

Description: A zero ring is a unique factorization domain. (Contributed by Thierry Arnoux, 18-May-2025)

Ref Expression
Hypotheses 0ringufd.1 
|- B = ( Base ` R )
0ringufd.2 
|- ( ph -> R e. Ring )
0ringufd.3 
|- ( ph -> ( # ` B ) = 1 )
Assertion 0ringufd 
|- ( ph -> R e. UFD )

Proof

Step Hyp Ref Expression
1 0ringufd.1 
 |-  B = ( Base ` R )
2 0ringufd.2 
 |-  ( ph -> R e. Ring )
3 0ringufd.3 
 |-  ( ph -> ( # ` B ) = 1 )
4 1 2 3 0ringcring 
 |-  ( ph -> R e. CRing )
5 eqid 
 |-  ( AbsVal ` R ) = ( AbsVal ` R )
6 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
7 eqid 
 |-  ( x e. B |-> if ( x = ( 0g ` R ) , 0 , 1 ) ) = ( x e. B |-> if ( x = ( 0g ` R ) , 0 , 1 ) )
8 eqid 
 |-  ( .r ` R ) = ( .r ` R )
9 simprl 
 |-  ( ( ph /\ ( a e. B /\ a =/= ( 0g ` R ) ) ) -> a e. B )
10 1 fveq2i 
 |-  ( # ` B ) = ( # ` ( Base ` R ) )
11 10 3 eqtr3id 
 |-  ( ph -> ( # ` ( Base ` R ) ) = 1 )
12 0ringnnzr 
 |-  ( R e. Ring -> ( ( # ` ( Base ` R ) ) = 1 <-> -. R e. NzRing ) )
13 12 biimpa 
 |-  ( ( R e. Ring /\ ( # ` ( Base ` R ) ) = 1 ) -> -. R e. NzRing )
14 2 11 13 syl2anc 
 |-  ( ph -> -. R e. NzRing )
15 2 14 eldifd 
 |-  ( ph -> R e. ( Ring \ NzRing ) )
16 1 6 0ringbas 
 |-  ( R e. ( Ring \ NzRing ) -> B = { ( 0g ` R ) } )
17 15 16 syl 
 |-  ( ph -> B = { ( 0g ` R ) } )
18 17 adantr 
 |-  ( ( ph /\ ( a e. B /\ a =/= ( 0g ` R ) ) ) -> B = { ( 0g ` R ) } )
19 9 18 eleqtrd 
 |-  ( ( ph /\ ( a e. B /\ a =/= ( 0g ` R ) ) ) -> a e. { ( 0g ` R ) } )
20 elsni 
 |-  ( a e. { ( 0g ` R ) } -> a = ( 0g ` R ) )
21 19 20 syl 
 |-  ( ( ph /\ ( a e. B /\ a =/= ( 0g ` R ) ) ) -> a = ( 0g ` R ) )
22 simprr 
 |-  ( ( ph /\ ( a e. B /\ a =/= ( 0g ` R ) ) ) -> a =/= ( 0g ` R ) )
23 21 22 pm2.21ddne 
 |-  ( ( ph /\ ( a e. B /\ a =/= ( 0g ` R ) ) ) -> ( a ( .r ` R ) b ) =/= ( 0g ` R ) )
24 23 3adant3 
 |-  ( ( ph /\ ( a e. B /\ a =/= ( 0g ` R ) ) /\ ( b e. B /\ b =/= ( 0g ` R ) ) ) -> ( a ( .r ` R ) b ) =/= ( 0g ` R ) )
25 5 1 6 7 8 2 24 abvtrivd 
 |-  ( ph -> ( x e. B |-> if ( x = ( 0g ` R ) , 0 , 1 ) ) e. ( AbsVal ` R ) )
26 25 ne0d 
 |-  ( ph -> ( AbsVal ` R ) =/= (/) )
27 ral0 
 |-  A. i e. (/) ( i i^i ( RPrime ` R ) ) =/= (/)
28 prmidlssidl 
 |-  ( R e. Ring -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) )
29 2 28 syl 
 |-  ( ph -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) )
30 1 6 0ringidl 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( LIdeal ` R ) = { { ( 0g ` R ) } } )
31 2 3 30 syl2anc 
 |-  ( ph -> ( LIdeal ` R ) = { { ( 0g ` R ) } } )
32 29 31 sseqtrd 
 |-  ( ph -> ( PrmIdeal ` R ) C_ { { ( 0g ` R ) } } )
33 ssdif0 
 |-  ( ( PrmIdeal ` R ) C_ { { ( 0g ` R ) } } <-> ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) = (/) )
34 32 33 sylib 
 |-  ( ph -> ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) = (/) )
35 34 raleqdv 
 |-  ( ph -> ( A. i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ( i i^i ( RPrime ` R ) ) =/= (/) <-> A. i e. (/) ( i i^i ( RPrime ` R ) ) =/= (/) ) )
36 27 35 mpbiri 
 |-  ( ph -> A. i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ( i i^i ( RPrime ` R ) ) =/= (/) )
37 26 36 jca 
 |-  ( ph -> ( ( AbsVal ` R ) =/= (/) /\ A. i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ( i i^i ( RPrime ` R ) ) =/= (/) ) )
38 eqid 
 |-  ( PrmIdeal ` R ) = ( PrmIdeal ` R )
39 eqid 
 |-  ( RPrime ` R ) = ( RPrime ` R )
40 5 38 39 6 isufd 
 |-  ( R e. UFD <-> ( R e. CRing /\ ( ( AbsVal ` R ) =/= (/) /\ A. i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ( i i^i ( RPrime ` R ) ) =/= (/) ) ) )
41 4 37 40 sylanbrc 
 |-  ( ph -> R e. UFD )