evl1gsumd

Description: Polynomial evaluation builder for a finite group sum of polynomials. (Contributed by AV, 17-Sep-2019)

	Ref	Expression
Hypotheses	evl1gsumd.q	$⊢ O = {eval}_{1} (R)$
	evl1gsumd.p	$⊢ P = {Poly}_{1} (R)$
	evl1gsumd.b	$⊢ B = {Base}_{R}$
	evl1gsumd.u	$⊢ U = {Base}_{P}$
	evl1gsumd.r	$⊢ φ \to R \in CRing$
	evl1gsumd.y	$⊢ φ \to Y \in B$
	evl1gsumd.m	$⊢ φ \to \forall x \in N M \in U$
	evl1gsumd.n	$⊢ φ \to N \in Fin$
Assertion	evl1gsumd	$⊢ φ \to O (\underset{x \in N}{\sum_{P}} M) (Y) = \underset{x \in N}{\sum_{R}} O (M) (Y)$

Proof

Step	Hyp	Ref	Expression
1		evl1gsumd.q	$⊢ O = {eval}_{1} (R)$
2		evl1gsumd.p	$⊢ P = {Poly}_{1} (R)$
3		evl1gsumd.b	$⊢ B = {Base}_{R}$
4		evl1gsumd.u	$⊢ U = {Base}_{P}$
5		evl1gsumd.r	$⊢ φ \to R \in CRing$
6		evl1gsumd.y	$⊢ φ \to Y \in B$
7		evl1gsumd.m	$⊢ φ \to \forall x \in N M \in U$
8		evl1gsumd.n	$⊢ φ \to N \in Fin$
9		raleq	$⊢ n = \emptyset \to (\forall x \in n M \in U \leftrightarrow \forall x \in \emptyset M \in U)$
10	9	anbi2d	$⊢ n = \emptyset \to ((φ \land \forall x \in n M \in U) \leftrightarrow (φ \land \forall x \in \emptyset M \in U))$
11		mpteq1	$⊢ n = \emptyset \to (x \in n ⟼ M) = (x \in \emptyset ⟼ M)$
12	11	oveq2d	$⊢ n = \emptyset \to \underset{x \in n}{\sum_{P}} M = \underset{x \in \emptyset}{\sum_{P}} M$
13	12	fveq2d	$⊢ n = \emptyset \to O (\underset{x \in n}{\sum_{P}} M) = O (\underset{x \in \emptyset}{\sum_{P}} M)$
14	13	fveq1d	$⊢ n = \emptyset \to O (\underset{x \in n}{\sum_{P}} M) (Y) = O (\underset{x \in \emptyset}{\sum_{P}} M) (Y)$
15		mpteq1	$⊢ n = \emptyset \to (x \in n ⟼ O (M) (Y)) = (x \in \emptyset ⟼ O (M) (Y))$
16	15	oveq2d	$⊢ n = \emptyset \to \underset{x \in n}{\sum_{R}} O (M) (Y) = \underset{x \in \emptyset}{\sum_{R}} O (M) (Y)$
17	14 16	eqeq12d	$⊢ n = \emptyset \to (O (\underset{x \in n}{\sum_{P}} M) (Y) = \underset{x \in n}{\sum_{R}} O (M) (Y) \leftrightarrow O (\underset{x \in \emptyset}{\sum_{P}} M) (Y) = \underset{x \in \emptyset}{\sum_{R}} O (M) (Y))$
18	10 17	imbi12d	$⊢ n = \emptyset \to (((φ \land \forall x \in n M \in U) \to O (\underset{x \in n}{\sum_{P}} M) (Y) = \underset{x \in n}{\sum_{R}} O (M) (Y)) \leftrightarrow ((φ \land \forall x \in \emptyset M \in U) \to O (\underset{x \in \emptyset}{\sum_{P}} M) (Y) = \underset{x \in \emptyset}{\sum_{R}} O (M) (Y)))$
19		raleq	$⊢ n = m \to (\forall x \in n M \in U \leftrightarrow \forall x \in m M \in U)$
20	19	anbi2d	$⊢ n = m \to ((φ \land \forall x \in n M \in U) \leftrightarrow (φ \land \forall x \in m M \in U))$
21		mpteq1	$⊢ n = m \to (x \in n ⟼ M) = (x \in m ⟼ M)$
22	21	oveq2d	$⊢ n = m \to \underset{x \in n}{\sum_{P}} M = \underset{x \in m}{\sum_{P}} M$
23	22	fveq2d	$⊢ n = m \to O (\underset{x \in n}{\sum_{P}} M) = O (\underset{x \in m}{\sum_{P}} M)$
24	23	fveq1d	$⊢ n = m \to O (\underset{x \in n}{\sum_{P}} M) (Y) = O (\underset{x \in m}{\sum_{P}} M) (Y)$
25		mpteq1	$⊢ n = m \to (x \in n ⟼ O (M) (Y)) = (x \in m ⟼ O (M) (Y))$
26	25	oveq2d	$⊢ n = m \to \underset{x \in n}{\sum_{R}} O (M) (Y) = \underset{x \in m}{\sum_{R}} O (M) (Y)$
27	24 26	eqeq12d	$⊢ n = m \to (O (\underset{x \in n}{\sum_{P}} M) (Y) = \underset{x \in n}{\sum_{R}} O (M) (Y) \leftrightarrow O (\underset{x \in m}{\sum_{P}} M) (Y) = \underset{x \in m}{\sum_{R}} O (M) (Y))$
28	20 27	imbi12d	$⊢ n = m \to (((φ \land \forall x \in n M \in U) \to O (\underset{x \in n}{\sum_{P}} M) (Y) = \underset{x \in n}{\sum_{R}} O (M) (Y)) \leftrightarrow ((φ \land \forall x \in m M \in U) \to O (\underset{x \in m}{\sum_{P}} M) (Y) = \underset{x \in m}{\sum_{R}} O (M) (Y)))$
29		raleq	$⊢ n = m \cup \{a\} \to (\forall x \in n M \in U \leftrightarrow \forall x \in (m \cup \{a\}) M \in U)$
30	29	anbi2d	$⊢ n = m \cup \{a\} \to ((φ \land \forall x \in n M \in U) \leftrightarrow (φ \land \forall x \in (m \cup \{a\}) M \in U))$
31		mpteq1	$⊢ n = m \cup \{a\} \to (x \in n ⟼ M) = (x \in (m \cup \{a\}) ⟼ M)$
32	31	oveq2d	$⊢ n = m \cup \{a\} \to \underset{x \in n}{\sum_{P}} M = \underset{x \in m \cup \{a\}}{\sum_{P}} M$
33	32	fveq2d	$⊢ n = m \cup \{a\} \to O (\underset{x \in n}{\sum_{P}} M) = O (\underset{x \in m \cup \{a\}}{\sum_{P}} M)$
34	33	fveq1d	$⊢ n = m \cup \{a\} \to O (\underset{x \in n}{\sum_{P}} M) (Y) = O (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (Y)$
35		mpteq1	$⊢ n = m \cup \{a\} \to (x \in n ⟼ O (M) (Y)) = (x \in (m \cup \{a\}) ⟼ O (M) (Y))$
36	35	oveq2d	$⊢ n = m \cup \{a\} \to \underset{x \in n}{\sum_{R}} O (M) (Y) = \underset{x \in m \cup \{a\}}{\sum_{R}} O (M) (Y)$
37	34 36	eqeq12d	$⊢ n = m \cup \{a\} \to (O (\underset{x \in n}{\sum_{P}} M) (Y) = \underset{x \in n}{\sum_{R}} O (M) (Y) \leftrightarrow O (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (Y) = \underset{x \in m \cup \{a\}}{\sum_{R}} O (M) (Y))$
38	30 37	imbi12d	$⊢ n = m \cup \{a\} \to (((φ \land \forall x \in n M \in U) \to O (\underset{x \in n}{\sum_{P}} M) (Y) = \underset{x \in n}{\sum_{R}} O (M) (Y)) \leftrightarrow ((φ \land \forall x \in (m \cup \{a\}) M \in U) \to O (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (Y) = \underset{x \in m \cup \{a\}}{\sum_{R}} O (M) (Y)))$
39		raleq	$⊢ n = N \to (\forall x \in n M \in U \leftrightarrow \forall x \in N M \in U)$
40	39	anbi2d	$⊢ n = N \to ((φ \land \forall x \in n M \in U) \leftrightarrow (φ \land \forall x \in N M \in U))$
41		mpteq1	$⊢ n = N \to (x \in n ⟼ M) = (x \in N ⟼ M)$
42	41	oveq2d	$⊢ n = N \to \underset{x \in n}{\sum_{P}} M = \underset{x \in N}{\sum_{P}} M$
43	42	fveq2d	$⊢ n = N \to O (\underset{x \in n}{\sum_{P}} M) = O (\underset{x \in N}{\sum_{P}} M)$
44	43	fveq1d	$⊢ n = N \to O (\underset{x \in n}{\sum_{P}} M) (Y) = O (\underset{x \in N}{\sum_{P}} M) (Y)$
45		mpteq1	$⊢ n = N \to (x \in n ⟼ O (M) (Y)) = (x \in N ⟼ O (M) (Y))$
46	45	oveq2d	$⊢ n = N \to \underset{x \in n}{\sum_{R}} O (M) (Y) = \underset{x \in N}{\sum_{R}} O (M) (Y)$
47	44 46	eqeq12d	$⊢ n = N \to (O (\underset{x \in n}{\sum_{P}} M) (Y) = \underset{x \in n}{\sum_{R}} O (M) (Y) \leftrightarrow O (\underset{x \in N}{\sum_{P}} M) (Y) = \underset{x \in N}{\sum_{R}} O (M) (Y))$
48	40 47	imbi12d	$⊢ n = N \to (((φ \land \forall x \in n M \in U) \to O (\underset{x \in n}{\sum_{P}} M) (Y) = \underset{x \in n}{\sum_{R}} O (M) (Y)) \leftrightarrow ((φ \land \forall x \in N M \in U) \to O (\underset{x \in N}{\sum_{P}} M) (Y) = \underset{x \in N}{\sum_{R}} O (M) (Y)))$
49		mpt0	$⊢ (x \in \emptyset ⟼ M) = \emptyset$
50	49	oveq2i	$⊢ \underset{x \in \emptyset}{\sum_{P}} M = \sum_{P} \emptyset$
51		eqid	$⊢ 0_{P} = 0_{P}$
52	51	gsum0	$⊢ \sum_{P} \emptyset = 0_{P}$
53	50 52	eqtri	$⊢ \underset{x \in \emptyset}{\sum_{P}} M = 0_{P}$
54	53	fveq2i	$⊢ O (\underset{x \in \emptyset}{\sum_{P}} M) = O (0_{P})$
55		crngring	$⊢ R \in CRing \to R \in Ring$
56	5 55	syl	$⊢ φ \to R \in Ring$
57		eqid	$⊢ algSc (P) = algSc (P)$
58		eqid	$⊢ 0_{R} = 0_{R}$
59	2 57 58 51	ply1scl0	$⊢ R \in Ring \to algSc (P) (0_{R}) = 0_{P}$
60	56 59	syl	$⊢ φ \to algSc (P) (0_{R}) = 0_{P}$
61	60	eqcomd	$⊢ φ \to 0_{P} = algSc (P) (0_{R})$
62	61	fveq2d	$⊢ φ \to O (0_{P}) = O (algSc (P) (0_{R}))$
63	54 62	syl5eq	$⊢ φ \to O (\underset{x \in \emptyset}{\sum_{P}} M) = O (algSc (P) (0_{R}))$
64	63	fveq1d	$⊢ φ \to O (\underset{x \in \emptyset}{\sum_{P}} M) (Y) = O (algSc (P) (0_{R})) (Y)$
65		ringgrp	$⊢ R \in Ring \to R \in Grp$
66	56 65	syl	$⊢ φ \to R \in Grp$
67	3 58	grpidcl	$⊢ R \in Grp \to 0_{R} \in B$
68	66 67	syl	$⊢ φ \to 0_{R} \in B$
69	1 2 3 57 4 5 68 6	evl1scad	$⊢ φ \to (algSc (P) (0_{R}) \in U \land O (algSc (P) (0_{R})) (Y) = 0_{R})$
70	69	simprd	$⊢ φ \to O (algSc (P) (0_{R})) (Y) = 0_{R}$
71	64 70	eqtrd	$⊢ φ \to O (\underset{x \in \emptyset}{\sum_{P}} M) (Y) = 0_{R}$
72		mpt0	$⊢ (x \in \emptyset ⟼ O (M) (Y)) = \emptyset$
73	72	oveq2i	$⊢ \underset{x \in \emptyset}{\sum_{R}} O (M) (Y) = \sum_{R} \emptyset$
74	58	gsum0	$⊢ \sum_{R} \emptyset = 0_{R}$
75	73 74	eqtri	$⊢ \underset{x \in \emptyset}{\sum_{R}} O (M) (Y) = 0_{R}$
76	71 75	eqtr4di	$⊢ φ \to O (\underset{x \in \emptyset}{\sum_{P}} M) (Y) = \underset{x \in \emptyset}{\sum_{R}} O (M) (Y)$
77	76	adantr	$⊢ (φ \land \forall x \in \emptyset M \in U) \to O (\underset{x \in \emptyset}{\sum_{P}} M) (Y) = \underset{x \in \emptyset}{\sum_{R}} O (M) (Y)$
78	1 2 3 4 5 6	evl1gsumdlem	$⊢ (m \in Fin \land \neg a \in m \land φ) \to ((\forall x \in m M \in U \to O (\underset{x \in m}{\sum_{P}} M) (Y) = \underset{x \in m}{\sum_{R}} O (M) (Y)) \to (\forall x \in (m \cup \{a\}) M \in U \to O (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (Y) = \underset{x \in m \cup \{a\}}{\sum_{R}} O (M) (Y)))$
79	78	3expia	$⊢ (m \in Fin \land \neg a \in m) \to (φ \to ((\forall x \in m M \in U \to O (\underset{x \in m}{\sum_{P}} M) (Y) = \underset{x \in m}{\sum_{R}} O (M) (Y)) \to (\forall x \in (m \cup \{a\}) M \in U \to O (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (Y) = \underset{x \in m \cup \{a\}}{\sum_{R}} O (M) (Y))))$
80	79	a2d	$⊢ (m \in Fin \land \neg a \in m) \to ((φ \to (\forall x \in m M \in U \to O (\underset{x \in m}{\sum_{P}} M) (Y) = \underset{x \in m}{\sum_{R}} O (M) (Y))) \to (φ \to (\forall x \in (m \cup \{a\}) M \in U \to O (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (Y) = \underset{x \in m \cup \{a\}}{\sum_{R}} O (M) (Y))))$
81		impexp	$⊢ ((φ \land \forall x \in m M \in U) \to O (\underset{x \in m}{\sum_{P}} M) (Y) = \underset{x \in m}{\sum_{R}} O (M) (Y)) \leftrightarrow (φ \to (\forall x \in m M \in U \to O (\underset{x \in m}{\sum_{P}} M) (Y) = \underset{x \in m}{\sum_{R}} O (M) (Y)))$
82		impexp	$⊢ ((φ \land \forall x \in (m \cup \{a\}) M \in U) \to O (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (Y) = \underset{x \in m \cup \{a\}}{\sum_{R}} O (M) (Y)) \leftrightarrow (φ \to (\forall x \in (m \cup \{a\}) M \in U \to O (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (Y) = \underset{x \in m \cup \{a\}}{\sum_{R}} O (M) (Y)))$
83	80 81 82	3imtr4g	$⊢ (m \in Fin \land \neg a \in m) \to (((φ \land \forall x \in m M \in U) \to O (\underset{x \in m}{\sum_{P}} M) (Y) = \underset{x \in m}{\sum_{R}} O (M) (Y)) \to ((φ \land \forall x \in (m \cup \{a\}) M \in U) \to O (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (Y) = \underset{x \in m \cup \{a\}}{\sum_{R}} O (M) (Y)))$
84	18 28 38 48 77 83	findcard2s	$⊢ N \in Fin \to ((φ \land \forall x \in N M \in U) \to O (\underset{x \in N}{\sum_{P}} M) (Y) = \underset{x \in N}{\sum_{R}} O (M) (Y))$
85	84	expd	$⊢ N \in Fin \to (φ \to (\forall x \in N M \in U \to O (\underset{x \in N}{\sum_{P}} M) (Y) = \underset{x \in N}{\sum_{R}} O (M) (Y)))$
86	8 85	mpcom	$⊢ φ \to (\forall x \in N M \in U \to O (\underset{x \in N}{\sum_{P}} M) (Y) = \underset{x \in N}{\sum_{R}} O (M) (Y))$
87	7 86	mpd	$⊢ φ \to O (\underset{x \in N}{\sum_{P}} M) (Y) = \underset{x \in N}{\sum_{R}} O (M) (Y)$

Metamath Proof Explorer

Theorem evl1gsumd

Proof