Metamath Proof Explorer

Theorem 1arithufdlem2

Description: Lemma for 1arithufd . The set S of elements which can be written as a product of primes is multiplicatively closed. (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 ) }
1arithufdlem2.1 
|- .x. = ( .r ` R )
1arithufdlem2.2 
|- ( ph -> X e. S )
1arithufdlem2.3 
|- ( ph -> Y e. S )
Assertion 1arithufdlem2 
|- ( ph -> ( X .x. Y ) e. 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 1arithufdlem2.1 
 |-  .x. = ( .r ` R )
10 1arithufdlem2.2 
 |-  ( ph -> X e. S )
11 1arithufdlem2.3 
 |-  ( ph -> Y e. S )
12 eqeq1 
 |-  ( x = ( X .x. Y ) -> ( x = ( M gsum f ) <-> ( X .x. Y ) = ( M gsum f ) ) )
13 12 rexbidv 
 |-  ( x = ( X .x. Y ) -> ( E. f e. Word P x = ( M gsum f ) <-> E. f e. Word P ( X .x. Y ) = ( M gsum f ) ) )
14 6 ufdidom 
 |-  ( ph -> R e. IDomn )
15 14 idomringd 
 |-  ( ph -> R e. Ring )
16 8 ssrab3 
 |-  S C_ B
17 16 10 sselid 
 |-  ( ph -> X e. B )
18 16 11 sselid 
 |-  ( ph -> Y e. B )
19 1 9 15 17 18 ringcld 
 |-  ( ph -> ( X .x. Y ) e. B )
20 oveq2 
 |-  ( f = ( g ++ h ) -> ( M gsum f ) = ( M gsum ( g ++ h ) ) )
21 20 eqeq2d 
 |-  ( f = ( g ++ h ) -> ( ( X .x. Y ) = ( M gsum f ) <-> ( X .x. Y ) = ( M gsum ( g ++ h ) ) ) )
22 ccatcl 
 |-  ( ( g e. Word P /\ h e. Word P ) -> ( g ++ h ) e. Word P )
23 22 ad5ant24 
 |-  ( ( ( ( ( ph /\ g e. Word P ) /\ X = ( M gsum g ) ) /\ h e. Word P ) /\ Y = ( M gsum h ) ) -> ( g ++ h ) e. Word P )
24 simpllr 
 |-  ( ( ( ( ( ph /\ g e. Word P ) /\ X = ( M gsum g ) ) /\ h e. Word P ) /\ Y = ( M gsum h ) ) -> X = ( M gsum g ) )
25 simpr 
 |-  ( ( ( ( ( ph /\ g e. Word P ) /\ X = ( M gsum g ) ) /\ h e. Word P ) /\ Y = ( M gsum h ) ) -> Y = ( M gsum h ) )
26 24 25 oveq12d 
 |-  ( ( ( ( ( ph /\ g e. Word P ) /\ X = ( M gsum g ) ) /\ h e. Word P ) /\ Y = ( M gsum h ) ) -> ( X .x. Y ) = ( ( M gsum g ) .x. ( M gsum h ) ) )
27 5 ringmgp 
 |-  ( R e. Ring -> M e. Mnd )
28 15 27 syl 
 |-  ( ph -> M e. Mnd )
29 28 ad4antr 
 |-  ( ( ( ( ( ph /\ g e. Word P ) /\ X = ( M gsum g ) ) /\ h e. Word P ) /\ Y = ( M gsum h ) ) -> M e. Mnd )
30 6 adantr 
 |-  ( ( ph /\ x e. P ) -> R e. UFD )
31 simpr 
 |-  ( ( ph /\ x e. P ) -> x e. P )
32 1 4 30 31 rprmcl 
 |-  ( ( ph /\ x e. P ) -> x e. B )
33 32 ex 
 |-  ( ph -> ( x e. P -> x e. B ) )
34 33 ssrdv 
 |-  ( ph -> P C_ B )
35 sswrd 
 |-  ( P C_ B -> Word P C_ Word B )
36 34 35 syl 
 |-  ( ph -> Word P C_ Word B )
37 36 ad4antr 
 |-  ( ( ( ( ( ph /\ g e. Word P ) /\ X = ( M gsum g ) ) /\ h e. Word P ) /\ Y = ( M gsum h ) ) -> Word P C_ Word B )
38 simp-4r 
 |-  ( ( ( ( ( ph /\ g e. Word P ) /\ X = ( M gsum g ) ) /\ h e. Word P ) /\ Y = ( M gsum h ) ) -> g e. Word P )
39 37 38 sseldd 
 |-  ( ( ( ( ( ph /\ g e. Word P ) /\ X = ( M gsum g ) ) /\ h e. Word P ) /\ Y = ( M gsum h ) ) -> g e. Word B )
40 simplr 
 |-  ( ( ( ( ( ph /\ g e. Word P ) /\ X = ( M gsum g ) ) /\ h e. Word P ) /\ Y = ( M gsum h ) ) -> h e. Word P )
41 37 40 sseldd 
 |-  ( ( ( ( ( ph /\ g e. Word P ) /\ X = ( M gsum g ) ) /\ h e. Word P ) /\ Y = ( M gsum h ) ) -> h e. Word B )
42 5 1 mgpbas 
 |-  B = ( Base ` M )
43 5 9 mgpplusg 
 |-  .x. = ( +g ` M )
44 42 43 gsumccat 
 |-  ( ( M e. Mnd /\ g e. Word B /\ h e. Word B ) -> ( M gsum ( g ++ h ) ) = ( ( M gsum g ) .x. ( M gsum h ) ) )
45 29 39 41 44 syl3anc 
 |-  ( ( ( ( ( ph /\ g e. Word P ) /\ X = ( M gsum g ) ) /\ h e. Word P ) /\ Y = ( M gsum h ) ) -> ( M gsum ( g ++ h ) ) = ( ( M gsum g ) .x. ( M gsum h ) ) )
46 26 45 eqtr4d 
 |-  ( ( ( ( ( ph /\ g e. Word P ) /\ X = ( M gsum g ) ) /\ h e. Word P ) /\ Y = ( M gsum h ) ) -> ( X .x. Y ) = ( M gsum ( g ++ h ) ) )
47 21 23 46 rspcedvdw 
 |-  ( ( ( ( ( ph /\ g e. Word P ) /\ X = ( M gsum g ) ) /\ h e. Word P ) /\ Y = ( M gsum h ) ) -> E. f e. Word P ( X .x. Y ) = ( M gsum f ) )
48 11 8 eleqtrdi 
 |-  ( ph -> Y e. { x e. B | E. f e. Word P x = ( M gsum f ) } )
49 oveq2 
 |-  ( f = h -> ( M gsum f ) = ( M gsum h ) )
50 49 eqeq2d 
 |-  ( f = h -> ( x = ( M gsum f ) <-> x = ( M gsum h ) ) )
51 50 cbvrexvw 
 |-  ( E. f e. Word P x = ( M gsum f ) <-> E. h e. Word P x = ( M gsum h ) )
52 eqeq1 
 |-  ( x = Y -> ( x = ( M gsum h ) <-> Y = ( M gsum h ) ) )
53 52 rexbidv 
 |-  ( x = Y -> ( E. h e. Word P x = ( M gsum h ) <-> E. h e. Word P Y = ( M gsum h ) ) )
54 51 53 bitrid 
 |-  ( x = Y -> ( E. f e. Word P x = ( M gsum f ) <-> E. h e. Word P Y = ( M gsum h ) ) )
55 54 elrab3 
 |-  ( Y e. B -> ( Y e. { x e. B | E. f e. Word P x = ( M gsum f ) } <-> E. h e. Word P Y = ( M gsum h ) ) )
56 55 biimpa 
 |-  ( ( Y e. B /\ Y e. { x e. B | E. f e. Word P x = ( M gsum f ) } ) -> E. h e. Word P Y = ( M gsum h ) )
57 18 48 56 syl2anc 
 |-  ( ph -> E. h e. Word P Y = ( M gsum h ) )
58 57 ad2antrr 
 |-  ( ( ( ph /\ g e. Word P ) /\ X = ( M gsum g ) ) -> E. h e. Word P Y = ( M gsum h ) )
59 47 58 r19.29a 
 |-  ( ( ( ph /\ g e. Word P ) /\ X = ( M gsum g ) ) -> E. f e. Word P ( X .x. Y ) = ( M gsum f ) )
60 10 8 eleqtrdi 
 |-  ( ph -> X e. { x e. B | E. f e. Word P x = ( M gsum f ) } )
61 oveq2 
 |-  ( f = g -> ( M gsum f ) = ( M gsum g ) )
62 61 eqeq2d 
 |-  ( f = g -> ( x = ( M gsum f ) <-> x = ( M gsum g ) ) )
63 62 cbvrexvw 
 |-  ( E. f e. Word P x = ( M gsum f ) <-> E. g e. Word P x = ( M gsum g ) )
64 eqeq1 
 |-  ( x = X -> ( x = ( M gsum g ) <-> X = ( M gsum g ) ) )
65 64 rexbidv 
 |-  ( x = X -> ( E. g e. Word P x = ( M gsum g ) <-> E. g e. Word P X = ( M gsum g ) ) )
66 63 65 bitrid 
 |-  ( x = X -> ( E. f e. Word P x = ( M gsum f ) <-> E. g e. Word P X = ( M gsum g ) ) )
67 66 elrab3 
 |-  ( X e. B -> ( X e. { x e. B | E. f e. Word P x = ( M gsum f ) } <-> E. g e. Word P X = ( M gsum g ) ) )
68 67 biimpa 
 |-  ( ( X e. B /\ X e. { x e. B | E. f e. Word P x = ( M gsum f ) } ) -> E. g e. Word P X = ( M gsum g ) )
69 17 60 68 syl2anc 
 |-  ( ph -> E. g e. Word P X = ( M gsum g ) )
70 59 69 r19.29a 
 |-  ( ph -> E. f e. Word P ( X .x. Y ) = ( M gsum f ) )
71 13 19 70 elrabd 
 |-  ( ph -> ( X .x. Y ) e. { x e. B | E. f e. Word P x = ( M gsum f ) } )
72 71 8 eleqtrrdi 
 |-  ( ph -> ( X .x. Y ) e. S )