Metamath Proof Explorer

Theorem gsumply1eq

Description: Two univariate polynomials given as (finitely supported) sum of scaled monomials are equal iff the corresponding coefficients are equal. (Contributed by AV, 21-Nov-2019)

Ref Expression
Hypotheses gsumply1eq.p 
|- P = ( Poly1 ` R )
gsumply1eq.x 
|- X = ( var1 ` R )
gsumply1eq.e 
|- .^ = ( .g ` ( mulGrp ` P ) )
gsumply1eq.r 
|- ( ph -> R e. Ring )
gsumply1eq.k 
|- K = ( Base ` R )
gsumply1eq.m 
|- .* = ( .s ` P )
gsumply1eq.0 
|- .0. = ( 0g ` R )
gsumply1eq.a 
|- ( ph -> A. k e. NN0 A e. K )
gsumply1eq.f1 
|- ( ph -> ( k e. NN0 |-> A ) finSupp .0. )
gsumply1eq.b 
|- ( ph -> A. k e. NN0 B e. K )
gsumply1eq.f2 
|- ( ph -> ( k e. NN0 |-> B ) finSupp .0. )
gsumply1eq.o 
|- ( ph -> O = ( P gsum ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) ) )
gsumply1eq.q 
|- ( ph -> Q = ( P gsum ( k e. NN0 |-> ( B .* ( k .^ X ) ) ) ) )
Assertion gsumply1eq 
|- ( ph -> ( O = Q <-> A. k e. NN0 A = B ) )

Proof

Step Hyp Ref Expression
1 gsumply1eq.p 
 |-  P = ( Poly1 ` R )
2 gsumply1eq.x 
 |-  X = ( var1 ` R )
3 gsumply1eq.e 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
4 gsumply1eq.r 
 |-  ( ph -> R e. Ring )
5 gsumply1eq.k 
 |-  K = ( Base ` R )
6 gsumply1eq.m 
 |-  .* = ( .s ` P )
7 gsumply1eq.0 
 |-  .0. = ( 0g ` R )
8 gsumply1eq.a 
 |-  ( ph -> A. k e. NN0 A e. K )
9 gsumply1eq.f1 
 |-  ( ph -> ( k e. NN0 |-> A ) finSupp .0. )
10 gsumply1eq.b 
 |-  ( ph -> A. k e. NN0 B e. K )
11 gsumply1eq.f2 
 |-  ( ph -> ( k e. NN0 |-> B ) finSupp .0. )
12 gsumply1eq.o 
 |-  ( ph -> O = ( P gsum ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) ) )
13 gsumply1eq.q 
 |-  ( ph -> Q = ( P gsum ( k e. NN0 |-> ( B .* ( k .^ X ) ) ) ) )
14 eqid 
 |-  ( Base ` P ) = ( Base ` P )
15 1 14 2 3 4 5 6 7 8 9 gsumsmonply1 
 |-  ( ph -> ( P gsum ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) ) e. ( Base ` P ) )
16 12 15 eqeltrd 
 |-  ( ph -> O e. ( Base ` P ) )
17 1 14 2 3 4 5 6 7 10 11 gsumsmonply1 
 |-  ( ph -> ( P gsum ( k e. NN0 |-> ( B .* ( k .^ X ) ) ) ) e. ( Base ` P ) )
18 13 17 eqeltrd 
 |-  ( ph -> Q e. ( Base ` P ) )
19 eqid 
 |-  ( coe1 ` O ) = ( coe1 ` O )
20 eqid 
 |-  ( coe1 ` Q ) = ( coe1 ` Q )
21 1 14 19 20 ply1coe1eq 
 |-  ( ( R e. Ring /\ O e. ( Base ` P ) /\ Q e. ( Base ` P ) ) -> ( A. k e. NN0 ( ( coe1 ` O ) ` k ) = ( ( coe1 ` Q ) ` k ) <-> O = Q ) )
22 21 bicomd 
 |-  ( ( R e. Ring /\ O e. ( Base ` P ) /\ Q e. ( Base ` P ) ) -> ( O = Q <-> A. k e. NN0 ( ( coe1 ` O ) ` k ) = ( ( coe1 ` Q ) ` k ) ) )
23 4 16 18 22 syl3anc 
 |-  ( ph -> ( O = Q <-> A. k e. NN0 ( ( coe1 ` O ) ` k ) = ( ( coe1 ` Q ) ` k ) ) )
24 12 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> O = ( P gsum ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) ) )
25 nfcv 
 |-  F/_ l ( A .* ( k .^ X ) )
26 nfcsb1v 
 |-  F/_ k [_ l / k ]_ A
27 nfcv 
 |-  F/_ k .*
28 nfcv 
 |-  F/_ k ( l .^ X )
29 26 27 28 nfov 
 |-  F/_ k ( [_ l / k ]_ A .* ( l .^ X ) )
30 csbeq1a 
 |-  ( k = l -> A = [_ l / k ]_ A )
31 oveq1 
 |-  ( k = l -> ( k .^ X ) = ( l .^ X ) )
32 30 31 oveq12d 
 |-  ( k = l -> ( A .* ( k .^ X ) ) = ( [_ l / k ]_ A .* ( l .^ X ) ) )
33 25 29 32 cbvmpt 
 |-  ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) = ( l e. NN0 |-> ( [_ l / k ]_ A .* ( l .^ X ) ) )
34 33 oveq2i 
 |-  ( P gsum ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) ) = ( P gsum ( l e. NN0 |-> ( [_ l / k ]_ A .* ( l .^ X ) ) ) )
35 24 34 eqtrdi 
 |-  ( ( ph /\ k e. NN0 ) -> O = ( P gsum ( l e. NN0 |-> ( [_ l / k ]_ A .* ( l .^ X ) ) ) ) )
36 35 fveq2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( coe1 ` O ) = ( coe1 ` ( P gsum ( l e. NN0 |-> ( [_ l / k ]_ A .* ( l .^ X ) ) ) ) ) )
37 36 fveq1d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( coe1 ` O ) ` k ) = ( ( coe1 ` ( P gsum ( l e. NN0 |-> ( [_ l / k ]_ A .* ( l .^ X ) ) ) ) ) ` k ) )
38 4 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> R e. Ring )
39 nfv 
 |-  F/ l A e. K
40 26 nfel1 
 |-  F/ k [_ l / k ]_ A e. K
41 30 eleq1d 
 |-  ( k = l -> ( A e. K <-> [_ l / k ]_ A e. K ) )
42 39 40 41 cbvralw 
 |-  ( A. k e. NN0 A e. K <-> A. l e. NN0 [_ l / k ]_ A e. K )
43 8 42 sylib 
 |-  ( ph -> A. l e. NN0 [_ l / k ]_ A e. K )
44 43 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> A. l e. NN0 [_ l / k ]_ A e. K )
45 nfcv 
 |-  F/_ l A
46 45 26 30 cbvmpt 
 |-  ( k e. NN0 |-> A ) = ( l e. NN0 |-> [_ l / k ]_ A )
47 46 9 eqbrtrrid 
 |-  ( ph -> ( l e. NN0 |-> [_ l / k ]_ A ) finSupp .0. )
48 47 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> ( l e. NN0 |-> [_ l / k ]_ A ) finSupp .0. )
49 simpr 
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
50 1 14 2 3 38 5 6 7 44 48 49 gsummoncoe1 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( coe1 ` ( P gsum ( l e. NN0 |-> ( [_ l / k ]_ A .* ( l .^ X ) ) ) ) ) ` k ) = [_ k / l ]_ [_ l / k ]_ A )
51 csbcow 
 |-  [_ k / l ]_ [_ l / k ]_ A = [_ k / k ]_ A
52 csbid 
 |-  [_ k / k ]_ A = A
53 51 52 eqtri 
 |-  [_ k / l ]_ [_ l / k ]_ A = A
54 50 53 eqtrdi 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( coe1 ` ( P gsum ( l e. NN0 |-> ( [_ l / k ]_ A .* ( l .^ X ) ) ) ) ) ` k ) = A )
55 37 54 eqtrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( coe1 ` O ) ` k ) = A )
56 13 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> Q = ( P gsum ( k e. NN0 |-> ( B .* ( k .^ X ) ) ) ) )
57 nfcv 
 |-  F/_ l ( B .* ( k .^ X ) )
58 nfcsb1v 
 |-  F/_ k [_ l / k ]_ B
59 58 27 28 nfov 
 |-  F/_ k ( [_ l / k ]_ B .* ( l .^ X ) )
60 csbeq1a 
 |-  ( k = l -> B = [_ l / k ]_ B )
61 60 31 oveq12d 
 |-  ( k = l -> ( B .* ( k .^ X ) ) = ( [_ l / k ]_ B .* ( l .^ X ) ) )
62 57 59 61 cbvmpt 
 |-  ( k e. NN0 |-> ( B .* ( k .^ X ) ) ) = ( l e. NN0 |-> ( [_ l / k ]_ B .* ( l .^ X ) ) )
63 62 a1i 
 |-  ( ( ph /\ k e. NN0 ) -> ( k e. NN0 |-> ( B .* ( k .^ X ) ) ) = ( l e. NN0 |-> ( [_ l / k ]_ B .* ( l .^ X ) ) ) )
64 63 oveq2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( P gsum ( k e. NN0 |-> ( B .* ( k .^ X ) ) ) ) = ( P gsum ( l e. NN0 |-> ( [_ l / k ]_ B .* ( l .^ X ) ) ) ) )
65 56 64 eqtrd 
 |-  ( ( ph /\ k e. NN0 ) -> Q = ( P gsum ( l e. NN0 |-> ( [_ l / k ]_ B .* ( l .^ X ) ) ) ) )
66 65 fveq2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( coe1 ` Q ) = ( coe1 ` ( P gsum ( l e. NN0 |-> ( [_ l / k ]_ B .* ( l .^ X ) ) ) ) ) )
67 66 fveq1d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( coe1 ` Q ) ` k ) = ( ( coe1 ` ( P gsum ( l e. NN0 |-> ( [_ l / k ]_ B .* ( l .^ X ) ) ) ) ) ` k ) )
68 nfv 
 |-  F/ l B e. K
69 58 nfel1 
 |-  F/ k [_ l / k ]_ B e. K
70 60 eleq1d 
 |-  ( k = l -> ( B e. K <-> [_ l / k ]_ B e. K ) )
71 68 69 70 cbvralw 
 |-  ( A. k e. NN0 B e. K <-> A. l e. NN0 [_ l / k ]_ B e. K )
72 10 71 sylib 
 |-  ( ph -> A. l e. NN0 [_ l / k ]_ B e. K )
73 72 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> A. l e. NN0 [_ l / k ]_ B e. K )
74 nfcv 
 |-  F/_ l B
75 74 58 60 cbvmpt 
 |-  ( k e. NN0 |-> B ) = ( l e. NN0 |-> [_ l / k ]_ B )
76 75 11 eqbrtrrid 
 |-  ( ph -> ( l e. NN0 |-> [_ l / k ]_ B ) finSupp .0. )
77 76 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> ( l e. NN0 |-> [_ l / k ]_ B ) finSupp .0. )
78 1 14 2 3 38 5 6 7 73 77 49 gsummoncoe1 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( coe1 ` ( P gsum ( l e. NN0 |-> ( [_ l / k ]_ B .* ( l .^ X ) ) ) ) ) ` k ) = [_ k / l ]_ [_ l / k ]_ B )
79 csbcow 
 |-  [_ k / l ]_ [_ l / k ]_ B = [_ k / k ]_ B
80 csbid 
 |-  [_ k / k ]_ B = B
81 79 80 eqtri 
 |-  [_ k / l ]_ [_ l / k ]_ B = B
82 78 81 eqtrdi 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( coe1 ` ( P gsum ( l e. NN0 |-> ( [_ l / k ]_ B .* ( l .^ X ) ) ) ) ) ` k ) = B )
83 67 82 eqtrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( coe1 ` Q ) ` k ) = B )
84 55 83 eqeq12d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( coe1 ` O ) ` k ) = ( ( coe1 ` Q ) ` k ) <-> A = B ) )
85 84 ralbidva 
 |-  ( ph -> ( A. k e. NN0 ( ( coe1 ` O ) ` k ) = ( ( coe1 ` Q ) ` k ) <-> A. k e. NN0 A = B ) )
86 23 85 bitrd 
 |-  ( ph -> ( O = Q <-> A. k e. NN0 A = B ) )