This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ∈ Ring ∧ K ∈ B ∧ L ∈ B → ∀ k ∈ ℕ 0 A ⁡ k = C ⁡ k ↔ 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 1 2 3 4 eqcoe1ply1eq ⊢ R ∈ Ring ∧ K ∈ B ∧ L ∈ B → ∀ k ∈ ℕ 0 A ⁡ k = C ⁡ k → K = L
6 fveq2 ⊢ K = L → coe 1 ⁡ K = coe 1 ⁡ L
7 6 adantl ⊢ R ∈ Ring ∧ K ∈ B ∧ L ∈ B ∧ K = L → coe 1 ⁡ K = coe 1 ⁡ L
8 7 3 4 3eqtr4g ⊢ R ∈ Ring ∧ K ∈ B ∧ L ∈ B ∧ K = L → A = C
9 8 adantr ⊢ R ∈ Ring ∧ K ∈ B ∧ L ∈ B ∧ K = L ∧ k ∈ ℕ 0 → A = C
10 9 fveq1d ⊢ R ∈ Ring ∧ K ∈ B ∧ L ∈ B ∧ K = L ∧ k ∈ ℕ 0 → A ⁡ k = C ⁡ k
11 10 ralrimiva ⊢ R ∈ Ring ∧ K ∈ B ∧ L ∈ B ∧ K = L → ∀ k ∈ ℕ 0 A ⁡ k = C ⁡ k
12 11 ex ⊢ R ∈ Ring ∧ K ∈ B ∧ L ∈ B → K = L → ∀ k ∈ ℕ 0 A ⁡ k = C ⁡ k
13 5 12 impbid ⊢ R ∈ Ring ∧ K ∈ B ∧ L ∈ B → ∀ k ∈ ℕ 0 A ⁡ k = C ⁡ k ↔ K = L