coe11

Description: The coefficient function is one-to-one, so if the coefficients are equal then the functions are equal and vice-versa. (Contributed by Mario Carneiro, 24-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

	Ref	Expression
Hypotheses	coefv0.1	$⊢ A = coeff (F)$
	coeadd.2	$⊢ B = coeff (G)$
Assertion	coe11	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to (F = G \leftrightarrow A = B)$

Proof

Step	Hyp	Ref	Expression
1		coefv0.1	$⊢ A = coeff (F)$
2		coeadd.2	$⊢ B = coeff (G)$
3		fveq2	$⊢ F = G \to coeff (F) = coeff (G)$
4	3 1 2	3eqtr4g	$⊢ F = G \to A = B$
5		simp3	$⊢ (F \in Poly (S) \land G \in Poly (S) \land A = B) \to A = B$
6	5	cnveqd	$⊢ (F \in Poly (S) \land G \in Poly (S) \land A = B) \to A^{-1} = B^{-1}$
7	6	imaeq1d	$⊢ (F \in Poly (S) \land G \in Poly (S) \land A = B) \to A^{-1} [ℂ ∖ \{0\}] = B^{-1} [ℂ ∖ \{0\}]$
8	7	supeq1d	$⊢ (F \in Poly (S) \land G \in Poly (S) \land A = B) \to sup (A^{-1} [ℂ ∖ \{0\}] ℕ_{0} <) = sup (B^{-1} [ℂ ∖ \{0\}] ℕ_{0} <)$
9	1	dgrval	$⊢ F \in Poly (S) \to \deg (F) = sup (A^{-1} [ℂ ∖ \{0\}] ℕ_{0} <)$
10	9	3ad2ant1	$⊢ (F \in Poly (S) \land G \in Poly (S) \land A = B) \to \deg (F) = sup (A^{-1} [ℂ ∖ \{0\}] ℕ_{0} <)$
11	2	dgrval	$⊢ G \in Poly (S) \to \deg (G) = sup (B^{-1} [ℂ ∖ \{0\}] ℕ_{0} <)$
12	11	3ad2ant2	$⊢ (F \in Poly (S) \land G \in Poly (S) \land A = B) \to \deg (G) = sup (B^{-1} [ℂ ∖ \{0\}] ℕ_{0} <)$
13	8 10 12	3eqtr4d	$⊢ (F \in Poly (S) \land G \in Poly (S) \land A = B) \to \deg (F) = \deg (G)$
14	13	oveq2d	$⊢ (F \in Poly (S) \land G \in Poly (S) \land A = B) \to (0 \dots \deg (F)) = (0 \dots \deg (G))$
15		simpl3	$⊢ ((F \in Poly (S) \land G \in Poly (S) \land A = B) \land k \in (0 \dots \deg (F))) \to A = B$
16	15	fveq1d	$⊢ ((F \in Poly (S) \land G \in Poly (S) \land A = B) \land k \in (0 \dots \deg (F))) \to A (k) = B (k)$
17	16	oveq1d	$⊢ ((F \in Poly (S) \land G \in Poly (S) \land A = B) \land k \in (0 \dots \deg (F))) \to A (k) z^{k} = B (k) z^{k}$
18	14 17	sumeq12dv	$⊢ (F \in Poly (S) \land G \in Poly (S) \land A = B) \to \sum_{k = 0}^{\deg (F)} A (k) z^{k} = \sum_{k = 0}^{\deg (G)} B (k) z^{k}$
19	18	mpteq2dv	$⊢ (F \in Poly (S) \land G \in Poly (S) \land A = B) \to (z \in ℂ ⟼ \sum_{k = 0}^{\deg (F)} A (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{\deg (G)} B (k) z^{k})$
20		eqid	$⊢ \deg (F) = \deg (F)$
21	1 20	coeid	$⊢ F \in Poly (S) \to F = (z \in ℂ ⟼ \sum_{k = 0}^{\deg (F)} A (k) z^{k})$
22	21	3ad2ant1	$⊢ (F \in Poly (S) \land G \in Poly (S) \land A = B) \to F = (z \in ℂ ⟼ \sum_{k = 0}^{\deg (F)} A (k) z^{k})$
23		eqid	$⊢ \deg (G) = \deg (G)$
24	2 23	coeid	$⊢ G \in Poly (S) \to G = (z \in ℂ ⟼ \sum_{k = 0}^{\deg (G)} B (k) z^{k})$
25	24	3ad2ant2	$⊢ (F \in Poly (S) \land G \in Poly (S) \land A = B) \to G = (z \in ℂ ⟼ \sum_{k = 0}^{\deg (G)} B (k) z^{k})$
26	19 22 25	3eqtr4d	$⊢ (F \in Poly (S) \land G \in Poly (S) \land A = B) \to F = G$
27	26	3expia	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to (A = B \to F = G)$
28	4 27	impbid2	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to (F = G \leftrightarrow A = B)$

Metamath Proof Explorer

Theorem coe11

Proof