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

Metamath Proof Explorer

Theorem eqcoe1ply1eq

Description: Two polynomials over the same ring are equal if they have identical coefficients. (Contributed by AV, 7-Oct-2019)

Ref Expression
Hypotheses eqcoe1ply1eq.p 
|- P = ( Poly1 ` R )
eqcoe1ply1eq.b 
|- B = ( Base ` P )
eqcoe1ply1eq.a 
|- A = ( coe1 ` K )
eqcoe1ply1eq.c 
|- C = ( coe1 ` L )
Assertion eqcoe1ply1eq 
|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( A. k e. NN0 ( A ` k ) = ( C ` k ) -> K = L ) )

Proof

Step Hyp Ref Expression
1 eqcoe1ply1eq.p 
 |-  P = ( Poly1 ` R )
2 eqcoe1ply1eq.b 
 |-  B = ( Base ` P )
3 eqcoe1ply1eq.a 
 |-  A = ( coe1 ` K )
4 eqcoe1ply1eq.c 
 |-  C = ( coe1 ` L )
5 fveq2 
 |-  ( k = n -> ( A ` k ) = ( A ` n ) )
6 fveq2 
 |-  ( k = n -> ( C ` k ) = ( C ` n ) )
7 5 6 eqeq12d 
 |-  ( k = n -> ( ( A ` k ) = ( C ` k ) <-> ( A ` n ) = ( C ` n ) ) )
8 7 rspccv 
 |-  ( A. k e. NN0 ( A ` k ) = ( C ` k ) -> ( n e. NN0 -> ( A ` n ) = ( C ` n ) ) )
9 8 adantl 
 |-  ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ A. k e. NN0 ( A ` k ) = ( C ` k ) ) -> ( n e. NN0 -> ( A ` n ) = ( C ` n ) ) )
10 9 imp 
 |-  ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ A. k e. NN0 ( A ` k ) = ( C ` k ) ) /\ n e. NN0 ) -> ( A ` n ) = ( C ` n ) )
11 3 fveq1i 
 |-  ( A ` n ) = ( ( coe1 ` K ) ` n )
12 4 fveq1i 
 |-  ( C ` n ) = ( ( coe1 ` L ) ` n )
13 10 11 12 3eqtr3g 
 |-  ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ A. k e. NN0 ( A ` k ) = ( C ` k ) ) /\ n e. NN0 ) -> ( ( coe1 ` K ) ` n ) = ( ( coe1 ` L ) ` n ) )
14 13 oveq1d 
 |-  ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ A. k e. NN0 ( A ` k ) = ( C ` k ) ) /\ n e. NN0 ) -> ( ( ( coe1 ` K ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( ( ( coe1 ` L ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
15 14 mpteq2dva 
 |-  ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ A. k e. NN0 ( A ` k ) = ( C ` k ) ) -> ( n e. NN0 |-> ( ( ( coe1 ` K ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = ( n e. NN0 |-> ( ( ( coe1 ` L ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) )
16 15 oveq2d 
 |-  ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ A. k e. NN0 ( A ` k ) = ( C ` k ) ) -> ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` K ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) = ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` L ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) )
17 eqid 
 |-  ( var1 ` R ) = ( var1 ` R )
18 eqid 
 |-  ( .s ` P ) = ( .s ` P )
19 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
20 eqid 
 |-  ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
21 eqid 
 |-  ( coe1 ` K ) = ( coe1 ` K )
22 1 17 2 18 19 20 21 ply1coe 
 |-  ( ( R e. Ring /\ K e. B ) -> K = ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` K ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) )
23 22 3adant3 
 |-  ( ( R e. Ring /\ K e. B /\ L e. B ) -> K = ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` K ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) )
24 eqid 
 |-  ( coe1 ` L ) = ( coe1 ` L )
25 1 17 2 18 19 20 24 ply1coe 
 |-  ( ( R e. Ring /\ L e. B ) -> L = ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` L ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) )
26 25 3adant2 
 |-  ( ( R e. Ring /\ K e. B /\ L e. B ) -> L = ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` L ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) )
27 23 26 eqeq12d 
 |-  ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( K = L <-> ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` K ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) = ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` L ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) )
28 27 adantr 
 |-  ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ A. k e. NN0 ( A ` k ) = ( C ` k ) ) -> ( K = L <-> ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` K ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) = ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` L ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) )
29 16 28 mpbird 
 |-  ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ A. k e. NN0 ( A ` k ) = ( C ` k ) ) -> K = L )
30 29 ex 
 |-  ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( A. k e. NN0 ( A ` k ) = ( C ` k ) -> K = L ) )