Metamath Proof Explorer

Theorem dfufd2lem

Description: Lemma for dfufd2 . (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 )
dfufd2lem.1 
|- ( ph -> R e. IDomn )
dfufd2lem.2 
|- ( ph -> I e. ( PrmIdeal ` R ) )
dfufd2lem.3 
|- ( ph -> F e. Word P )
dfufd2lem.4 
|- ( ph -> ( M gsum F ) e. I )
dfufd2lem.5 
|- ( ph -> ( M gsum F ) =/= .0. )
Assertion dfufd2lem 
|- ( ph -> ( I i^i P ) =/= (/) )

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 dfufd2lem.1 
 |-  ( ph -> R e. IDomn )
7 dfufd2lem.2 
 |-  ( ph -> I e. ( PrmIdeal ` R ) )
8 dfufd2lem.3 
 |-  ( ph -> F e. Word P )
9 dfufd2lem.4 
 |-  ( ph -> ( M gsum F ) e. I )
10 dfufd2lem.5 
 |-  ( ph -> ( M gsum F ) =/= .0. )
11 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) /\ ( F ` i ) e. I ) -> ( F ` i ) e. I )
12 eqidd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) /\ ( F ` i ) e. I ) -> ( # ` F ) = ( # ` F ) )
13 8 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) /\ ( F ` i ) e. I ) -> F e. Word P )
14 12 13 wrdfd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) /\ ( F ` i ) e. I ) -> F : ( 0 ..^ ( # ` F ) ) --> P )
15 simplr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) /\ ( F ` i ) e. I ) -> i e. ( 0 ..^ ( # ` F ) ) )
16 14 15 ffvelcdmd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) /\ ( F ` i ) e. I ) -> ( F ` i ) e. P )
17 inelcm 
 |-  ( ( ( F ` i ) e. I /\ ( F ` i ) e. P ) -> ( I i^i P ) =/= (/) )
18 11 16 17 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) /\ ( F ` i ) e. I ) -> ( I i^i P ) =/= (/) )
19 id 
 |-  ( ph -> ph )
20 oveq2 
 |-  ( g = (/) -> ( M gsum g ) = ( M gsum (/) ) )
21 20 eleq1d 
 |-  ( g = (/) -> ( ( M gsum g ) e. I <-> ( M gsum (/) ) e. I ) )
22 20 neeq1d 
 |-  ( g = (/) -> ( ( M gsum g ) =/= .0. <-> ( M gsum (/) ) =/= .0. ) )
23 21 22 3anbi23d 
 |-  ( g = (/) -> ( ( ph /\ ( M gsum g ) e. I /\ ( M gsum g ) =/= .0. ) <-> ( ph /\ ( M gsum (/) ) e. I /\ ( M gsum (/) ) =/= .0. ) ) )
24 fveq2 
 |-  ( g = (/) -> ( # ` g ) = ( # ` (/) ) )
25 24 oveq2d 
 |-  ( g = (/) -> ( 0 ..^ ( # ` g ) ) = ( 0 ..^ ( # ` (/) ) ) )
26 fveq1 
 |-  ( g = (/) -> ( g ` i ) = ( (/) ` i ) )
27 26 eleq1d 
 |-  ( g = (/) -> ( ( g ` i ) e. I <-> ( (/) ` i ) e. I ) )
28 25 27 rexeqbidv 
 |-  ( g = (/) -> ( E. i e. ( 0 ..^ ( # ` g ) ) ( g ` i ) e. I <-> E. i e. ( 0 ..^ ( # ` (/) ) ) ( (/) ` i ) e. I ) )
29 23 28 imbi12d 
 |-  ( g = (/) -> ( ( ( ph /\ ( M gsum g ) e. I /\ ( M gsum g ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` g ) ) ( g ` i ) e. I ) <-> ( ( ph /\ ( M gsum (/) ) e. I /\ ( M gsum (/) ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` (/) ) ) ( (/) ` i ) e. I ) ) )
30 oveq2 
 |-  ( g = f -> ( M gsum g ) = ( M gsum f ) )
31 30 eleq1d 
 |-  ( g = f -> ( ( M gsum g ) e. I <-> ( M gsum f ) e. I ) )
32 30 neeq1d 
 |-  ( g = f -> ( ( M gsum g ) =/= .0. <-> ( M gsum f ) =/= .0. ) )
33 31 32 3anbi23d 
 |-  ( g = f -> ( ( ph /\ ( M gsum g ) e. I /\ ( M gsum g ) =/= .0. ) <-> ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) ) )
34 fveq2 
 |-  ( g = f -> ( # ` g ) = ( # ` f ) )
35 34 oveq2d 
 |-  ( g = f -> ( 0 ..^ ( # ` g ) ) = ( 0 ..^ ( # ` f ) ) )
36 fveq1 
 |-  ( g = f -> ( g ` i ) = ( f ` i ) )
37 36 eleq1d 
 |-  ( g = f -> ( ( g ` i ) e. I <-> ( f ` i ) e. I ) )
38 35 37 rexeqbidv 
 |-  ( g = f -> ( E. i e. ( 0 ..^ ( # ` g ) ) ( g ` i ) e. I <-> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) )
39 33 38 imbi12d 
 |-  ( g = f -> ( ( ( ph /\ ( M gsum g ) e. I /\ ( M gsum g ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` g ) ) ( g ` i ) e. I ) <-> ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) )
40 oveq2 
 |-  ( g = ( f ++ <" p "> ) -> ( M gsum g ) = ( M gsum ( f ++ <" p "> ) ) )
41 40 eleq1d 
 |-  ( g = ( f ++ <" p "> ) -> ( ( M gsum g ) e. I <-> ( M gsum ( f ++ <" p "> ) ) e. I ) )
42 40 neeq1d 
 |-  ( g = ( f ++ <" p "> ) -> ( ( M gsum g ) =/= .0. <-> ( M gsum ( f ++ <" p "> ) ) =/= .0. ) )
43 41 42 3anbi23d 
 |-  ( g = ( f ++ <" p "> ) -> ( ( ph /\ ( M gsum g ) e. I /\ ( M gsum g ) =/= .0. ) <-> ( ph /\ ( M gsum ( f ++ <" p "> ) ) e. I /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) ) )
44 fveq2 
 |-  ( g = ( f ++ <" p "> ) -> ( # ` g ) = ( # ` ( f ++ <" p "> ) ) )
45 44 oveq2d 
 |-  ( g = ( f ++ <" p "> ) -> ( 0 ..^ ( # ` g ) ) = ( 0 ..^ ( # ` ( f ++ <" p "> ) ) ) )
46 fveq1 
 |-  ( g = ( f ++ <" p "> ) -> ( g ` i ) = ( ( f ++ <" p "> ) ` i ) )
47 46 eleq1d 
 |-  ( g = ( f ++ <" p "> ) -> ( ( g ` i ) e. I <-> ( ( f ++ <" p "> ) ` i ) e. I ) )
48 45 47 rexeqbidv 
 |-  ( g = ( f ++ <" p "> ) -> ( E. i e. ( 0 ..^ ( # ` g ) ) ( g ` i ) e. I <-> E. i e. ( 0 ..^ ( # ` ( f ++ <" p "> ) ) ) ( ( f ++ <" p "> ) ` i ) e. I ) )
49 43 48 imbi12d 
 |-  ( g = ( f ++ <" p "> ) -> ( ( ( ph /\ ( M gsum g ) e. I /\ ( M gsum g ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` g ) ) ( g ` i ) e. I ) <-> ( ( ph /\ ( M gsum ( f ++ <" p "> ) ) e. I /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` ( f ++ <" p "> ) ) ) ( ( f ++ <" p "> ) ` i ) e. I ) ) )
50 oveq2 
 |-  ( g = F -> ( M gsum g ) = ( M gsum F ) )
51 50 eleq1d 
 |-  ( g = F -> ( ( M gsum g ) e. I <-> ( M gsum F ) e. I ) )
52 50 neeq1d 
 |-  ( g = F -> ( ( M gsum g ) =/= .0. <-> ( M gsum F ) =/= .0. ) )
53 51 52 3anbi23d 
 |-  ( g = F -> ( ( ph /\ ( M gsum g ) e. I /\ ( M gsum g ) =/= .0. ) <-> ( ph /\ ( M gsum F ) e. I /\ ( M gsum F ) =/= .0. ) ) )
54 fveq2 
 |-  ( g = F -> ( # ` g ) = ( # ` F ) )
55 54 oveq2d 
 |-  ( g = F -> ( 0 ..^ ( # ` g ) ) = ( 0 ..^ ( # ` F ) ) )
56 fveq1 
 |-  ( g = F -> ( g ` i ) = ( F ` i ) )
57 56 eleq1d 
 |-  ( g = F -> ( ( g ` i ) e. I <-> ( F ` i ) e. I ) )
58 55 57 rexeqbidv 
 |-  ( g = F -> ( E. i e. ( 0 ..^ ( # ` g ) ) ( g ` i ) e. I <-> E. i e. ( 0 ..^ ( # ` F ) ) ( F ` i ) e. I ) )
59 53 58 imbi12d 
 |-  ( g = F -> ( ( ( ph /\ ( M gsum g ) e. I /\ ( M gsum g ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` g ) ) ( g ` i ) e. I ) <-> ( ( ph /\ ( M gsum F ) e. I /\ ( M gsum F ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` F ) ) ( F ` i ) e. I ) ) )
60 6 idomringd 
 |-  ( ph -> R e. Ring )
61 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
62 3 61 1unit 
 |-  ( R e. Ring -> ( 1r ` R ) e. U )
63 60 62 syl 
 |-  ( ph -> ( 1r ` R ) e. U )
64 63 ad2antrr 
 |-  ( ( ( ph /\ ( M gsum (/) ) e. I ) /\ ( M gsum (/) ) =/= .0. ) -> ( 1r ` R ) e. U )
65 5 61 ringidval 
 |-  ( 1r ` R ) = ( 0g ` M )
66 65 gsum0 
 |-  ( M gsum (/) ) = ( 1r ` R )
67 simplr 
 |-  ( ( ( ph /\ ( M gsum (/) ) e. I ) /\ ( M gsum (/) ) =/= .0. ) -> ( M gsum (/) ) e. I )
68 66 67 eqeltrrid 
 |-  ( ( ( ph /\ ( M gsum (/) ) e. I ) /\ ( M gsum (/) ) =/= .0. ) -> ( 1r ` R ) e. I )
69 60 ad2antrr 
 |-  ( ( ( ph /\ ( M gsum (/) ) e. I ) /\ ( M gsum (/) ) =/= .0. ) -> R e. Ring )
70 7 ad2antrr 
 |-  ( ( ( ph /\ ( M gsum (/) ) e. I ) /\ ( M gsum (/) ) =/= .0. ) -> I e. ( PrmIdeal ` R ) )
71 prmidlidl 
 |-  ( ( R e. Ring /\ I e. ( PrmIdeal ` R ) ) -> I e. ( LIdeal ` R ) )
72 69 70 71 syl2anc 
 |-  ( ( ( ph /\ ( M gsum (/) ) e. I ) /\ ( M gsum (/) ) =/= .0. ) -> I e. ( LIdeal ` R ) )
73 1 3 64 68 69 72 lidlunitel 
 |-  ( ( ( ph /\ ( M gsum (/) ) e. I ) /\ ( M gsum (/) ) =/= .0. ) -> I = B )
74 eqid 
 |-  ( .r ` R ) = ( .r ` R )
75 1 74 prmidlnr 
 |-  ( ( R e. Ring /\ I e. ( PrmIdeal ` R ) ) -> I =/= B )
76 69 70 75 syl2anc 
 |-  ( ( ( ph /\ ( M gsum (/) ) e. I ) /\ ( M gsum (/) ) =/= .0. ) -> I =/= B )
77 73 76 pm2.21ddne 
 |-  ( ( ( ph /\ ( M gsum (/) ) e. I ) /\ ( M gsum (/) ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` (/) ) ) ( (/) ` i ) e. I )
78 77 3impa 
 |-  ( ( ph /\ ( M gsum (/) ) e. I /\ ( M gsum (/) ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` (/) ) ) ( (/) ` i ) e. I )
79 simpllr 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( M gsum f ) e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ph )
80 simp-4r 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( M gsum f ) e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ( M gsum f ) e. I )
81 6 idomdomd 
 |-  ( ph -> R e. Domn )
82 81 ad3antlr 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( M gsum f ) e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> R e. Domn )
83 6 adantr 
 |-  ( ( ph /\ p e. P ) -> R e. IDomn )
84 simpr 
 |-  ( ( ph /\ p e. P ) -> p e. P )
85 1 4 83 84 rprmcl 
 |-  ( ( ph /\ p e. P ) -> p e. B )
86 4 2 83 84 rprmnz 
 |-  ( ( ph /\ p e. P ) -> p =/= .0. )
87 85 86 eldifsnd 
 |-  ( ( ph /\ p e. P ) -> p e. ( B \ { .0. } ) )
88 87 ex 
 |-  ( ph -> ( p e. P -> p e. ( B \ { .0. } ) ) )
89 88 ssrdv 
 |-  ( ph -> P C_ ( B \ { .0. } ) )
90 sswrd 
 |-  ( P C_ ( B \ { .0. } ) -> Word P C_ Word ( B \ { .0. } ) )
91 89 90 syl 
 |-  ( ph -> Word P C_ Word ( B \ { .0. } ) )
92 91 ad3antlr 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( M gsum f ) e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> Word P C_ Word ( B \ { .0. } ) )
93 simpll 
 |-  ( ( ( f e. Word P /\ p e. P ) /\ ph ) -> f e. Word P )
94 93 ad5ant13 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( M gsum f ) e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> f e. Word P )
95 92 94 sseldd 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( M gsum f ) e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> f e. Word ( B \ { .0. } ) )
96 1 5 2 82 95 domnprodn0 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( M gsum f ) e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ( M gsum f ) =/= .0. )
97 79 80 96 3jca 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( M gsum f ) e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) )
98 lencl 
 |-  ( f e. Word P -> ( # ` f ) e. NN0 )
99 fzossfzop1 
 |-  ( ( # ` f ) e. NN0 -> ( 0 ..^ ( # ` f ) ) C_ ( 0 ..^ ( ( # ` f ) + 1 ) ) )
100 94 98 99 3syl 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( M gsum f ) e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ( 0 ..^ ( # ` f ) ) C_ ( 0 ..^ ( ( # ` f ) + 1 ) ) )
101 ccatws1len 
 |-  ( f e. Word P -> ( # ` ( f ++ <" p "> ) ) = ( ( # ` f ) + 1 ) )
102 94 101 syl 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( M gsum f ) e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ( # ` ( f ++ <" p "> ) ) = ( ( # ` f ) + 1 ) )
103 102 oveq2d 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( M gsum f ) e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ( 0 ..^ ( # ` ( f ++ <" p "> ) ) ) = ( 0 ..^ ( ( # ` f ) + 1 ) ) )
104 100 103 sseqtrrd 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( M gsum f ) e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ( 0 ..^ ( # ` f ) ) C_ ( 0 ..^ ( # ` ( f ++ <" p "> ) ) ) )
105 94 ad2antrr 
 |-  ( ( ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( M gsum f ) e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) /\ i e. ( 0 ..^ ( # ` f ) ) ) /\ ( f ` i ) e. I ) -> f e. Word P )
106 simplr 
 |-  ( ( ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( M gsum f ) e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) /\ i e. ( 0 ..^ ( # ` f ) ) ) /\ ( f ` i ) e. I ) -> i e. ( 0 ..^ ( # ` f ) ) )
107 ccats1val1 
 |-  ( ( f e. Word P /\ i e. ( 0 ..^ ( # ` f ) ) ) -> ( ( f ++ <" p "> ) ` i ) = ( f ` i ) )
108 105 106 107 syl2anc 
 |-  ( ( ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( M gsum f ) e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) /\ i e. ( 0 ..^ ( # ` f ) ) ) /\ ( f ` i ) e. I ) -> ( ( f ++ <" p "> ) ` i ) = ( f ` i ) )
109 simpr 
 |-  ( ( ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( M gsum f ) e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) /\ i e. ( 0 ..^ ( # ` f ) ) ) /\ ( f ` i ) e. I ) -> ( f ` i ) e. I )
110 108 109 eqeltrd 
 |-  ( ( ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( M gsum f ) e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) /\ i e. ( 0 ..^ ( # ` f ) ) ) /\ ( f ` i ) e. I ) -> ( ( f ++ <" p "> ) ` i ) e. I )
111 110 ex 
 |-  ( ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( M gsum f ) e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) /\ i e. ( 0 ..^ ( # ` f ) ) ) -> ( ( f ` i ) e. I -> ( ( f ++ <" p "> ) ` i ) e. I ) )
112 111 reximdva 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( M gsum f ) e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ( E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I -> E. i e. ( 0 ..^ ( # ` f ) ) ( ( f ++ <" p "> ) ` i ) e. I ) )
113 ssrexv 
 |-  ( ( 0 ..^ ( # ` f ) ) C_ ( 0 ..^ ( # ` ( f ++ <" p "> ) ) ) -> ( E. i e. ( 0 ..^ ( # ` f ) ) ( ( f ++ <" p "> ) ` i ) e. I -> E. i e. ( 0 ..^ ( # ` ( f ++ <" p "> ) ) ) ( ( f ++ <" p "> ) ` i ) e. I ) )
114 104 112 113 sylsyld 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( M gsum f ) e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ( E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I -> E. i e. ( 0 ..^ ( # ` ( f ++ <" p "> ) ) ) ( ( f ++ <" p "> ) ` i ) e. I ) )
115 97 114 embantd 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( M gsum f ) e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ( ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) -> E. i e. ( 0 ..^ ( # ` ( f ++ <" p "> ) ) ) ( ( f ++ <" p "> ) ` i ) e. I ) )
116 115 imp 
 |-  ( ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( M gsum f ) e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) -> E. i e. ( 0 ..^ ( # ` ( f ++ <" p "> ) ) ) ( ( f ++ <" p "> ) ` i ) e. I )
117 116 an62ds 
 |-  ( ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) /\ ( M gsum f ) e. I ) -> E. i e. ( 0 ..^ ( # ` ( f ++ <" p "> ) ) ) ( ( f ++ <" p "> ) ` i ) e. I )
118 fveq2 
 |-  ( i = ( # ` f ) -> ( ( f ++ <" p "> ) ` i ) = ( ( f ++ <" p "> ) ` ( # ` f ) ) )
119 118 eleq1d 
 |-  ( i = ( # ` f ) -> ( ( ( f ++ <" p "> ) ` i ) e. I <-> ( ( f ++ <" p "> ) ` ( # ` f ) ) e. I ) )
120 98 ad5antr 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ p e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ( # ` f ) e. NN0 )
121 fzonn0p1 
 |-  ( ( # ` f ) e. NN0 -> ( # ` f ) e. ( 0 ..^ ( ( # ` f ) + 1 ) ) )
122 120 121 syl 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ p e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ( # ` f ) e. ( 0 ..^ ( ( # ` f ) + 1 ) ) )
123 101 ad5antr 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ p e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ( # ` ( f ++ <" p "> ) ) = ( ( # ` f ) + 1 ) )
124 123 oveq2d 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ p e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ( 0 ..^ ( # ` ( f ++ <" p "> ) ) ) = ( 0 ..^ ( ( # ` f ) + 1 ) ) )
125 122 124 eleqtrrd 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ p e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ( # ` f ) e. ( 0 ..^ ( # ` ( f ++ <" p "> ) ) ) )
126 ccatws1ls 
 |-  ( ( f e. Word P /\ p e. P ) -> ( ( f ++ <" p "> ) ` ( # ` f ) ) = p )
127 126 ad4antr 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ p e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ( ( f ++ <" p "> ) ` ( # ` f ) ) = p )
128 simp-4r 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ p e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> p e. I )
129 127 128 eqeltrd 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ p e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ( ( f ++ <" p "> ) ` ( # ` f ) ) e. I )
130 119 125 129 rspcedvdw 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ p e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` ( f ++ <" p "> ) ) ) ( ( f ++ <" p "> ) ` i ) e. I )
131 130 adantr 
 |-  ( ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ p e. I ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) -> E. i e. ( 0 ..^ ( # ` ( f ++ <" p "> ) ) ) ( ( f ++ <" p "> ) ` i ) e. I )
132 131 an62ds 
 |-  ( ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) /\ p e. I ) -> E. i e. ( 0 ..^ ( # ` ( f ++ <" p "> ) ) ) ( ( f ++ <" p "> ) ` i ) e. I )
133 6 idomcringd 
 |-  ( ph -> R e. CRing )
134 133 ad3antlr 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> R e. CRing )
135 7 ad3antlr 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> I e. ( PrmIdeal ` R ) )
136 5 1 mgpbas 
 |-  B = ( Base ` M )
137 5 crngmgp 
 |-  ( R e. CRing -> M e. CMnd )
138 133 137 syl 
 |-  ( ph -> M e. CMnd )
139 138 adantl 
 |-  ( ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) /\ ph ) -> M e. CMnd )
140 ovexd 
 |-  ( ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) /\ ph ) -> ( 0 ..^ ( # ` f ) ) e. _V )
141 eqidd 
 |-  ( ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) /\ ph ) -> ( # ` f ) = ( # ` f ) )
142 simplll 
 |-  ( ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) /\ ph ) -> f e. Word P )
143 141 142 wrdfd 
 |-  ( ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) /\ ph ) -> f : ( 0 ..^ ( # ` f ) ) --> P )
144 85 ex 
 |-  ( ph -> ( p e. P -> p e. B ) )
145 144 ssrdv 
 |-  ( ph -> P C_ B )
146 145 adantl 
 |-  ( ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) /\ ph ) -> P C_ B )
147 143 146 fssd 
 |-  ( ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) /\ ph ) -> f : ( 0 ..^ ( # ` f ) ) --> B )
148 fvexd 
 |-  ( ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) /\ ph ) -> ( 1r ` R ) e. _V )
149 148 142 wrdfsupp 
 |-  ( ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) /\ ph ) -> f finSupp ( 1r ` R ) )
150 136 65 139 140 147 149 gsumcl 
 |-  ( ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) /\ ph ) -> ( M gsum f ) e. B )
151 150 ad2antrr 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ( M gsum f ) e. B )
152 145 adantl 
 |-  ( ( ( f e. Word P /\ p e. P ) /\ ph ) -> P C_ B )
153 simplr 
 |-  ( ( ( f e. Word P /\ p e. P ) /\ ph ) -> p e. P )
154 152 153 sseldd 
 |-  ( ( ( f e. Word P /\ p e. P ) /\ ph ) -> p e. B )
155 154 ad5ant13 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> p e. B )
156 138 cmnmndd 
 |-  ( ph -> M e. Mnd )
157 156 adantl 
 |-  ( ( ( f e. Word P /\ p e. P ) /\ ph ) -> M e. Mnd )
158 sswrd 
 |-  ( P C_ B -> Word P C_ Word B )
159 145 158 syl 
 |-  ( ph -> Word P C_ Word B )
160 159 adantl 
 |-  ( ( ( f e. Word P /\ p e. P ) /\ ph ) -> Word P C_ Word B )
161 160 93 sseldd 
 |-  ( ( ( f e. Word P /\ p e. P ) /\ ph ) -> f e. Word B )
162 5 74 mgpplusg 
 |-  ( .r ` R ) = ( +g ` M )
163 136 162 gsumccatsn 
 |-  ( ( M e. Mnd /\ f e. Word B /\ p e. B ) -> ( M gsum ( f ++ <" p "> ) ) = ( ( M gsum f ) ( .r ` R ) p ) )
164 157 161 154 163 syl3anc 
 |-  ( ( ( f e. Word P /\ p e. P ) /\ ph ) -> ( M gsum ( f ++ <" p "> ) ) = ( ( M gsum f ) ( .r ` R ) p ) )
165 164 ad5ant13 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ( M gsum ( f ++ <" p "> ) ) = ( ( M gsum f ) ( .r ` R ) p ) )
166 simplr 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ( M gsum ( f ++ <" p "> ) ) e. I )
167 165 166 eqeltrrd 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ( ( M gsum f ) ( .r ` R ) p ) e. I )
168 1 74 prmidlc 
 |-  ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ ( ( M gsum f ) e. B /\ p e. B /\ ( ( M gsum f ) ( .r ` R ) p ) e. I ) ) -> ( ( M gsum f ) e. I \/ p e. I ) )
169 134 135 151 155 167 168 syl23anc 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> ( ( M gsum f ) e. I \/ p e. I ) )
170 117 132 169 mpjaodan 
 |-  ( ( ( ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) /\ ph ) /\ ( M gsum ( f ++ <" p "> ) ) e. I ) /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` ( f ++ <" p "> ) ) ) ( ( f ++ <" p "> ) ` i ) e. I )
171 170 exp41 
 |-  ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) -> ( ph -> ( ( M gsum ( f ++ <" p "> ) ) e. I -> ( ( M gsum ( f ++ <" p "> ) ) =/= .0. -> E. i e. ( 0 ..^ ( # ` ( f ++ <" p "> ) ) ) ( ( f ++ <" p "> ) ` i ) e. I ) ) ) )
172 171 3impd 
 |-  ( ( ( f e. Word P /\ p e. P ) /\ ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) ) -> ( ( ph /\ ( M gsum ( f ++ <" p "> ) ) e. I /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` ( f ++ <" p "> ) ) ) ( ( f ++ <" p "> ) ` i ) e. I ) )
173 172 ex 
 |-  ( ( f e. Word P /\ p e. P ) -> ( ( ( ph /\ ( M gsum f ) e. I /\ ( M gsum f ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` f ) ) ( f ` i ) e. I ) -> ( ( ph /\ ( M gsum ( f ++ <" p "> ) ) e. I /\ ( M gsum ( f ++ <" p "> ) ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` ( f ++ <" p "> ) ) ) ( ( f ++ <" p "> ) ` i ) e. I ) ) )
174 29 39 49 59 78 173 wrdind 
 |-  ( F e. Word P -> ( ( ph /\ ( M gsum F ) e. I /\ ( M gsum F ) =/= .0. ) -> E. i e. ( 0 ..^ ( # ` F ) ) ( F ` i ) e. I ) )
175 174 imp 
 |-  ( ( F e. Word P /\ ( ph /\ ( M gsum F ) e. I /\ ( M gsum F ) =/= .0. ) ) -> E. i e. ( 0 ..^ ( # ` F ) ) ( F ` i ) e. I )
176 8 19 9 10 175 syl13anc 
 |-  ( ph -> E. i e. ( 0 ..^ ( # ` F ) ) ( F ` i ) e. I )
177 18 176 r19.29a 
 |-  ( ph -> ( I i^i P ) =/= (/) )