Theorem 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	⊢ 𝐴 = ( coeff ‘ 𝐹 )
	coeadd.2	⊢ 𝐵 = ( coeff ‘ 𝐺 )
Assertion	coe11	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐹 = 𝐺 ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		coefv0.1	⊢ 𝐴 = ( coeff ‘ 𝐹 )
2		coeadd.2	⊢ 𝐵 = ( coeff ‘ 𝐺 )
3		fveq2	⊢ ( 𝐹 = 𝐺 → ( coeff ‘ 𝐹 ) = ( coeff ‘ 𝐺 ) )
4	3 1 2	3eqtr4g	⊢ ( 𝐹 = 𝐺 → 𝐴 = 𝐵 )
5		simp3	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
6	5	cnveqd	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 = 𝐵 ) → ◡ 𝐴 = ◡ 𝐵 )
7	6	imaeq1d	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 = 𝐵 ) → ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) = ( ◡ 𝐵 “ ( ℂ ∖ { 0 } ) ) )
8	7	supeq1d	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 = 𝐵 ) → sup ( ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) = sup ( ( ◡ 𝐵 “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) )
9	1	dgrval	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) = sup ( ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) )
10	9	3ad2ant1	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 = 𝐵 ) → ( deg ‘ 𝐹 ) = sup ( ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) )
11	2	dgrval	⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐺 ) = sup ( ( ◡ 𝐵 “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) )
12	11	3ad2ant2	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 = 𝐵 ) → ( deg ‘ 𝐺 ) = sup ( ( ◡ 𝐵 “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) )
13	8 10 12	3eqtr4d	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 = 𝐵 ) → ( deg ‘ 𝐹 ) = ( deg ‘ 𝐺 ) )
14	13	oveq2d	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 = 𝐵 ) → ( 0 ... ( deg ‘ 𝐹 ) ) = ( 0 ... ( deg ‘ 𝐺 ) ) )
15		simpl3	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 = 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → 𝐴 = 𝐵 )
16	15	fveq1d	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 = 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝐴 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) )
17	16	oveq1d	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 = 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
18	14 17	sumeq12dv	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 = 𝐵 ) → Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
19	18	mpteq2dv	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 = 𝐵 ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
20		eqid	⊢ ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 )
21	1 20	coeid	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
22	21	3ad2ant1	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 = 𝐵 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
23		eqid	⊢ ( deg ‘ 𝐺 ) = ( deg ‘ 𝐺 )
24	2 23	coeid	⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
25	24	3ad2ant2	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 = 𝐵 ) → 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
26	19 22 25	3eqtr4d	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 = 𝐵 ) → 𝐹 = 𝐺 )
27	26	3expia	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐴 = 𝐵 → 𝐹 = 𝐺 ) )
28	4 27	impbid2	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐹 = 𝐺 ↔ 𝐴 = 𝐵 ) )