Metamath Proof Explorer

Theorem 1arithufdlem1

Description: Lemma for 1arithufd . The set S of elements which can be written as a product of primes is not empty. (Contributed by Thierry Arnoux, 3-Jun-2025)

Ref Expression
Hypotheses 1arithufd.b 
|- B = ( Base ` R )
1arithufd.0 
|- .0. = ( 0g ` R )
1arithufd.u 
|- U = ( Unit ` R )
1arithufd.p 
|- P = ( RPrime ` R )
1arithufd.m 
|- M = ( mulGrp ` R )
1arithufd.r 
|- ( ph -> R e. UFD )
1arithufdlem.2 
|- ( ph -> -. R e. DivRing )
1arithufdlem.s 
|- S = { x e. B | E. f e. Word P x = ( M gsum f ) }
Assertion 1arithufdlem1 
|- ( ph -> S =/= (/) )

Proof

Step Hyp Ref Expression
1 1arithufd.b 
 |-  B = ( Base ` R )
2 1arithufd.0 
 |-  .0. = ( 0g ` R )
3 1arithufd.u 
 |-  U = ( Unit ` R )
4 1arithufd.p 
 |-  P = ( RPrime ` R )
5 1arithufd.m 
 |-  M = ( mulGrp ` R )
6 1arithufd.r 
 |-  ( ph -> R e. UFD )
7 1arithufdlem.2 
 |-  ( ph -> -. R e. DivRing )
8 1arithufdlem.s 
 |-  S = { x e. B | E. f e. Word P x = ( M gsum f ) }
9 eqeq1 
 |-  ( x = p -> ( x = ( M gsum f ) <-> p = ( M gsum f ) ) )
10 9 rexbidv 
 |-  ( x = p -> ( E. f e. Word P x = ( M gsum f ) <-> E. f e. Word P p = ( M gsum f ) ) )
11 6 ad2antrr 
 |-  ( ( ( ph /\ m e. ( MaxIdeal ` R ) ) /\ m =/= { .0. } ) -> R e. UFD )
12 11 ad2antrr 
 |-  ( ( ( ( ( ph /\ m e. ( MaxIdeal ` R ) ) /\ m =/= { .0. } ) /\ p e. P ) /\ p e. m ) -> R e. UFD )
13 simplr 
 |-  ( ( ( ( ( ph /\ m e. ( MaxIdeal ` R ) ) /\ m =/= { .0. } ) /\ p e. P ) /\ p e. m ) -> p e. P )
14 1 4 12 13 rprmcl 
 |-  ( ( ( ( ( ph /\ m e. ( MaxIdeal ` R ) ) /\ m =/= { .0. } ) /\ p e. P ) /\ p e. m ) -> p e. B )
15 oveq2 
 |-  ( f = <" p "> -> ( M gsum f ) = ( M gsum <" p "> ) )
16 15 eqeq2d 
 |-  ( f = <" p "> -> ( p = ( M gsum f ) <-> p = ( M gsum <" p "> ) ) )
17 13 s1cld 
 |-  ( ( ( ( ( ph /\ m e. ( MaxIdeal ` R ) ) /\ m =/= { .0. } ) /\ p e. P ) /\ p e. m ) -> <" p "> e. Word P )
18 5 1 mgpbas 
 |-  B = ( Base ` M )
19 18 gsumws1 
 |-  ( p e. B -> ( M gsum <" p "> ) = p )
20 14 19 syl 
 |-  ( ( ( ( ( ph /\ m e. ( MaxIdeal ` R ) ) /\ m =/= { .0. } ) /\ p e. P ) /\ p e. m ) -> ( M gsum <" p "> ) = p )
21 20 eqcomd 
 |-  ( ( ( ( ( ph /\ m e. ( MaxIdeal ` R ) ) /\ m =/= { .0. } ) /\ p e. P ) /\ p e. m ) -> p = ( M gsum <" p "> ) )
22 16 17 21 rspcedvdw 
 |-  ( ( ( ( ( ph /\ m e. ( MaxIdeal ` R ) ) /\ m =/= { .0. } ) /\ p e. P ) /\ p e. m ) -> E. f e. Word P p = ( M gsum f ) )
23 10 14 22 elrabd 
 |-  ( ( ( ( ( ph /\ m e. ( MaxIdeal ` R ) ) /\ m =/= { .0. } ) /\ p e. P ) /\ p e. m ) -> p e. { x e. B | E. f e. Word P x = ( M gsum f ) } )
24 23 8 eleqtrrdi 
 |-  ( ( ( ( ( ph /\ m e. ( MaxIdeal ` R ) ) /\ m =/= { .0. } ) /\ p e. P ) /\ p e. m ) -> p e. S )
25 24 ne0d 
 |-  ( ( ( ( ( ph /\ m e. ( MaxIdeal ` R ) ) /\ m =/= { .0. } ) /\ p e. P ) /\ p e. m ) -> S =/= (/) )
26 eqid 
 |-  ( PrmIdeal ` R ) = ( PrmIdeal ` R )
27 6 ufdidom 
 |-  ( ph -> R e. IDomn )
28 27 idomcringd 
 |-  ( ph -> R e. CRing )
29 28 ad2antrr 
 |-  ( ( ( ph /\ m e. ( MaxIdeal ` R ) ) /\ m =/= { .0. } ) -> R e. CRing )
30 simplr 
 |-  ( ( ( ph /\ m e. ( MaxIdeal ` R ) ) /\ m =/= { .0. } ) -> m e. ( MaxIdeal ` R ) )
31 eqid 
 |-  ( LSSum ` ( mulGrp ` R ) ) = ( LSSum ` ( mulGrp ` R ) )
32 31 mxidlprm 
 |-  ( ( R e. CRing /\ m e. ( MaxIdeal ` R ) ) -> m e. ( PrmIdeal ` R ) )
33 29 30 32 syl2anc 
 |-  ( ( ( ph /\ m e. ( MaxIdeal ` R ) ) /\ m =/= { .0. } ) -> m e. ( PrmIdeal ` R ) )
34 simpr 
 |-  ( ( ( ph /\ m e. ( MaxIdeal ` R ) ) /\ m =/= { .0. } ) -> m =/= { .0. } )
35 26 4 2 11 33 34 ufdprmidl 
 |-  ( ( ( ph /\ m e. ( MaxIdeal ` R ) ) /\ m =/= { .0. } ) -> E. p e. P p e. m )
36 25 35 r19.29a 
 |-  ( ( ( ph /\ m e. ( MaxIdeal ` R ) ) /\ m =/= { .0. } ) -> S =/= (/) )
37 27 idomdomd 
 |-  ( ph -> R e. Domn )
38 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
39 37 38 syl 
 |-  ( ph -> R e. NzRing )
40 2 39 7 krullndrng 
 |-  ( ph -> E. m e. ( MaxIdeal ` R ) m =/= { .0. } )
41 36 40 r19.29a 
 |-  ( ph -> S =/= (/) )