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 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
eqcoe1ply1eq.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
eqcoe1ply1eq.a ⊢ 𝐴 = ( coe1 ‘ 𝐾 )
eqcoe1ply1eq.c ⊢ 𝐶 = ( coe1 ‘ 𝐿 )
Assertion ply1coe1eq ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( ∀ 𝑘 ∈ ℕ0 ( 𝐴 ‘ 𝑘 ) = ( 𝐶 ‘ 𝑘 ) ↔ 𝐾 = 𝐿 ) )

Proof

Step Hyp Ref Expression
1 eqcoe1ply1eq.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 eqcoe1ply1eq.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 eqcoe1ply1eq.a ⊢ 𝐴 = ( coe1 ‘ 𝐾 )
4 eqcoe1ply1eq.c ⊢ 𝐶 = ( coe1 ‘ 𝐿 )
5 1 2 3 4 eqcoe1ply1eq ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( ∀ 𝑘 ∈ ℕ0 ( 𝐴 ‘ 𝑘 ) = ( 𝐶 ‘ 𝑘 ) → 𝐾 = 𝐿 ) )
6 fveq2 ⊢ ( 𝐾 = 𝐿 → ( coe1 ‘ 𝐾 ) = ( coe1 ‘ 𝐿 ) )
7 6 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝐾 = 𝐿 ) → ( coe1 ‘ 𝐾 ) = ( coe1 ‘ 𝐿 ) )
8 7 3 4 3eqtr4g ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝐾 = 𝐿 ) → 𝐴 = 𝐶 )
9 8 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝐾 = 𝐿 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 = 𝐶 )
10 9 fveq1d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝐾 = 𝐿 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) = ( 𝐶 ‘ 𝑘 ) )
11 10 ralrimiva ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝐾 = 𝐿 ) → ∀ 𝑘 ∈ ℕ0 ( 𝐴 ‘ 𝑘 ) = ( 𝐶 ‘ 𝑘 ) )
12 11 ex ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( 𝐾 = 𝐿 → ∀ 𝑘 ∈ ℕ0 ( 𝐴 ‘ 𝑘 ) = ( 𝐶 ‘ 𝑘 ) ) )
13 5 12 impbid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( ∀ 𝑘 ∈ ℕ0 ( 𝐴 ‘ 𝑘 ) = ( 𝐶 ‘ 𝑘 ) ↔ 𝐾 = 𝐿 ) )