Metamath Proof Explorer


Theorem ply1coe1eq

Description: Two polynomials over the same ring are equal iff they have identical coefficients. (Contributed by AV, 13-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 ply1coe1eq
|- ( ( 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 1 2 3 4 eqcoe1ply1eq
 |-  ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( A. k e. NN0 ( A ` k ) = ( C ` k ) -> K = L ) )
6 fveq2
 |-  ( K = L -> ( coe1 ` K ) = ( coe1 ` L ) )
7 6 adantl
 |-  ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ K = L ) -> ( coe1 ` K ) = ( coe1 ` L ) )
8 7 3 4 3eqtr4g
 |-  ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ K = L ) -> A = C )
9 8 adantr
 |-  ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ K = L ) /\ k e. NN0 ) -> A = C )
10 9 fveq1d
 |-  ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ K = L ) /\ k e. NN0 ) -> ( A ` k ) = ( C ` k ) )
11 10 ralrimiva
 |-  ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ K = L ) -> A. k e. NN0 ( A ` k ) = ( C ` k ) )
12 11 ex
 |-  ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( K = L -> A. k e. NN0 ( A ` k ) = ( C ` k ) ) )
13 5 12 impbid
 |-  ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( A. k e. NN0 ( A ` k ) = ( C ` k ) <-> K = L ) )