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	$⊢ P = {Poly}_{1} (R)$
	ply1scleq.b	$⊢ B = {Base}_{R}$
	ply1scleq.a	$⊢ A = algSc (P)$
	ply1scleq.r	$⊢ φ \to R \in Ring$
	ply1scleq.e	$⊢ φ \to E \in B$
	ply1scleq.f	$⊢ φ \to F \in B$
Assertion	ply1scleq	$⊢ φ \to (A (E) = A (F) \leftrightarrow E = F)$

Proof

Step	Hyp	Ref	Expression
1		ply1scleq.p	$⊢ P = {Poly}_{1} (R)$
2		ply1scleq.b	$⊢ B = {Base}_{R}$
3		ply1scleq.a	$⊢ A = algSc (P)$
4		ply1scleq.r	$⊢ φ \to R \in Ring$
5		ply1scleq.e	$⊢ φ \to E \in B$
6		ply1scleq.f	$⊢ φ \to F \in B$
7		fveq2	$⊢ d = 0 \to {coe}_{1} (A (E)) (d) = {coe}_{1} (A (E)) (0)$
8		fveq2	$⊢ d = 0 \to {coe}_{1} (A (F)) (d) = {coe}_{1} (A (F)) (0)$
9	7 8	eqeq12d	$⊢ d = 0 \to ({coe}_{1} (A (E)) (d) = {coe}_{1} (A (F)) (d) \leftrightarrow {coe}_{1} (A (E)) (0) = {coe}_{1} (A (F)) (0))$
10		eqid	$⊢ {Base}_{P} = {Base}_{P}$
11	1 3 2 10	ply1sclcl	$⊢ (R \in Ring \land E \in B) \to A (E) \in {Base}_{P}$
12	4 5 11	syl2anc	$⊢ φ \to A (E) \in {Base}_{P}$
13	1 3 2 10	ply1sclcl	$⊢ (R \in Ring \land F \in B) \to A (F) \in {Base}_{P}$
14	4 6 13	syl2anc	$⊢ φ \to A (F) \in {Base}_{P}$
15		eqid	$⊢ {coe}_{1} (A (E)) = {coe}_{1} (A (E))$
16		eqid	$⊢ {coe}_{1} (A (F)) = {coe}_{1} (A (F))$
17	1 10 15 16	ply1coe1eq	$⊢ (R \in Ring \land A (E) \in {Base}_{P} \land A (F) \in {Base}_{P}) \to (\forall d \in ℕ_{0} {coe}_{1} (A (E)) (d) = {coe}_{1} (A (F)) (d) \leftrightarrow A (E) = A (F))$
18	4 12 14 17	syl3anc	$⊢ φ \to (\forall d \in ℕ_{0} {coe}_{1} (A (E)) (d) = {coe}_{1} (A (F)) (d) \leftrightarrow A (E) = A (F))$
19	18	biimpar	$⊢ (φ \land A (E) = A (F)) \to \forall d \in ℕ_{0} {coe}_{1} (A (E)) (d) = {coe}_{1} (A (F)) (d)$
20		0nn0	$⊢ 0 \in ℕ_{0}$
21	20	a1i	$⊢ (φ \land A (E) = A (F)) \to 0 \in ℕ_{0}$
22	9 19 21	rspcdva	$⊢ (φ \land A (E) = A (F)) \to {coe}_{1} (A (E)) (0) = {coe}_{1} (A (F)) (0)$
23	1 3 2	ply1sclid	$⊢ (R \in Ring \land E \in B) \to E = {coe}_{1} (A (E)) (0)$
24	4 5 23	syl2anc	$⊢ φ \to E = {coe}_{1} (A (E)) (0)$
25	24	adantr	$⊢ (φ \land A (E) = A (F)) \to E = {coe}_{1} (A (E)) (0)$
26	1 3 2	ply1sclid	$⊢ (R \in Ring \land F \in B) \to F = {coe}_{1} (A (F)) (0)$
27	4 6 26	syl2anc	$⊢ φ \to F = {coe}_{1} (A (F)) (0)$
28	27	adantr	$⊢ (φ \land A (E) = A (F)) \to F = {coe}_{1} (A (F)) (0)$
29	22 25 28	3eqtr4d	$⊢ (φ \land A (E) = A (F)) \to E = F$
30		fveq2	$⊢ E = F \to A (E) = A (F)$
31	30	adantl	$⊢ (φ \land E = F) \to A (E) = A (F)$
32	29 31	impbida	$⊢ φ \to (A (E) = A (F) \leftrightarrow E = F)$

Metamath Proof Explorer

Theorem ply1scleq

Proof