ply1gsumz

Description: If a polynomial given as a sum of scaled monomials by factors A is the zero polynomial, then all factors A are zero. (Contributed by Thierry Arnoux, 20-Feb-2025)

	Ref	Expression
Hypotheses	ply1gsumz.p	$⊢ P = {Poly}_{1} (R)$
	ply1gsumz.b	$⊢ B = {Base}_{R}$
	ply1gsumz.n	$⊢ φ \to N \in ℕ_{0}$
	ply1gsumz.r	$⊢ φ \to R \in Ring$
	ply1gsumz.f	$⊢ F = (n \in (0 ..^N) ⟼ n \cdot_{{mulGrp}_{P}} {var}_{1} (R))$
	ply1gsumz.1	$⊢ \underset{˙}{0} = 0_{R}$
	ply1gsumz.z	$⊢ Z = 0_{P}$
	ply1gsumz.a	$⊢ φ \to A : (0 ..^N) ⟶ B$
	ply1gsumz.s	$⊢ φ \to \sum_{P} (A {\cdot_{P}}_{f} F) = Z$
Assertion	ply1gsumz	$⊢ φ \to A = (0 ..^N) \times \{\underset{˙}{0}\}$

Proof

Step	Hyp	Ref	Expression
1		ply1gsumz.p	$⊢ P = {Poly}_{1} (R)$
2		ply1gsumz.b	$⊢ B = {Base}_{R}$
3		ply1gsumz.n	$⊢ φ \to N \in ℕ_{0}$
4		ply1gsumz.r	$⊢ φ \to R \in Ring$
5		ply1gsumz.f	$⊢ F = (n \in (0 ..^N) ⟼ n \cdot_{{mulGrp}_{P}} {var}_{1} (R))$
6		ply1gsumz.1	$⊢ \underset{˙}{0} = 0_{R}$
7		ply1gsumz.z	$⊢ Z = 0_{P}$
8		ply1gsumz.a	$⊢ φ \to A : (0 ..^N) ⟶ B$
9		ply1gsumz.s	$⊢ φ \to \sum_{P} (A {\cdot_{P}}_{f} F) = Z$
10	8	ffnd	$⊢ φ \to A Fn (0 ..^N)$
11	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
12		eqid	$⊢ {Base}_{P} = {Base}_{P}$
13	12 7	ring0cl	$⊢ P \in Ring \to Z \in {Base}_{P}$
14	4 11 13	3syl	$⊢ φ \to Z \in {Base}_{P}$
15		eqid	$⊢ {coe}_{1} (Z) = {coe}_{1} (Z)$
16	15 12 1 2	coe1f	$⊢ Z \in {Base}_{P} \to {coe}_{1} (Z) : ℕ_{0} ⟶ B$
17	14 16	syl	$⊢ φ \to {coe}_{1} (Z) : ℕ_{0} ⟶ B$
18	17	ffnd	$⊢ φ \to {coe}_{1} (Z) Fn ℕ_{0}$
19		fzo0ssnn0	$⊢ (0 ..^N) \subseteq ℕ_{0}$
20	19	a1i	$⊢ φ \to (0 ..^N) \subseteq ℕ_{0}$
21	18 20	fnssresd	$⊢ φ \to ({{coe}_{1} (Z) ↾}_{(0 ..^N)}) Fn (0 ..^N)$
22		simpr	$⊢ (φ \land j \in (0 ..^N)) \to j \in (0 ..^N)$
23	22	fvresd	$⊢ (φ \land j \in (0 ..^N)) \to ({{coe}_{1} (Z) ↾}_{(0 ..^N)}) (j) = {coe}_{1} (Z) (j)$
24		elfzonn0	$⊢ j \in (0 ..^N) \to j \in ℕ_{0}$
25	9 14	eqeltrd	$⊢ φ \to \sum_{P} (A {\cdot_{P}}_{f} F) \in {Base}_{P}$
26		eqid	$⊢ {coe}_{1} (\sum_{P} (A {\cdot_{P}}_{f} F)) = {coe}_{1} (\sum_{P} (A {\cdot_{P}}_{f} F))$
27	1 12 26 15	ply1coe1eq	$⊢ (R \in Ring \land \sum_{P} (A {\cdot_{P}}_{f} F) \in {Base}_{P} \land Z \in {Base}_{P}) \to (\forall j \in ℕ_{0} {coe}_{1} (\sum_{P} (A {\cdot_{P}}_{f} F)) (j) = {coe}_{1} (Z) (j) \leftrightarrow \sum_{P} (A {\cdot_{P}}_{f} F) = Z)$
28	27	biimpar	$⊢ ((R \in Ring \land \sum_{P} (A {\cdot_{P}}_{f} F) \in {Base}_{P} \land Z \in {Base}_{P}) \land \sum_{P} (A {\cdot_{P}}_{f} F) = Z) \to \forall j \in ℕ_{0} {coe}_{1} (\sum_{P} (A {\cdot_{P}}_{f} F)) (j) = {coe}_{1} (Z) (j)$
29	4 25 14 9 28	syl31anc	$⊢ φ \to \forall j \in ℕ_{0} {coe}_{1} (\sum_{P} (A {\cdot_{P}}_{f} F)) (j) = {coe}_{1} (Z) (j)$
30	29	r19.21bi	$⊢ (φ \land j \in ℕ_{0}) \to {coe}_{1} (\sum_{P} (A {\cdot_{P}}_{f} F)) (j) = {coe}_{1} (Z) (j)$
31	24 30	sylan2	$⊢ (φ \land j \in (0 ..^N)) \to {coe}_{1} (\sum_{P} (A {\cdot_{P}}_{f} F)) (j) = {coe}_{1} (Z) (j)$
32	10	adantr	$⊢ (φ \land j \in (0 ..^N)) \to A Fn (0 ..^N)$
33		nfv	$⊢ Ⅎ n φ$
34		ovexd	$⊢ (φ \land n \in (0 ..^N)) \to n \cdot_{{mulGrp}_{P}} {var}_{1} (R) \in V$
35	33 34 5	fnmptd	$⊢ φ \to F Fn (0 ..^N)$
36	35	adantr	$⊢ (φ \land j \in (0 ..^N)) \to F Fn (0 ..^N)$
37		ovexd	$⊢ (φ \land j \in (0 ..^N)) \to (0 ..^N) \in V$
38		inidm	$⊢ (0 ..^N) \cap (0 ..^N) = (0 ..^N)$
39		eqidd	$⊢ ((φ \land j \in (0 ..^N)) \land i \in (0 ..^N)) \to A (i) = A (i)$
40		oveq1	$⊢ n = i \to n \cdot_{{mulGrp}_{P}} {var}_{1} (R) = i \cdot_{{mulGrp}_{P}} {var}_{1} (R)$
41		simpr	$⊢ ((φ \land j \in (0 ..^N)) \land i \in (0 ..^N)) \to i \in (0 ..^N)$
42		ovexd	$⊢ ((φ \land j \in (0 ..^N)) \land i \in (0 ..^N)) \to i \cdot_{{mulGrp}_{P}} {var}_{1} (R) \in V$
43	5 40 41 42	fvmptd3	$⊢ ((φ \land j \in (0 ..^N)) \land i \in (0 ..^N)) \to F (i) = i \cdot_{{mulGrp}_{P}} {var}_{1} (R)$
44	32 36 37 37 38 39 43	offval	$⊢ (φ \land j \in (0 ..^N)) \to A {\cdot_{P}}_{f} F = (i \in (0 ..^N) ⟼ A (i) \cdot_{P} (i \cdot_{{mulGrp}_{P}} {var}_{1} (R)))$
45	44	oveq2d	$⊢ (φ \land j \in (0 ..^N)) \to \sum_{P} (A {\cdot_{P}}_{f} F) = \underset{i \in (0 ..^N)}{\sum_{P}} (A (i) \cdot_{P} (i \cdot_{{mulGrp}_{P}} {var}_{1} (R)))$
46	45	fveq2d	$⊢ (φ \land j \in (0 ..^N)) \to {coe}_{1} (\sum_{P} (A {\cdot_{P}}_{f} F)) = {coe}_{1} (\underset{i \in (0 ..^N)}{\sum_{P}} (A (i) \cdot_{P} (i \cdot_{{mulGrp}_{P}} {var}_{1} (R))))$
47	46	fveq1d	$⊢ (φ \land j \in (0 ..^N)) \to {coe}_{1} (\sum_{P} (A {\cdot_{P}}_{f} F)) (j) = {coe}_{1} (\underset{i \in (0 ..^N)}{\sum_{P}} (A (i) \cdot_{P} (i \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) (j)$
48		eqid	$⊢ {var}_{1} (R) = {var}_{1} (R)$
49		eqid	$⊢ \cdot_{{mulGrp}_{P}} = \cdot_{{mulGrp}_{P}}$
50	4	adantr	$⊢ (φ \land j \in (0 ..^N)) \to R \in Ring$
51		eqid	$⊢ \cdot_{P} = \cdot_{P}$
52	8	adantr	$⊢ (φ \land j \in (0 ..^N)) \to A : (0 ..^N) ⟶ B$
53	52	ffvelcdmda	$⊢ ((φ \land j \in (0 ..^N)) \land i \in (0 ..^N)) \to A (i) \in B$
54	53	ralrimiva	$⊢ (φ \land j \in (0 ..^N)) \to \forall i \in (0 ..^N) A (i) \in B$
55	3	adantr	$⊢ (φ \land j \in (0 ..^N)) \to N \in ℕ_{0}$
56		fveq2	$⊢ i = j \to A (i) = A (j)$
57	1 12 48 49 50 2 51 6 54 22 55 56	gsummoncoe1fzo	$⊢ (φ \land j \in (0 ..^N)) \to {coe}_{1} (\underset{i \in (0 ..^N)}{\sum_{P}} (A (i) \cdot_{P} (i \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) (j) = A (j)$
58	47 57	eqtrd	$⊢ (φ \land j \in (0 ..^N)) \to {coe}_{1} (\sum_{P} (A {\cdot_{P}}_{f} F)) (j) = A (j)$
59	23 31 58	3eqtr2rd	$⊢ (φ \land j \in (0 ..^N)) \to A (j) = ({{coe}_{1} (Z) ↾}_{(0 ..^N)}) (j)$
60	10 21 59	eqfnfvd	$⊢ φ \to A = {{coe}_{1} (Z) ↾}_{(0 ..^N)}$
61	1 7 6	coe1z	$⊢ R \in Ring \to {coe}_{1} (Z) = ℕ_{0} \times \{\underset{˙}{0}\}$
62	4 61	syl	$⊢ φ \to {coe}_{1} (Z) = ℕ_{0} \times \{\underset{˙}{0}\}$
63	62	reseq1d	$⊢ φ \to {{coe}_{1} (Z) ↾}_{(0 ..^N)} = {(ℕ_{0} \times \{\underset{˙}{0}\}) ↾}_{(0 ..^N)}$
64	60 63	eqtrd	$⊢ φ \to A = {(ℕ_{0} \times \{\underset{˙}{0}\}) ↾}_{(0 ..^N)}$
65		xpssres	$⊢ (0 ..^N) \subseteq ℕ_{0} \to {(ℕ_{0} \times \{\underset{˙}{0}\}) ↾}_{(0 ..^N)} = (0 ..^N) \times \{\underset{˙}{0}\}$
66	19 65	ax-mp	$⊢ {(ℕ_{0} \times \{\underset{˙}{0}\}) ↾}_{(0 ..^N)} = (0 ..^N) \times \{\underset{˙}{0}\}$
67	64 66	eqtrdi	$⊢ φ \to A = (0 ..^N) \times \{\underset{˙}{0}\}$

Metamath Proof Explorer

Theorem ply1gsumz

Proof