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

Metamath Proof Explorer

Theorem evl1gsummon

Description: Value of a univariate polynomial evaluation mapping an additive group sum of a multiple of an exponentiation of a variable to a group sum of the multiple of the exponentiation of the evaluated variable. (Contributed by AV, 18-Sep-2019)

Ref Expression
Hypotheses evl1gsummon.q ⊢ 𝑄 = ( eval1 ‘ 𝑅 )
evl1gsummon.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
evl1gsummon.w ⊢ 𝑊 = ( Poly1 ‘ 𝑅 )
evl1gsummon.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
evl1gsummon.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
evl1gsummon.h ⊢ 𝐻 = ( mulGrp ‘ 𝑅 )
evl1gsummon.e ⊢ 𝐸 = ( .g ‘ 𝐻 )
evl1gsummon.g ⊢ 𝐺 = ( mulGrp ‘ 𝑊 )
evl1gsummon.p ⊢ ↑ = ( .g ‘ 𝐺 )
evl1gsummon.t1 ⊢ × = ( ·𝑠 ‘ 𝑊 )
evl1gsummon.t2 ⊢ · = ( .r ‘ 𝑅 )
evl1gsummon.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
evl1gsummon.a ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑀 𝐴 ∈ 𝐾 )
evl1gsummon.m ⊢ ( 𝜑 → 𝑀 ⊆ ℕ0 )
evl1gsummon.f ⊢ ( 𝜑 → 𝑀 ∈ Fin )
evl1gsummon.n ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑀 𝑁 ∈ ℕ0 )
evl1gsummon.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
Assertion evl1gsummon ( 𝜑 → ( ( 𝑄 ‘ ( 𝑊 Σg ( 𝑥 ∈ 𝑀 ↦ ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ) ) ) ‘ 𝐶 ) = ( 𝑅 Σg ( 𝑥 ∈ 𝑀 ↦ ( 𝐴 · ( 𝑁 𝐸 𝐶 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 evl1gsummon.q ⊢ 𝑄 = ( eval1 ‘ 𝑅 )
2 evl1gsummon.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
3 evl1gsummon.w ⊢ 𝑊 = ( Poly1 ‘ 𝑅 )
4 evl1gsummon.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
5 evl1gsummon.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
6 evl1gsummon.h ⊢ 𝐻 = ( mulGrp ‘ 𝑅 )
7 evl1gsummon.e ⊢ 𝐸 = ( .g ‘ 𝐻 )
8 evl1gsummon.g ⊢ 𝐺 = ( mulGrp ‘ 𝑊 )
9 evl1gsummon.p ⊢ ↑ = ( .g ‘ 𝐺 )
10 evl1gsummon.t1 ⊢ × = ( ·𝑠 ‘ 𝑊 )
11 evl1gsummon.t2 ⊢ · = ( .r ‘ 𝑅 )
12 evl1gsummon.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
13 evl1gsummon.a ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑀 𝐴 ∈ 𝐾 )
14 evl1gsummon.m ⊢ ( 𝜑 → 𝑀 ⊆ ℕ0 )
15 evl1gsummon.f ⊢ ( 𝜑 → 𝑀 ∈ Fin )
16 evl1gsummon.n ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑀 𝑁 ∈ ℕ0 )
17 evl1gsummon.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
18 eqid ⊢ ( 𝑅 ↑s 𝐾 ) = ( 𝑅 ↑s 𝐾 )
19 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
20 12 19 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
21 3 ply1lmod ⊢ ( 𝑅 ∈ Ring → 𝑊 ∈ LMod )
22 20 21 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝑊 ∈ LMod )
24 13 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝐴 ∈ 𝐾 )
25 3 ply1sca ⊢ ( 𝑅 ∈ CRing → 𝑅 = ( Scalar ‘ 𝑊 ) )
26 12 25 syl ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑊 ) )
27 26 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
28 2 27 eqtrid ⊢ ( 𝜑 → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
30 24 29 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
31 8 4 mgpbas ⊢ 𝐵 = ( Base ‘ 𝐺 )
32 3 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑊 ∈ Ring )
33 20 32 syl ⊢ ( 𝜑 → 𝑊 ∈ Ring )
34 8 ringmgp ⊢ ( 𝑊 ∈ Ring → 𝐺 ∈ Mnd )
35 33 34 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝐺 ∈ Mnd )
37 16 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝑁 ∈ ℕ0 )
38 20 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝑅 ∈ Ring )
39 5 3 4 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )
40 38 39 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝑋 ∈ 𝐵 )
41 31 9 36 37 40 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → ( 𝑁 ↑ 𝑋 ) ∈ 𝐵 )
42 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
43 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
44 4 42 10 43 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑁 ↑ 𝑋 ) ∈ 𝐵 ) → ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ∈ 𝐵 )
45 23 30 41 44 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ∈ 𝐵 )
46 1 2 3 18 4 12 45 14 15 17 evl1gsumaddval ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑊 Σg ( 𝑥 ∈ 𝑀 ↦ ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ) ) ) ‘ 𝐶 ) = ( 𝑅 Σg ( 𝑥 ∈ 𝑀 ↦ ( ( 𝑄 ‘ ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ) ‘ 𝐶 ) ) ) )
47 12 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝑅 ∈ CRing )
48 17 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝐶 ∈ 𝐾 )
49 1 3 8 5 2 9 47 37 10 24 48 6 7 11 evl1scvarpwval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → ( ( 𝑄 ‘ ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ) ‘ 𝐶 ) = ( 𝐴 · ( 𝑁 𝐸 𝐶 ) ) )
50 49 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑀 ↦ ( ( 𝑄 ‘ ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ) ‘ 𝐶 ) ) = ( 𝑥 ∈ 𝑀 ↦ ( 𝐴 · ( 𝑁 𝐸 𝐶 ) ) ) )
51 50 oveq2d ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑥 ∈ 𝑀 ↦ ( ( 𝑄 ‘ ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ) ‘ 𝐶 ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ 𝑀 ↦ ( 𝐴 · ( 𝑁 𝐸 𝐶 ) ) ) ) )
52 46 51 eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑊 Σg ( 𝑥 ∈ 𝑀 ↦ ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ) ) ) ‘ 𝐶 ) = ( 𝑅 Σg ( 𝑥 ∈ 𝑀 ↦ ( 𝐴 · ( 𝑁 𝐸 𝐶 ) ) ) ) )