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

Metamath Proof Explorer

Theorem evl1gsummul

Description: Univariate polynomial evaluation maps (multiplicative) group sums to group sums. (Contributed by AV, 15-Sep-2019)

Ref Expression
Hypotheses evl1gsumadd.q ⊢ Q = eval 1 ⁡ R
evl1gsumadd.k ⊢ K = Base R
evl1gsumadd.w ⊢ W = Poly 1 ⁡ R
evl1gsumadd.p ⊢ P = R ↑ 𝑠 K
evl1gsumadd.b ⊢ B = Base W
evl1gsumadd.r ⊢ φ → R ∈ CRing
evl1gsumadd.y ⊢ φ ∧ x ∈ N → Y ∈ B
evl1gsumadd.n ⊢ φ → N ⊆ ℕ 0
evl1gsummul.1 ⊢ 1 ˙ = 1 W
evl1gsummul.g ⊢ G = mulGrp W
evl1gsummul.h ⊢ H = mulGrp P
evl1gsummul.f ⊢ φ → finSupp 1 ˙⁡ x ∈ N ⟼ Y
Assertion evl1gsummul ⊢ φ → Q ⁡ ∑ G x ∈ N Y = ∑ H x ∈ N Q ⁡ Y

Proof

Step Hyp Ref Expression
1 evl1gsumadd.q ⊢ Q = eval 1 ⁡ R
2 evl1gsumadd.k ⊢ K = Base R
3 evl1gsumadd.w ⊢ W = Poly 1 ⁡ R
4 evl1gsumadd.p ⊢ P = R ↑ 𝑠 K
5 evl1gsumadd.b ⊢ B = Base W
6 evl1gsumadd.r ⊢ φ → R ∈ CRing
7 evl1gsumadd.y ⊢ φ ∧ x ∈ N → Y ∈ B
8 evl1gsumadd.n ⊢ φ → N ⊆ ℕ 0
9 evl1gsummul.1 ⊢ 1 ˙ = 1 W
10 evl1gsummul.g ⊢ G = mulGrp W
11 evl1gsummul.h ⊢ H = mulGrp P
12 evl1gsummul.f ⊢ φ → finSupp 1 ˙⁡ x ∈ N ⟼ Y
13 10 5 mgpbas ⊢ B = Base G
14 10 9 ringidval ⊢ 1 ˙ = 0 G
15 3 ply1crng ⊢ R ∈ CRing → W ∈ CRing
16 10 crngmgp ⊢ W ∈ CRing → G ∈ CMnd
17 6 15 16 3syl ⊢ φ → G ∈ CMnd
18 crngring ⊢ R ∈ CRing → R ∈ Ring
19 6 18 syl ⊢ φ → R ∈ Ring
20 2 fvexi ⊢ K ∈ V
21 19 20 jctir ⊢ φ → R ∈ Ring ∧ K ∈ V
22 4 pwsring ⊢ R ∈ Ring ∧ K ∈ V → P ∈ Ring
23 11 ringmgp ⊢ P ∈ Ring → H ∈ Mnd
24 21 22 23 3syl ⊢ φ → H ∈ Mnd
25 nn0ex ⊢ ℕ 0 ∈ V
26 25 a1i ⊢ φ → ℕ 0 ∈ V
27 26 8 ssexd ⊢ φ → N ∈ V
28 1 3 4 2 evl1rhm ⊢ R ∈ CRing → Q ∈ W RingHom P
29 10 11 rhmmhm ⊢ Q ∈ W RingHom P → Q ∈ G MndHom H
30 6 28 29 3syl ⊢ φ → Q ∈ G MndHom H
31 13 14 17 24 27 30 7 12 gsummptmhm ⊢ φ → ∑ H x ∈ N Q ⁡ Y = Q ⁡ ∑ G x ∈ N Y
32 31 eqcomd ⊢ φ → Q ⁡ ∑ G x ∈ N Y = ∑ H x ∈ N Q ⁡ Y