Theorem ply1scleq

Description: Equality of a constant polynomial is the same as equality of the constant term. (Contributed by Thierry Arnoux, 24-Jul-2024)

	Ref	Expression
Hypotheses	ply1scleq.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1scleq.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	ply1scleq.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
	ply1scleq.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	ply1scleq.e	⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
	ply1scleq.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion	ply1scleq	⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) ↔ 𝐸 = 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		ply1scleq.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1scleq.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		ply1scleq.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
4		ply1scleq.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
5		ply1scleq.e	⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
6		ply1scleq.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7		fveq2	⊢ ( 𝑑 = 0 → ( ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) ‘ 𝑑 ) = ( ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) ‘ 0 ) )
8		fveq2	⊢ ( 𝑑 = 0 → ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 𝑑 ) = ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 0 ) )
9	7 8	eqeq12d	⊢ ( 𝑑 = 0 → ( ( ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) ‘ 𝑑 ) = ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 𝑑 ) ↔ ( ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) ‘ 0 ) = ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 0 ) ) )
10		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
11	1 3 2 10	ply1sclcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝐵 ) → ( 𝐴 ‘ 𝐸 ) ∈ ( Base ‘ 𝑃 ) )
12	4 5 11	syl2anc	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐸 ) ∈ ( Base ‘ 𝑃 ) )
13	1 3 2 10	ply1sclcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → ( 𝐴 ‘ 𝐹 ) ∈ ( Base ‘ 𝑃 ) )
14	4 6 13	syl2anc	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐹 ) ∈ ( Base ‘ 𝑃 ) )
15		eqid	⊢ ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) = ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) )
16		eqid	⊢ ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) = ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) )
17	1 10 15 16	ply1coe1eq	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ‘ 𝐸 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐴 ‘ 𝐹 ) ∈ ( Base ‘ 𝑃 ) ) → ( ∀ 𝑑 ∈ ℕ0 ( ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) ‘ 𝑑 ) = ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 𝑑 ) ↔ ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) ) )
18	4 12 14 17	syl3anc	⊢ ( 𝜑 → ( ∀ 𝑑 ∈ ℕ0 ( ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) ‘ 𝑑 ) = ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 𝑑 ) ↔ ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) ) )
19	18	biimpar	⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) ) → ∀ 𝑑 ∈ ℕ0 ( ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) ‘ 𝑑 ) = ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 𝑑 ) )
20		0nn0	⊢ 0 ∈ ℕ0
21	20	a1i	⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) ) → 0 ∈ ℕ0 )
22	9 19 21	rspcdva	⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) ) → ( ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) ‘ 0 ) = ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 0 ) )
23	1 3 2	ply1sclid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝐵 ) → 𝐸 = ( ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) ‘ 0 ) )
24	4 5 23	syl2anc	⊢ ( 𝜑 → 𝐸 = ( ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) ‘ 0 ) )
25	24	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) ) → 𝐸 = ( ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) ‘ 0 ) )
26	1 3 2	ply1sclid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → 𝐹 = ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 0 ) )
27	4 6 26	syl2anc	⊢ ( 𝜑 → 𝐹 = ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 0 ) )
28	27	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) ) → 𝐹 = ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 0 ) )
29	22 25 28	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) ) → 𝐸 = 𝐹 )
30		fveq2	⊢ ( 𝐸 = 𝐹 → ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) )
31	30	adantl	⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) )
32	29 31	impbida	⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) ↔ 𝐸 = 𝐹 ) )