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