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

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 ) )