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	$⊢ Q = {eval}_{1} (R)$
	evl1gsummon.k	$⊢ K = {Base}_{R}$
	evl1gsummon.w	$⊢ W = {Poly}_{1} (R)$
	evl1gsummon.b	$⊢ B = {Base}_{W}$
	evl1gsummon.x	$⊢ X = {var}_{1} (R)$
	evl1gsummon.h	$⊢ H = {mulGrp}_{R}$
	evl1gsummon.e	$⊢ E = \cdot_{H}$
	evl1gsummon.g	$⊢ G = {mulGrp}_{W}$
	evl1gsummon.p	$⊢ \underset{˙}{\times} = \cdot_{G}$
	evl1gsummon.t1	$⊢ \underset{˙}{\times} = \cdot_{W}$
	evl1gsummon.t2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	evl1gsummon.r	$⊢ φ \to R \in CRing$
	evl1gsummon.a	$⊢ φ \to \forall x \in M A \in K$
	evl1gsummon.m	$⊢ φ \to M \subseteq ℕ_{0}$
	evl1gsummon.f	$⊢ φ \to M \in Fin$
	evl1gsummon.n	$⊢ φ \to \forall x \in M N \in ℕ_{0}$
	evl1gsummon.c	$⊢ φ \to C \in K$
Assertion	evl1gsummon	$⊢ φ \to Q (\underset{x \in M}{\sum_{W}} (A \underset{˙}{\times} (N \underset{˙}{\times} X))) (C) = \underset{x \in M}{\sum_{R}} (A \underset{˙}{\cdot} (N E C))$

Proof

Step	Hyp	Ref	Expression
1		evl1gsummon.q	$⊢ Q = {eval}_{1} (R)$
2		evl1gsummon.k	$⊢ K = {Base}_{R}$
3		evl1gsummon.w	$⊢ W = {Poly}_{1} (R)$
4		evl1gsummon.b	$⊢ B = {Base}_{W}$
5		evl1gsummon.x	$⊢ X = {var}_{1} (R)$
6		evl1gsummon.h	$⊢ H = {mulGrp}_{R}$
7		evl1gsummon.e	$⊢ E = \cdot_{H}$
8		evl1gsummon.g	$⊢ G = {mulGrp}_{W}$
9		evl1gsummon.p	$⊢ \underset{˙}{\times} = \cdot_{G}$
10		evl1gsummon.t1	$⊢ \underset{˙}{\times} = \cdot_{W}$
11		evl1gsummon.t2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
12		evl1gsummon.r	$⊢ φ \to R \in CRing$
13		evl1gsummon.a	$⊢ φ \to \forall x \in M A \in K$
14		evl1gsummon.m	$⊢ φ \to M \subseteq ℕ_{0}$
15		evl1gsummon.f	$⊢ φ \to M \in Fin$
16		evl1gsummon.n	$⊢ φ \to \forall x \in M N \in ℕ_{0}$
17		evl1gsummon.c	$⊢ φ \to C \in K$
18		eqid	$⊢ R ↑_{𝑠} K = R ↑_{𝑠} K$
19		crngring	$⊢ R \in CRing \to R \in Ring$
20	12 19	syl	$⊢ φ \to R \in Ring$
21	3	ply1lmod	$⊢ R \in Ring \to W \in LMod$
22	20 21	syl	$⊢ φ \to W \in LMod$
23	22	adantr	$⊢ (φ \land x \in M) \to W \in LMod$
24	13	r19.21bi	$⊢ (φ \land x \in M) \to A \in K$
25	3	ply1sca	$⊢ R \in CRing \to R = Scalar (W)$
26	12 25	syl	$⊢ φ \to R = Scalar (W)$
27	26	fveq2d	$⊢ φ \to {Base}_{R} = {Base}_{Scalar (W)}$
28	2 27	eqtrid	$⊢ φ \to K = {Base}_{Scalar (W)}$
29	28	adantr	$⊢ (φ \land x \in M) \to K = {Base}_{Scalar (W)}$
30	24 29	eleqtrd	$⊢ (φ \land x \in M) \to A \in {Base}_{Scalar (W)}$
31	8 4	mgpbas	$⊢ B = {Base}_{G}$
32	3	ply1ring	$⊢ R \in Ring \to W \in Ring$
33	20 32	syl	$⊢ φ \to W \in Ring$
34	8	ringmgp	$⊢ W \in Ring \to G \in Mnd$
35	33 34	syl	$⊢ φ \to G \in Mnd$
36	35	adantr	$⊢ (φ \land x \in M) \to G \in Mnd$
37	16	r19.21bi	$⊢ (φ \land x \in M) \to N \in ℕ_{0}$
38	20	adantr	$⊢ (φ \land x \in M) \to R \in Ring$
39	5 3 4	vr1cl	$⊢ R \in Ring \to X \in B$
40	38 39	syl	$⊢ (φ \land x \in M) \to X \in B$
41	31 9 36 37 40	mulgnn0cld	$⊢ (φ \land x \in M) \to N \underset{˙}{\times} X \in B$
42		eqid	$⊢ Scalar (W) = Scalar (W)$
43		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
44	4 42 10 43	lmodvscl	$⊢ (W \in LMod \land A \in {Base}_{Scalar (W)} \land N \underset{˙}{\times} X \in B) \to A \underset{˙}{\times} (N \underset{˙}{\times} X) \in B$
45	23 30 41 44	syl3anc	$⊢ (φ \land x \in M) \to A \underset{˙}{\times} (N \underset{˙}{\times} X) \in B$
46	1 2 3 18 4 12 45 14 15 17	evl1gsumaddval	$⊢ φ \to Q (\underset{x \in M}{\sum_{W}} (A \underset{˙}{\times} (N \underset{˙}{\times} X))) (C) = \underset{x \in M}{\sum_{R}} Q (A \underset{˙}{\times} (N \underset{˙}{\times} X)) (C)$
47	12	adantr	$⊢ (φ \land x \in M) \to R \in CRing$
48	17	adantr	$⊢ (φ \land x \in M) \to C \in K$
49	1 3 8 5 2 9 47 37 10 24 48 6 7 11	evl1scvarpwval	$⊢ (φ \land x \in M) \to Q (A \underset{˙}{\times} (N \underset{˙}{\times} X)) (C) = A \underset{˙}{\cdot} (N E C)$
50	49	mpteq2dva	$⊢ φ \to (x \in M ⟼ Q (A \underset{˙}{\times} (N \underset{˙}{\times} X)) (C)) = (x \in M ⟼ A \underset{˙}{\cdot} (N E C))$
51	50	oveq2d	$⊢ φ \to \underset{x \in M}{\sum_{R}} Q (A \underset{˙}{\times} (N \underset{˙}{\times} X)) (C) = \underset{x \in M}{\sum_{R}} (A \underset{˙}{\cdot} (N E C))$
52	46 51	eqtrd	$⊢ φ \to Q (\underset{x \in M}{\sum_{W}} (A \underset{˙}{\times} (N \underset{˙}{\times} X))) (C) = \underset{x \in M}{\sum_{R}} (A \underset{˙}{\cdot} (N E C))$

Metamath Proof Explorer

Theorem evl1gsummon

Proof