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

Metamath Proof Explorer

Theorem gsumply1eq

Description: Two univariate polynomials given as (finitely supported) sum of scaled monomials are equal iff the corresponding coefficients are equal. (Contributed by AV, 21-Nov-2019)

Ref Expression
Hypotheses gsumply1eq.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
gsumply1eq.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
gsumply1eq.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
gsumply1eq.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
gsumply1eq.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
gsumply1eq.m ⊢ ∗ = ( ·𝑠 ‘ 𝑃 )
gsumply1eq.0 ⊢ 0 = ( 0g ‘ 𝑅 )
gsumply1eq.a ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐴 ∈ 𝐾 )
gsumply1eq.f1 ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) finSupp 0 )
gsumply1eq.b ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐵 ∈ 𝐾 )
gsumply1eq.f2 ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐵 ) finSupp 0 )
gsumply1eq.o ⊢ ( 𝜑 → 𝑂 = ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
gsumply1eq.q ⊢ ( 𝜑 → 𝑄 = ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐵 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
Assertion gsumply1eq ( 𝜑 → ( 𝑂 = 𝑄 ↔ ∀ 𝑘 ∈ ℕ0 𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 gsumply1eq.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 gsumply1eq.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
3 gsumply1eq.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
4 gsumply1eq.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 gsumply1eq.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
6 gsumply1eq.m ⊢ ∗ = ( ·𝑠 ‘ 𝑃 )
7 gsumply1eq.0 ⊢ 0 = ( 0g ‘ 𝑅 )
8 gsumply1eq.a ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐴 ∈ 𝐾 )
9 gsumply1eq.f1 ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) finSupp 0 )
10 gsumply1eq.b ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐵 ∈ 𝐾 )
11 gsumply1eq.f2 ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐵 ) finSupp 0 )
12 gsumply1eq.o ⊢ ( 𝜑 → 𝑂 = ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
13 gsumply1eq.q ⊢ ( 𝜑 → 𝑄 = ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐵 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
14 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
15 1 14 2 3 4 5 6 7 8 9 gsumsmonply1 ⊢ ( 𝜑 → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ∈ ( Base ‘ 𝑃 ) )
16 12 15 eqeltrd ⊢ ( 𝜑 → 𝑂 ∈ ( Base ‘ 𝑃 ) )
17 1 14 2 3 4 5 6 7 10 11 gsumsmonply1 ⊢ ( 𝜑 → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐵 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ∈ ( Base ‘ 𝑃 ) )
18 13 17 eqeltrd ⊢ ( 𝜑 → 𝑄 ∈ ( Base ‘ 𝑃 ) )
19 eqid ⊢ ( coe1 ‘ 𝑂 ) = ( coe1 ‘ 𝑂 )
20 eqid ⊢ ( coe1 ‘ 𝑄 ) = ( coe1 ‘ 𝑄 )
21 1 14 19 20 ply1coe1eq ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑂 ∈ ( Base ‘ 𝑃 ) ∧ 𝑄 ∈ ( Base ‘ 𝑃 ) ) → ( ∀ 𝑘 ∈ ℕ0 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) = ( ( coe1 ‘ 𝑄 ) ‘ 𝑘 ) ↔ 𝑂 = 𝑄 ) )
22 21 bicomd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑂 ∈ ( Base ‘ 𝑃 ) ∧ 𝑄 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑂 = 𝑄 ↔ ∀ 𝑘 ∈ ℕ0 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) = ( ( coe1 ‘ 𝑄 ) ‘ 𝑘 ) ) )
23 4 16 18 22 syl3anc ⊢ ( 𝜑 → ( 𝑂 = 𝑄 ↔ ∀ 𝑘 ∈ ℕ0 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) = ( ( coe1 ‘ 𝑄 ) ‘ 𝑘 ) ) )
24 12 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑂 = ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
25 nfcv ⊢ Ⅎ 𝑙 ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) )
26 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑙 / 𝑘 ⦌ 𝐴
27 nfcv ⊢ Ⅎ 𝑘 ∗
28 nfcv ⊢ Ⅎ 𝑘 ( 𝑙 ↑ 𝑋 )
29 26 27 28 nfov ⊢ Ⅎ 𝑘 ( ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∗ ( 𝑙 ↑ 𝑋 ) )
30 csbeq1a ⊢ ( 𝑘 = 𝑙 → 𝐴 = ⦋ 𝑙 / 𝑘 ⦌ 𝐴 )
31 oveq1 ⊢ ( 𝑘 = 𝑙 → ( 𝑘 ↑ 𝑋 ) = ( 𝑙 ↑ 𝑋 ) )
32 30 31 oveq12d ⊢ ( 𝑘 = 𝑙 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∗ ( 𝑙 ↑ 𝑋 ) ) )
33 25 29 32 cbvmpt ⊢ ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∗ ( 𝑙 ↑ 𝑋 ) ) )
34 33 oveq2i ⊢ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∗ ( 𝑙 ↑ 𝑋 ) ) ) )
35 24 34 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑂 = ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∗ ( 𝑙 ↑ 𝑋 ) ) ) ) )
36 35 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( coe1 ‘ 𝑂 ) = ( coe1 ‘ ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∗ ( 𝑙 ↑ 𝑋 ) ) ) ) ) )
37 36 fveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∗ ( 𝑙 ↑ 𝑋 ) ) ) ) ) ‘ 𝑘 ) )
38 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑅 ∈ Ring )
39 nfv ⊢ Ⅎ 𝑙 𝐴 ∈ 𝐾
40 26 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∈ 𝐾
41 30 eleq1d ⊢ ( 𝑘 = 𝑙 → ( 𝐴 ∈ 𝐾 ↔ ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∈ 𝐾 ) )
42 39 40 41 cbvralw ⊢ ( ∀ 𝑘 ∈ ℕ0 𝐴 ∈ 𝐾 ↔ ∀ 𝑙 ∈ ℕ0 ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∈ 𝐾 )
43 8 42 sylib ⊢ ( 𝜑 → ∀ 𝑙 ∈ ℕ0 ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∈ 𝐾 )
44 43 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ∀ 𝑙 ∈ ℕ0 ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∈ 𝐾 )
45 nfcv ⊢ Ⅎ 𝑙 𝐴
46 45 26 30 cbvmpt ⊢ ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) = ( 𝑙 ∈ ℕ0 ↦ ⦋ 𝑙 / 𝑘 ⦌ 𝐴 )
47 46 9 eqbrtrrid ⊢ ( 𝜑 → ( 𝑙 ∈ ℕ0 ↦ ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ) finSupp 0 )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑙 ∈ ℕ0 ↦ ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ) finSupp 0 )
49 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
50 1 14 2 3 38 5 6 7 44 48 49 gsummoncoe1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∗ ( 𝑙 ↑ 𝑋 ) ) ) ) ) ‘ 𝑘 ) = ⦋ 𝑘 / 𝑙 ⦌ ⦋ 𝑙 / 𝑘 ⦌ 𝐴 )
51 csbcow ⊢ ⦋ 𝑘 / 𝑙 ⦌ ⦋ 𝑙 / 𝑘 ⦌ 𝐴 = ⦋ 𝑘 / 𝑘 ⦌ 𝐴
52 csbid ⊢ ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 𝐴
53 51 52 eqtri ⊢ ⦋ 𝑘 / 𝑙 ⦌ ⦋ 𝑙 / 𝑘 ⦌ 𝐴 = 𝐴
54 50 53 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∗ ( 𝑙 ↑ 𝑋 ) ) ) ) ) ‘ 𝑘 ) = 𝐴 )
55 37 54 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) = 𝐴 )
56 13 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑄 = ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐵 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
57 nfcv ⊢ Ⅎ 𝑙 ( 𝐵 ∗ ( 𝑘 ↑ 𝑋 ) )
58 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑙 / 𝑘 ⦌ 𝐵
59 58 27 28 nfov ⊢ Ⅎ 𝑘 ( ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∗ ( 𝑙 ↑ 𝑋 ) )
60 csbeq1a ⊢ ( 𝑘 = 𝑙 → 𝐵 = ⦋ 𝑙 / 𝑘 ⦌ 𝐵 )
61 60 31 oveq12d ⊢ ( 𝑘 = 𝑙 → ( 𝐵 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∗ ( 𝑙 ↑ 𝑋 ) ) )
62 57 59 61 cbvmpt ⊢ ( 𝑘 ∈ ℕ0 ↦ ( 𝐵 ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∗ ( 𝑙 ↑ 𝑋 ) ) )
63 62 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝐵 ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∗ ( 𝑙 ↑ 𝑋 ) ) ) )
64 63 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐵 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∗ ( 𝑙 ↑ 𝑋 ) ) ) ) )
65 56 64 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑄 = ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∗ ( 𝑙 ↑ 𝑋 ) ) ) ) )
66 65 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( coe1 ‘ 𝑄 ) = ( coe1 ‘ ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∗ ( 𝑙 ↑ 𝑋 ) ) ) ) ) )
67 66 fveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑄 ) ‘ 𝑘 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∗ ( 𝑙 ↑ 𝑋 ) ) ) ) ) ‘ 𝑘 ) )
68 nfv ⊢ Ⅎ 𝑙 𝐵 ∈ 𝐾
69 58 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∈ 𝐾
70 60 eleq1d ⊢ ( 𝑘 = 𝑙 → ( 𝐵 ∈ 𝐾 ↔ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∈ 𝐾 ) )
71 68 69 70 cbvralw ⊢ ( ∀ 𝑘 ∈ ℕ0 𝐵 ∈ 𝐾 ↔ ∀ 𝑙 ∈ ℕ0 ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∈ 𝐾 )
72 10 71 sylib ⊢ ( 𝜑 → ∀ 𝑙 ∈ ℕ0 ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∈ 𝐾 )
73 72 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ∀ 𝑙 ∈ ℕ0 ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∈ 𝐾 )
74 nfcv ⊢ Ⅎ 𝑙 𝐵
75 74 58 60 cbvmpt ⊢ ( 𝑘 ∈ ℕ0 ↦ 𝐵 ) = ( 𝑙 ∈ ℕ0 ↦ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 )
76 75 11 eqbrtrrid ⊢ ( 𝜑 → ( 𝑙 ∈ ℕ0 ↦ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) finSupp 0 )
77 76 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑙 ∈ ℕ0 ↦ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) finSupp 0 )
78 1 14 2 3 38 5 6 7 73 77 49 gsummoncoe1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∗ ( 𝑙 ↑ 𝑋 ) ) ) ) ) ‘ 𝑘 ) = ⦋ 𝑘 / 𝑙 ⦌ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 )
79 csbcow ⊢ ⦋ 𝑘 / 𝑙 ⦌ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 = ⦋ 𝑘 / 𝑘 ⦌ 𝐵
80 csbid ⊢ ⦋ 𝑘 / 𝑘 ⦌ 𝐵 = 𝐵
81 79 80 eqtri ⊢ ⦋ 𝑘 / 𝑙 ⦌ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 = 𝐵
82 78 81 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∗ ( 𝑙 ↑ 𝑋 ) ) ) ) ) ‘ 𝑘 ) = 𝐵 )
83 67 82 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑄 ) ‘ 𝑘 ) = 𝐵 )
84 55 83 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) = ( ( coe1 ‘ 𝑄 ) ‘ 𝑘 ) ↔ 𝐴 = 𝐵 ) )
85 84 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ℕ0 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) = ( ( coe1 ‘ 𝑄 ) ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ ℕ0 𝐴 = 𝐵 ) )
86 23 85 bitrd ⊢ ( 𝜑 → ( 𝑂 = 𝑄 ↔ ∀ 𝑘 ∈ ℕ0 𝐴 = 𝐵 ) )