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 𝐴 = 𝐵 ) )