This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ply1gsumz

Description: If a polynomial given as a sum of scaled monomials by factors A is the zero polynomial, then all factors A are zero. (Contributed by Thierry Arnoux, 20-Feb-2025)

Ref Expression
Hypotheses ply1gsumz.p 
|- P = ( Poly1 ` R )
ply1gsumz.b 
|- B = ( Base ` R )
ply1gsumz.n 
|- ( ph -> N e. NN0 )
ply1gsumz.r 
|- ( ph -> R e. Ring )
ply1gsumz.f 
|- F = ( n e. ( 0 ..^ N ) |-> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) )
ply1gsumz.1 
|- .0. = ( 0g ` R )
ply1gsumz.z 
|- Z = ( 0g ` P )
ply1gsumz.a 
|- ( ph -> A : ( 0 ..^ N ) --> B )
ply1gsumz.s 
|- ( ph -> ( P gsum ( A oF ( .s ` P ) F ) ) = Z )
Assertion ply1gsumz 
|- ( ph -> A = ( ( 0 ..^ N ) X. { .0. } ) )

Proof

Step Hyp Ref Expression
1 ply1gsumz.p 
 |-  P = ( Poly1 ` R )
2 ply1gsumz.b 
 |-  B = ( Base ` R )
3 ply1gsumz.n 
 |-  ( ph -> N e. NN0 )
4 ply1gsumz.r 
 |-  ( ph -> R e. Ring )
5 ply1gsumz.f 
 |-  F = ( n e. ( 0 ..^ N ) |-> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) )
6 ply1gsumz.1 
 |-  .0. = ( 0g ` R )
7 ply1gsumz.z 
 |-  Z = ( 0g ` P )
8 ply1gsumz.a 
 |-  ( ph -> A : ( 0 ..^ N ) --> B )
9 ply1gsumz.s 
 |-  ( ph -> ( P gsum ( A oF ( .s ` P ) F ) ) = Z )
10 8 ffnd 
 |-  ( ph -> A Fn ( 0 ..^ N ) )
11 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
12 eqid 
 |-  ( Base ` P ) = ( Base ` P )
13 12 7 ring0cl 
 |-  ( P e. Ring -> Z e. ( Base ` P ) )
14 4 11 13 3syl 
 |-  ( ph -> Z e. ( Base ` P ) )
15 eqid 
 |-  ( coe1 ` Z ) = ( coe1 ` Z )
16 15 12 1 2 coe1f 
 |-  ( Z e. ( Base ` P ) -> ( coe1 ` Z ) : NN0 --> B )
17 14 16 syl 
 |-  ( ph -> ( coe1 ` Z ) : NN0 --> B )
18 17 ffnd 
 |-  ( ph -> ( coe1 ` Z ) Fn NN0 )
19 fzo0ssnn0 
 |-  ( 0 ..^ N ) C_ NN0
20 19 a1i 
 |-  ( ph -> ( 0 ..^ N ) C_ NN0 )
21 18 20 fnssresd 
 |-  ( ph -> ( ( coe1 ` Z ) |` ( 0 ..^ N ) ) Fn ( 0 ..^ N ) )
22 simpr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> j e. ( 0 ..^ N ) )
23 22 fvresd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( coe1 ` Z ) |` ( 0 ..^ N ) ) ` j ) = ( ( coe1 ` Z ) ` j ) )
24 elfzonn0 
 |-  ( j e. ( 0 ..^ N ) -> j e. NN0 )
25 9 14 eqeltrd 
 |-  ( ph -> ( P gsum ( A oF ( .s ` P ) F ) ) e. ( Base ` P ) )
26 eqid 
 |-  ( coe1 ` ( P gsum ( A oF ( .s ` P ) F ) ) ) = ( coe1 ` ( P gsum ( A oF ( .s ` P ) F ) ) )
27 1 12 26 15 ply1coe1eq 
 |-  ( ( R e. Ring /\ ( P gsum ( A oF ( .s ` P ) F ) ) e. ( Base ` P ) /\ Z e. ( Base ` P ) ) -> ( A. j e. NN0 ( ( coe1 ` ( P gsum ( A oF ( .s ` P ) F ) ) ) ` j ) = ( ( coe1 ` Z ) ` j ) <-> ( P gsum ( A oF ( .s ` P ) F ) ) = Z ) )
28 27 biimpar 
 |-  ( ( ( R e. Ring /\ ( P gsum ( A oF ( .s ` P ) F ) ) e. ( Base ` P ) /\ Z e. ( Base ` P ) ) /\ ( P gsum ( A oF ( .s ` P ) F ) ) = Z ) -> A. j e. NN0 ( ( coe1 ` ( P gsum ( A oF ( .s ` P ) F ) ) ) ` j ) = ( ( coe1 ` Z ) ` j ) )
29 4 25 14 9 28 syl31anc 
 |-  ( ph -> A. j e. NN0 ( ( coe1 ` ( P gsum ( A oF ( .s ` P ) F ) ) ) ` j ) = ( ( coe1 ` Z ) ` j ) )
30 29 r19.21bi 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( coe1 ` ( P gsum ( A oF ( .s ` P ) F ) ) ) ` j ) = ( ( coe1 ` Z ) ` j ) )
31 24 30 sylan2 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( coe1 ` ( P gsum ( A oF ( .s ` P ) F ) ) ) ` j ) = ( ( coe1 ` Z ) ` j ) )
32 10 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> A Fn ( 0 ..^ N ) )
33 nfv 
 |-  F/ n ph
34 ovexd 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. _V )
35 33 34 5 fnmptd 
 |-  ( ph -> F Fn ( 0 ..^ N ) )
36 35 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> F Fn ( 0 ..^ N ) )
37 ovexd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( 0 ..^ N ) e. _V )
38 inidm 
 |-  ( ( 0 ..^ N ) i^i ( 0 ..^ N ) ) = ( 0 ..^ N )
39 eqidd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ N ) ) -> ( A ` i ) = ( A ` i ) )
40 oveq1 
 |-  ( n = i -> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) )
41 simpr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ N ) ) -> i e. ( 0 ..^ N ) )
42 ovexd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ N ) ) -> ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. _V )
43 5 40 41 42 fvmptd3 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ N ) ) -> ( F ` i ) = ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) )
44 32 36 37 37 38 39 43 offval 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( A oF ( .s ` P ) F ) = ( i e. ( 0 ..^ N ) |-> ( ( A ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) )
45 44 oveq2d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( P gsum ( A oF ( .s ` P ) F ) ) = ( P gsum ( i e. ( 0 ..^ N ) |-> ( ( A ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) )
46 45 fveq2d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( coe1 ` ( P gsum ( A oF ( .s ` P ) F ) ) ) = ( coe1 ` ( P gsum ( i e. ( 0 ..^ N ) |-> ( ( A ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) )
47 46 fveq1d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( coe1 ` ( P gsum ( A oF ( .s ` P ) F ) ) ) ` j ) = ( ( coe1 ` ( P gsum ( i e. ( 0 ..^ N ) |-> ( ( A ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ` j ) )
48 eqid 
 |-  ( var1 ` R ) = ( var1 ` R )
49 eqid 
 |-  ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
50 4 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> R e. Ring )
51 eqid 
 |-  ( .s ` P ) = ( .s ` P )
52 8 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> A : ( 0 ..^ N ) --> B )
53 52 ffvelcdmda 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ N ) ) -> ( A ` i ) e. B )
54 53 ralrimiva 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> A. i e. ( 0 ..^ N ) ( A ` i ) e. B )
55 3 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> N e. NN0 )
56 fveq2 
 |-  ( i = j -> ( A ` i ) = ( A ` j ) )
57 1 12 48 49 50 2 51 6 54 22 55 56 gsummoncoe1fzo 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( coe1 ` ( P gsum ( i e. ( 0 ..^ N ) |-> ( ( A ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ` j ) = ( A ` j ) )
58 47 57 eqtrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( coe1 ` ( P gsum ( A oF ( .s ` P ) F ) ) ) ` j ) = ( A ` j ) )
59 23 31 58 3eqtr2rd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( A ` j ) = ( ( ( coe1 ` Z ) |` ( 0 ..^ N ) ) ` j ) )
60 10 21 59 eqfnfvd 
 |-  ( ph -> A = ( ( coe1 ` Z ) |` ( 0 ..^ N ) ) )
61 1 7 6 coe1z 
 |-  ( R e. Ring -> ( coe1 ` Z ) = ( NN0 X. { .0. } ) )
62 4 61 syl 
 |-  ( ph -> ( coe1 ` Z ) = ( NN0 X. { .0. } ) )
63 62 reseq1d 
 |-  ( ph -> ( ( coe1 ` Z ) |` ( 0 ..^ N ) ) = ( ( NN0 X. { .0. } ) |` ( 0 ..^ N ) ) )
64 60 63 eqtrd 
 |-  ( ph -> A = ( ( NN0 X. { .0. } ) |` ( 0 ..^ N ) ) )
65 xpssres 
 |-  ( ( 0 ..^ N ) C_ NN0 -> ( ( NN0 X. { .0. } ) |` ( 0 ..^ N ) ) = ( ( 0 ..^ N ) X. { .0. } ) )
66 19 65 ax-mp 
 |-  ( ( NN0 X. { .0. } ) |` ( 0 ..^ N ) ) = ( ( 0 ..^ N ) X. { .0. } )
67 64 66 eqtrdi 
 |-  ( ph -> A = ( ( 0 ..^ N ) X. { .0. } ) )