Metamath Proof Explorer

Theorem dfufd2

Description: Alternative definition of unique factorization domain (UFD). This is often the textbook definition. Chapter VII, Paragraph 3, Section 3, Proposition 2 of BourbakiCAlg2, p. 228. (Contributed by Thierry Arnoux, 6-Jun-2025)

Ref Expression
Hypotheses dfufd2.b 
|- B = ( Base ` R )
dfufd2.0 
|- .0. = ( 0g ` R )
dfufd2.u 
|- U = ( Unit ` R )
dfufd2.p 
|- P = ( RPrime ` R )
dfufd2.m 
|- M = ( mulGrp ` R )
Assertion dfufd2 
|- ( R e. UFD <-> ( R e. IDomn /\ A. x e. ( ( B \ U ) \ { .0. } ) E. f e. Word P x = ( M gsum f ) ) )

Proof

Step Hyp Ref Expression
1 dfufd2.b 
 |-  B = ( Base ` R )
2 dfufd2.0 
 |-  .0. = ( 0g ` R )
3 dfufd2.u 
 |-  U = ( Unit ` R )
4 dfufd2.p 
 |-  P = ( RPrime ` R )
5 dfufd2.m 
 |-  M = ( mulGrp ` R )
6 id 
 |-  ( R e. UFD -> R e. UFD )
7 6 ufdidom 
 |-  ( R e. UFD -> R e. IDomn )
8 simpl 
 |-  ( ( R e. UFD /\ x e. ( ( B \ U ) \ { .0. } ) ) -> R e. UFD )
9 simpr 
 |-  ( ( R e. UFD /\ x e. ( ( B \ U ) \ { .0. } ) ) -> x e. ( ( B \ U ) \ { .0. } ) )
10 9 eldifad 
 |-  ( ( R e. UFD /\ x e. ( ( B \ U ) \ { .0. } ) ) -> x e. ( B \ U ) )
11 10 eldifad 
 |-  ( ( R e. UFD /\ x e. ( ( B \ U ) \ { .0. } ) ) -> x e. B )
12 10 eldifbd 
 |-  ( ( R e. UFD /\ x e. ( ( B \ U ) \ { .0. } ) ) -> -. x e. U )
13 eldifsni 
 |-  ( x e. ( ( B \ U ) \ { .0. } ) -> x =/= .0. )
14 13 adantl 
 |-  ( ( R e. UFD /\ x e. ( ( B \ U ) \ { .0. } ) ) -> x =/= .0. )
15 1 2 3 4 5 8 11 12 14 1arithufd 
 |-  ( ( R e. UFD /\ x e. ( ( B \ U ) \ { .0. } ) ) -> E. f e. Word P x = ( M gsum f ) )
16 15 ralrimiva 
 |-  ( R e. UFD -> A. x e. ( ( B \ U ) \ { .0. } ) E. f e. Word P x = ( M gsum f ) )
17 7 16 jca 
 |-  ( R e. UFD -> ( R e. IDomn /\ A. x e. ( ( B \ U ) \ { .0. } ) E. f e. Word P x = ( M gsum f ) ) )
18 simpl 
 |-  ( ( R e. IDomn /\ A. x e. ( ( B \ U ) \ { .0. } ) E. f e. Word P x = ( M gsum f ) ) -> R e. IDomn )
19 id 
 |-  ( R e. IDomn -> R e. IDomn )
20 19 idomringd 
 |-  ( R e. IDomn -> R e. Ring )
21 20 ad2antrr 
 |-  ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) -> R e. Ring )
22 simpr 
 |-  ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) -> i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) )
23 22 eldifad 
 |-  ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) -> i e. ( PrmIdeal ` R ) )
24 prmidlidl 
 |-  ( ( R e. Ring /\ i e. ( PrmIdeal ` R ) ) -> i e. ( LIdeal ` R ) )
25 21 23 24 syl2anc 
 |-  ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) -> i e. ( LIdeal ` R ) )
26 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
27 1 26 lidlss 
 |-  ( i e. ( LIdeal ` R ) -> i C_ B )
28 25 27 syl 
 |-  ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) -> i C_ B )
29 28 sselda 
 |-  ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) -> y e. B )
30 simpr 
 |-  ( ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) /\ y e. U ) -> y e. U )
31 simplr 
 |-  ( ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) /\ y e. U ) -> y e. i )
32 21 ad2antrr 
 |-  ( ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) /\ y e. U ) -> R e. Ring )
33 25 ad2antrr 
 |-  ( ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) /\ y e. U ) -> i e. ( LIdeal ` R ) )
34 1 3 30 31 32 33 lidlunitel 
 |-  ( ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) /\ y e. U ) -> i = B )
35 eqid 
 |-  ( .r ` R ) = ( .r ` R )
36 1 35 prmidlnr 
 |-  ( ( R e. Ring /\ i e. ( PrmIdeal ` R ) ) -> i =/= B )
37 21 23 36 syl2anc 
 |-  ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) -> i =/= B )
38 37 ad2antrr 
 |-  ( ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) /\ y e. U ) -> i =/= B )
39 38 neneqd 
 |-  ( ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) /\ y e. U ) -> -. i = B )
40 34 39 pm2.65da 
 |-  ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) -> -. y e. U )
41 29 40 eldifd 
 |-  ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) -> y e. ( B \ U ) )
42 simpllr 
 |-  ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) -> y =/= .0. )
43 41 42 eldifsnd 
 |-  ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) -> y e. ( ( B \ U ) \ { .0. } ) )
44 eqeq1 
 |-  ( x = y -> ( x = ( M gsum f ) <-> y = ( M gsum f ) ) )
45 44 rexbidv 
 |-  ( x = y -> ( E. f e. Word P x = ( M gsum f ) <-> E. f e. Word P y = ( M gsum f ) ) )
46 45 adantl 
 |-  ( ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) /\ x = y ) -> ( E. f e. Word P x = ( M gsum f ) <-> E. f e. Word P y = ( M gsum f ) ) )
47 43 46 rspcdv 
 |-  ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) -> ( A. x e. ( ( B \ U ) \ { .0. } ) E. f e. Word P x = ( M gsum f ) -> E. f e. Word P y = ( M gsum f ) ) )
48 simp-5l 
 |-  ( ( ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) /\ f e. Word P ) /\ y = ( M gsum f ) ) -> R e. IDomn )
49 23 ad3antrrr 
 |-  ( ( ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) /\ f e. Word P ) /\ y = ( M gsum f ) ) -> i e. ( PrmIdeal ` R ) )
50 simplr 
 |-  ( ( ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) /\ f e. Word P ) /\ y = ( M gsum f ) ) -> f e. Word P )
51 simpr 
 |-  ( ( ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) /\ f e. Word P ) /\ y = ( M gsum f ) ) -> y = ( M gsum f ) )
52 simpllr 
 |-  ( ( ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) /\ f e. Word P ) /\ y = ( M gsum f ) ) -> y e. i )
53 51 52 eqeltrrd 
 |-  ( ( ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) /\ f e. Word P ) /\ y = ( M gsum f ) ) -> ( M gsum f ) e. i )
54 42 ad2antrr 
 |-  ( ( ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) /\ f e. Word P ) /\ y = ( M gsum f ) ) -> y =/= .0. )
55 51 54 eqnetrrd 
 |-  ( ( ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) /\ f e. Word P ) /\ y = ( M gsum f ) ) -> ( M gsum f ) =/= .0. )
56 1 2 3 4 5 48 49 50 53 55 dfufd2lem 
 |-  ( ( ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) /\ f e. Word P ) /\ y = ( M gsum f ) ) -> ( i i^i P ) =/= (/) )
57 56 rexlimdva2 
 |-  ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) -> ( E. f e. Word P y = ( M gsum f ) -> ( i i^i P ) =/= (/) ) )
58 47 57 syld 
 |-  ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) -> ( A. x e. ( ( B \ U ) \ { .0. } ) E. f e. Word P x = ( M gsum f ) -> ( i i^i P ) =/= (/) ) )
59 58 imp 
 |-  ( ( ( ( ( R e. IDomn /\ y =/= .0. ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) /\ A. x e. ( ( B \ U ) \ { .0. } ) E. f e. Word P x = ( M gsum f ) ) -> ( i i^i P ) =/= (/) )
60 59 an52ds 
 |-  ( ( ( ( ( R e. IDomn /\ A. x e. ( ( B \ U ) \ { .0. } ) E. f e. Word P x = ( M gsum f ) ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) /\ y e. i ) /\ y =/= .0. ) -> ( i i^i P ) =/= (/) )
61 20 ad2antrr 
 |-  ( ( ( R e. IDomn /\ A. x e. ( ( B \ U ) \ { .0. } ) E. f e. Word P x = ( M gsum f ) ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) -> R e. Ring )
62 simpr 
 |-  ( ( ( R e. IDomn /\ A. x e. ( ( B \ U ) \ { .0. } ) E. f e. Word P x = ( M gsum f ) ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) -> i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) )
63 62 eldifad 
 |-  ( ( ( R e. IDomn /\ A. x e. ( ( B \ U ) \ { .0. } ) E. f e. Word P x = ( M gsum f ) ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) -> i e. ( PrmIdeal ` R ) )
64 61 63 24 syl2anc 
 |-  ( ( ( R e. IDomn /\ A. x e. ( ( B \ U ) \ { .0. } ) E. f e. Word P x = ( M gsum f ) ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) -> i e. ( LIdeal ` R ) )
65 eldifsni 
 |-  ( i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) -> i =/= { .0. } )
66 65 adantl 
 |-  ( ( ( R e. IDomn /\ A. x e. ( ( B \ U ) \ { .0. } ) E. f e. Word P x = ( M gsum f ) ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) -> i =/= { .0. } )
67 26 2 lidlnz 
 |-  ( ( R e. Ring /\ i e. ( LIdeal ` R ) /\ i =/= { .0. } ) -> E. y e. i y =/= .0. )
68 61 64 66 67 syl3anc 
 |-  ( ( ( R e. IDomn /\ A. x e. ( ( B \ U ) \ { .0. } ) E. f e. Word P x = ( M gsum f ) ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) -> E. y e. i y =/= .0. )
69 60 68 r19.29a 
 |-  ( ( ( R e. IDomn /\ A. x e. ( ( B \ U ) \ { .0. } ) E. f e. Word P x = ( M gsum f ) ) /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) -> ( i i^i P ) =/= (/) )
70 69 ralrimiva 
 |-  ( ( R e. IDomn /\ A. x e. ( ( B \ U ) \ { .0. } ) E. f e. Word P x = ( M gsum f ) ) -> A. i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ( i i^i P ) =/= (/) )
71 eqid 
 |-  ( PrmIdeal ` R ) = ( PrmIdeal ` R )
72 71 4 2 isufd 
 |-  ( R e. UFD <-> ( R e. IDomn /\ A. i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ( i i^i P ) =/= (/) ) )
73 18 70 72 sylanbrc 
 |-  ( ( R e. IDomn /\ A. x e. ( ( B \ U ) \ { .0. } ) E. f e. Word P x = ( M gsum f ) ) -> R e. UFD )
74 17 73 impbii 
 |-  ( R e. UFD <-> ( R e. IDomn /\ A. x e. ( ( B \ U ) \ { .0. } ) E. f e. Word P x = ( M gsum f ) ) )