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

Proof

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		fveq2	$⊢ k = n \to A (k) = A (n)$
6		fveq2	$⊢ k = n \to C (k) = C (n)$
7	5 6	eqeq12d	$⊢ k = n \to (A (k) = C (k) \leftrightarrow A (n) = C (n))$
8	7	rspccv	$⊢ \forall k \in ℕ_{0} A (k) = C (k) \to (n \in ℕ_{0} \to A (n) = C (n))$
9	8	adantl	$⊢ ((R \in Ring \land K \in B \land L \in B) \land \forall k \in ℕ_{0} A (k) = C (k)) \to (n \in ℕ_{0} \to A (n) = C (n))$
10	9	imp	$⊢ (((R \in Ring \land K \in B \land L \in B) \land \forall k \in ℕ_{0} A (k) = C (k)) \land n \in ℕ_{0}) \to A (n) = C (n)$
11	3	fveq1i	$⊢ A (n) = {coe}_{1} (K) (n)$
12	4	fveq1i	$⊢ C (n) = {coe}_{1} (L) (n)$
13	10 11 12	3eqtr3g	$⊢ (((R \in Ring \land K \in B \land L \in B) \land \forall k \in ℕ_{0} A (k) = C (k)) \land n \in ℕ_{0}) \to {coe}_{1} (K) (n) = {coe}_{1} (L) (n)$
14	13	oveq1d	$⊢ (((R \in Ring \land K \in B \land L \in B) \land \forall k \in ℕ_{0} A (k) = C (k)) \land n \in ℕ_{0}) \to {coe}_{1} (K) (n) \cdot_{P} (n \cdot_{{mulGrp}_{P}} {var}_{1} (R)) = {coe}_{1} (L) (n) \cdot_{P} (n \cdot_{{mulGrp}_{P}} {var}_{1} (R))$
15	14	mpteq2dva	$⊢ ((R \in Ring \land K \in B \land L \in B) \land \forall k \in ℕ_{0} A (k) = C (k)) \to (n \in ℕ_{0} ⟼ {coe}_{1} (K) (n) \cdot_{P} (n \cdot_{{mulGrp}_{P}} {var}_{1} (R))) = (n \in ℕ_{0} ⟼ {coe}_{1} (L) (n) \cdot_{P} (n \cdot_{{mulGrp}_{P}} {var}_{1} (R)))$
16	15	oveq2d	$⊢ ((R \in Ring \land K \in B \land L \in B) \land \forall k \in ℕ_{0} A (k) = C (k)) \to \underset{n \in ℕ_{0}}{\sum_{P}} ({coe}_{1} (K) (n) \cdot_{P} (n \cdot_{{mulGrp}_{P}} {var}_{1} (R))) = \underset{n \in ℕ_{0}}{\sum_{P}} ({coe}_{1} (L) (n) \cdot_{P} (n \cdot_{{mulGrp}_{P}} {var}_{1} (R)))$
17		eqid	$⊢ {var}_{1} (R) = {var}_{1} (R)$
18		eqid	$⊢ \cdot_{P} = \cdot_{P}$
19		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
20		eqid	$⊢ \cdot_{{mulGrp}_{P}} = \cdot_{{mulGrp}_{P}}$
21		eqid	$⊢ {coe}_{1} (K) = {coe}_{1} (K)$
22	1 17 2 18 19 20 21	ply1coe	$⊢ (R \in Ring \land K \in B) \to K = \underset{n \in ℕ_{0}}{\sum_{P}} ({coe}_{1} (K) (n) \cdot_{P} (n \cdot_{{mulGrp}_{P}} {var}_{1} (R)))$
23	22	3adant3	$⊢ (R \in Ring \land K \in B \land L \in B) \to K = \underset{n \in ℕ_{0}}{\sum_{P}} ({coe}_{1} (K) (n) \cdot_{P} (n \cdot_{{mulGrp}_{P}} {var}_{1} (R)))$
24		eqid	$⊢ {coe}_{1} (L) = {coe}_{1} (L)$
25	1 17 2 18 19 20 24	ply1coe	$⊢ (R \in Ring \land L \in B) \to L = \underset{n \in ℕ_{0}}{\sum_{P}} ({coe}_{1} (L) (n) \cdot_{P} (n \cdot_{{mulGrp}_{P}} {var}_{1} (R)))$
26	25	3adant2	$⊢ (R \in Ring \land K \in B \land L \in B) \to L = \underset{n \in ℕ_{0}}{\sum_{P}} ({coe}_{1} (L) (n) \cdot_{P} (n \cdot_{{mulGrp}_{P}} {var}_{1} (R)))$
27	23 26	eqeq12d	$⊢ (R \in Ring \land K \in B \land L \in B) \to (K = L \leftrightarrow \underset{n \in ℕ_{0}}{\sum_{P}} ({coe}_{1} (K) (n) \cdot_{P} (n \cdot_{{mulGrp}_{P}} {var}_{1} (R))) = \underset{n \in ℕ_{0}}{\sum_{P}} ({coe}_{1} (L) (n) \cdot_{P} (n \cdot_{{mulGrp}_{P}} {var}_{1} (R))))$
28	27	adantr	$⊢ ((R \in Ring \land K \in B \land L \in B) \land \forall k \in ℕ_{0} A (k) = C (k)) \to (K = L \leftrightarrow \underset{n \in ℕ_{0}}{\sum_{P}} ({coe}_{1} (K) (n) \cdot_{P} (n \cdot_{{mulGrp}_{P}} {var}_{1} (R))) = \underset{n \in ℕ_{0}}{\sum_{P}} ({coe}_{1} (L) (n) \cdot_{P} (n \cdot_{{mulGrp}_{P}} {var}_{1} (R))))$
29	16 28	mpbird	$⊢ ((R \in Ring \land K \in B \land L \in B) \land \forall k \in ℕ_{0} A (k) = C (k)) \to K = L$
30	29	ex	$⊢ (R \in Ring \land K \in B \land L \in B) \to (\forall k \in ℕ_{0} A (k) = C (k) \to K = L)$

Metamath Proof Explorer

Theorem eqcoe1ply1eq

Proof