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 = {Poly}_{1} (R)$
	eqcoe1ply1eq.b	$⊢ B = {Base}_{P}$
	eqcoe1ply1eq.a	$⊢ A = {coe}_{1} (K)$
	eqcoe1ply1eq.c	$⊢ C = {coe}_{1} (L)$
Assertion	ply1coe1eq	$⊢ (R \in Ring \land K \in B \land L \in B) \to (\forall k \in ℕ_{0} A (k) = C (k) \leftrightarrow K = L)$

Step	Hyp	Ref	Expression
1		eqcoe1ply1eq.p	$⊢ P = {Poly}_{1} (R)$
2		eqcoe1ply1eq.b	$⊢ B = {Base}_{P}$
3		eqcoe1ply1eq.a	$⊢ A = {coe}_{1} (K)$
4		eqcoe1ply1eq.c	$⊢ C = {coe}_{1} (L)$
5	1 2 3 4	eqcoe1ply1eq	$⊢ (R \in Ring \land K \in B \land L \in B) \to (\forall k \in ℕ_{0} A (k) = C (k) \to K = L)$
6		fveq2	$⊢ K = L \to {coe}_{1} (K) = {coe}_{1} (L)$
7	6	adantl	$⊢ ((R \in Ring \land K \in B \land L \in B) \land K = L) \to {coe}_{1} (K) = {coe}_{1} (L)$
8	7 3 4	3eqtr4g	$⊢ ((R \in Ring \land K \in B \land L \in B) \land K = L) \to A = C$
9	8	adantr	$⊢ (((R \in Ring \land K \in B \land L \in B) \land K = L) \land k \in ℕ_{0}) \to A = C$
10	9	fveq1d	$⊢ (((R \in Ring \land K \in B \land L \in B) \land K = L) \land k \in ℕ_{0}) \to A (k) = C (k)$
11	10	ralrimiva	$⊢ ((R \in Ring \land K \in B \land L \in B) \land K = L) \to \forall k \in ℕ_{0} A (k) = C (k)$
12	11	ex	$⊢ (R \in Ring \land K \in B \land L \in B) \to (K = L \to \forall k \in ℕ_{0} A (k) = C (k))$
13	5 12	impbid	$⊢ (R \in Ring \land K \in B \land L \in B) \to (\forall k \in ℕ_{0} A (k) = C (k) \leftrightarrow K = L)$

Metamath Proof Explorer