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 ( 𝐴 ‘ 𝑘 ) = ( 𝐶 ‘ 𝑘 ) ↔ 𝐾 = 𝐿 ) )