Metamath Proof Explorer

Theorem 1arithufd

Description: Existence of a factorization into irreducible elements in a unique factorization domain. Any non-zero, non-unit element X of a UFD R can be written as a product of primes f . As shown in 1arithidom , that factorization is unique, up to the order of the factors and multiplication by units. (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 )
1arithufd.x 
|- ( ph -> X e. B )
1arithufd.2 
|- ( ph -> -. X e. U )
1arithufd.3 
|- ( ph -> X =/= .0. )
Assertion 1arithufd 
|- ( ph -> E. f e. Word P X = ( M gsum f ) )

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 1arithufd.x 
 |-  ( ph -> X e. B )
8 1arithufd.2 
 |-  ( ph -> -. X e. U )
9 1arithufd.3 
 |-  ( ph -> X =/= .0. )
10 simpr 
 |-  ( ( ph /\ R e. DivRing ) -> R e. DivRing )
11 7 adantr 
 |-  ( ( ph /\ R e. DivRing ) -> X e. B )
12 9 adantr 
 |-  ( ( ph /\ R e. DivRing ) -> X =/= .0. )
13 1 3 2 drngunit 
 |-  ( R e. DivRing -> ( X e. U <-> ( X e. B /\ X =/= .0. ) ) )
14 13 biimpar 
 |-  ( ( R e. DivRing /\ ( X e. B /\ X =/= .0. ) ) -> X e. U )
15 10 11 12 14 syl12anc 
 |-  ( ( ph /\ R e. DivRing ) -> X e. U )
16 8 adantr 
 |-  ( ( ph /\ R e. DivRing ) -> -. X e. U )
17 15 16 pm2.21dd 
 |-  ( ( ph /\ R e. DivRing ) -> E. f e. Word P X = ( M gsum f ) )
18 6 adantr 
 |-  ( ( ph /\ -. R e. DivRing ) -> R e. UFD )
19 simpr 
 |-  ( ( ph /\ -. R e. DivRing ) -> -. R e. DivRing )
20 eqeq1 
 |-  ( y = x -> ( y = ( M gsum f ) <-> x = ( M gsum f ) ) )
21 20 rexbidv 
 |-  ( y = x -> ( E. f e. Word P y = ( M gsum f ) <-> E. f e. Word P x = ( M gsum f ) ) )
22 21 cbvrabv 
 |-  { y e. B | E. f e. Word P y = ( M gsum f ) } = { x e. B | E. f e. Word P x = ( M gsum f ) }
23 oveq2 
 |-  ( f = g -> ( M gsum f ) = ( M gsum g ) )
24 23 eqeq2d 
 |-  ( f = g -> ( x = ( M gsum f ) <-> x = ( M gsum g ) ) )
25 24 cbvrexvw 
 |-  ( E. f e. Word P x = ( M gsum f ) <-> E. g e. Word P x = ( M gsum g ) )
26 22 25 rabbieq 
 |-  { y e. B | E. f e. Word P y = ( M gsum f ) } = { x e. B | E. g e. Word P x = ( M gsum g ) }
27 7 adantr 
 |-  ( ( ph /\ -. R e. DivRing ) -> X e. B )
28 8 adantr 
 |-  ( ( ph /\ -. R e. DivRing ) -> -. X e. U )
29 9 adantr 
 |-  ( ( ph /\ -. R e. DivRing ) -> X =/= .0. )
30 1 2 3 4 5 18 19 26 27 28 29 1arithufdlem4 
 |-  ( ( ph /\ -. R e. DivRing ) -> X e. { y e. B | E. f e. Word P y = ( M gsum f ) } )
31 eqeq1 
 |-  ( y = X -> ( y = ( M gsum f ) <-> X = ( M gsum f ) ) )
32 31 rexbidv 
 |-  ( y = X -> ( E. f e. Word P y = ( M gsum f ) <-> E. f e. Word P X = ( M gsum f ) ) )
33 32 elrab 
 |-  ( X e. { y e. B | E. f e. Word P y = ( M gsum f ) } <-> ( X e. B /\ E. f e. Word P X = ( M gsum f ) ) )
34 30 33 sylib 
 |-  ( ( ph /\ -. R e. DivRing ) -> ( X e. B /\ E. f e. Word P X = ( M gsum f ) ) )
35 34 simprd 
 |-  ( ( ph /\ -. R e. DivRing ) -> E. f e. Word P X = ( M gsum f ) )
36 17 35 pm2.61dan 
 |-  ( ph -> E. f e. Word P X = ( M gsum f ) )