Metamath Proof Explorer

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 ‘ 𝑆 ) ) → ( 𝐹 = 𝐺 ↔ 𝐴 = 𝐵 ) )