This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
ply1gsumz.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
ply1gsumz.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
ply1gsumz.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
ply1gsumz.f ⊢ 𝐹 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) )
ply1gsumz.1 ⊢ 0 = ( 0g ‘ 𝑅 )
ply1gsumz.z ⊢ 𝑍 = ( 0g ‘ 𝑃 )
ply1gsumz.a ⊢ ( 𝜑 → 𝐴 : ( 0 ..^ 𝑁 ) ⟶ 𝐵 )
ply1gsumz.s ⊢ ( 𝜑 → ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = 𝑍 )
Assertion ply1gsumz ( 𝜑 → 𝐴 = ( ( 0 ..^ 𝑁 ) × { 0 } ) )

Proof

Step Hyp Ref Expression
1 ply1gsumz.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 ply1gsumz.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 ply1gsumz.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4 ply1gsumz.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 ply1gsumz.f ⊢ 𝐹 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) )
6 ply1gsumz.1 ⊢ 0 = ( 0g ‘ 𝑅 )
7 ply1gsumz.z ⊢ 𝑍 = ( 0g ‘ 𝑃 )
8 ply1gsumz.a ⊢ ( 𝜑 → 𝐴 : ( 0 ..^ 𝑁 ) ⟶ 𝐵 )
9 ply1gsumz.s ⊢ ( 𝜑 → ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = 𝑍 )
10 8 ffnd ⊢ ( 𝜑 → 𝐴 Fn ( 0 ..^ 𝑁 ) )
11 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
12 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
13 12 7 ring0cl ⊢ ( 𝑃 ∈ Ring → 𝑍 ∈ ( Base ‘ 𝑃 ) )
14 4 11 13 3syl ⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝑃 ) )
15 eqid ⊢ ( coe1 ‘ 𝑍 ) = ( coe1 ‘ 𝑍 )
16 15 12 1 2 coe1f ⊢ ( 𝑍 ∈ ( Base ‘ 𝑃 ) → ( coe1 ‘ 𝑍 ) : ℕ0 ⟶ 𝐵 )
17 14 16 syl ⊢ ( 𝜑 → ( coe1 ‘ 𝑍 ) : ℕ0 ⟶ 𝐵 )
18 17 ffnd ⊢ ( 𝜑 → ( coe1 ‘ 𝑍 ) Fn ℕ0 )
19 fzo0ssnn0 ⊢ ( 0 ..^ 𝑁 ) ⊆ ℕ0
20 19 a1i ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ⊆ ℕ0 )
21 18 20 fnssresd ⊢ ( 𝜑 → ( ( coe1 ‘ 𝑍 ) ↾ ( 0 ..^ 𝑁 ) ) Fn ( 0 ..^ 𝑁 ) )
22 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑗 ∈ ( 0 ..^ 𝑁 ) )
23 22 fvresd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( coe1 ‘ 𝑍 ) ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑗 ) = ( ( coe1 ‘ 𝑍 ) ‘ 𝑗 ) )
24 elfzonn0 ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → 𝑗 ∈ ℕ0 )
25 9 14 eqeltrd ⊢ ( 𝜑 → ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ∈ ( Base ‘ 𝑃 ) )
26 eqid ⊢ ( coe1 ‘ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) = ( coe1 ‘ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) )
27 1 12 26 15 ply1coe1eq ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ∈ ( Base ‘ 𝑃 ) ∧ 𝑍 ∈ ( Base ‘ 𝑃 ) ) → ( ∀ 𝑗 ∈ ℕ0 ( ( coe1 ‘ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) ‘ 𝑗 ) = ( ( coe1 ‘ 𝑍 ) ‘ 𝑗 ) ↔ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = 𝑍 ) )
28 27 biimpar ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ∈ ( Base ‘ 𝑃 ) ∧ 𝑍 ∈ ( Base ‘ 𝑃 ) ) ∧ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = 𝑍 ) → ∀ 𝑗 ∈ ℕ0 ( ( coe1 ‘ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) ‘ 𝑗 ) = ( ( coe1 ‘ 𝑍 ) ‘ 𝑗 ) )
29 4 25 14 9 28 syl31anc ⊢ ( 𝜑 → ∀ 𝑗 ∈ ℕ0 ( ( coe1 ‘ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) ‘ 𝑗 ) = ( ( coe1 ‘ 𝑍 ) ‘ 𝑗 ) )
30 29 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) ‘ 𝑗 ) = ( ( coe1 ‘ 𝑍 ) ‘ 𝑗 ) )
31 24 30 sylan2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) ‘ 𝑗 ) = ( ( coe1 ‘ 𝑍 ) ‘ 𝑗 ) )
32 10 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 Fn ( 0 ..^ 𝑁 ) )
33 nfv ⊢ Ⅎ 𝑛 𝜑
34 ovexd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ V )
35 33 34 5 fnmptd ⊢ ( 𝜑 → 𝐹 Fn ( 0 ..^ 𝑁 ) )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐹 Fn ( 0 ..^ 𝑁 ) )
37 ovexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 0 ..^ 𝑁 ) ∈ V )
38 inidm ⊢ ( ( 0 ..^ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 )
39 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) = ( 𝐴 ‘ 𝑖 ) )
40 oveq1 ⊢ ( 𝑛 = 𝑖 → ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) )
41 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑖 ∈ ( 0 ..^ 𝑁 ) )
42 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ V )
43 5 40 41 42 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 ‘ 𝑖 ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) )
44 32 36 37 37 38 39 43 offval ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) = ( 𝑖 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐴 ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) )
45 44 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 𝑃 Σg ( 𝑖 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐴 ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) )
46 45 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( coe1 ‘ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) = ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐴 ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) )
47 46 fveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) ‘ 𝑗 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐴 ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ‘ 𝑗 ) )
48 eqid ⊢ ( var1 ‘ 𝑅 ) = ( var1 ‘ 𝑅 )
49 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
50 4 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑅 ∈ Ring )
51 eqid ⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
52 8 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 : ( 0 ..^ 𝑁 ) ⟶ 𝐵 )
53 52 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ 𝐵 )
54 53 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝐴 ‘ 𝑖 ) ∈ 𝐵 )
55 3 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ∈ ℕ0 )
56 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐴 ‘ 𝑖 ) = ( 𝐴 ‘ 𝑗 ) )
57 1 12 48 49 50 2 51 6 54 22 55 56 gsummoncoe1fzo ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐴 ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ‘ 𝑗 ) = ( 𝐴 ‘ 𝑗 ) )
58 47 57 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) ‘ 𝑗 ) = ( 𝐴 ‘ 𝑗 ) )
59 23 31 58 3eqtr2rd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 ‘ 𝑗 ) = ( ( ( coe1 ‘ 𝑍 ) ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑗 ) )
60 10 21 59 eqfnfvd ⊢ ( 𝜑 → 𝐴 = ( ( coe1 ‘ 𝑍 ) ↾ ( 0 ..^ 𝑁 ) ) )
61 1 7 6 coe1z ⊢ ( 𝑅 ∈ Ring → ( coe1 ‘ 𝑍 ) = ( ℕ0 × { 0 } ) )
62 4 61 syl ⊢ ( 𝜑 → ( coe1 ‘ 𝑍 ) = ( ℕ0 × { 0 } ) )
63 62 reseq1d ⊢ ( 𝜑 → ( ( coe1 ‘ 𝑍 ) ↾ ( 0 ..^ 𝑁 ) ) = ( ( ℕ0 × { 0 } ) ↾ ( 0 ..^ 𝑁 ) ) )
64 60 63 eqtrd ⊢ ( 𝜑 → 𝐴 = ( ( ℕ0 × { 0 } ) ↾ ( 0 ..^ 𝑁 ) ) )
65 xpssres ⊢ ( ( 0 ..^ 𝑁 ) ⊆ ℕ0 → ( ( ℕ0 × { 0 } ) ↾ ( 0 ..^ 𝑁 ) ) = ( ( 0 ..^ 𝑁 ) × { 0 } ) )
66 19 65 ax-mp ⊢ ( ( ℕ0 × { 0 } ) ↾ ( 0 ..^ 𝑁 ) ) = ( ( 0 ..^ 𝑁 ) × { 0 } )
67 64 66 eqtrdi ⊢ ( 𝜑 → 𝐴 = ( ( 0 ..^ 𝑁 ) × { 0 } ) )