coe1fzgsumd

Description: Value of an evaluated coefficient in a finite group sum of polynomials. (Contributed by AV, 8-Oct-2019)

	Ref	Expression
Hypotheses	coe1fzgsumd.p	$⊢ P = {Poly}_{1} (R)$
	coe1fzgsumd.b	$⊢ B = {Base}_{P}$
	coe1fzgsumd.r	$⊢ φ \to R \in Ring$
	coe1fzgsumd.k	$⊢ φ \to K \in ℕ_{0}$
	coe1fzgsumd.m	$⊢ φ \to \forall x \in N M \in B$
	coe1fzgsumd.n	$⊢ φ \to N \in Fin$
Assertion	coe1fzgsumd	$⊢ φ \to {coe}_{1} (\underset{x \in N}{\sum_{P}} M) (K) = \underset{x \in N}{\sum_{R}} {coe}_{1} (M) (K)$

Proof

Step	Hyp	Ref	Expression
1		coe1fzgsumd.p	$⊢ P = {Poly}_{1} (R)$
2		coe1fzgsumd.b	$⊢ B = {Base}_{P}$
3		coe1fzgsumd.r	$⊢ φ \to R \in Ring$
4		coe1fzgsumd.k	$⊢ φ \to K \in ℕ_{0}$
5		coe1fzgsumd.m	$⊢ φ \to \forall x \in N M \in B$
6		coe1fzgsumd.n	$⊢ φ \to N \in Fin$
7		raleq	$⊢ n = \emptyset \to (\forall x \in n M \in B \leftrightarrow \forall x \in \emptyset M \in B)$
8	7	anbi2d	$⊢ n = \emptyset \to ((φ \land \forall x \in n M \in B) \leftrightarrow (φ \land \forall x \in \emptyset M \in B))$
9		mpteq1	$⊢ n = \emptyset \to (x \in n ⟼ M) = (x \in \emptyset ⟼ M)$
10	9	oveq2d	$⊢ n = \emptyset \to \underset{x \in n}{\sum_{P}} M = \underset{x \in \emptyset}{\sum_{P}} M$
11	10	fveq2d	$⊢ n = \emptyset \to {coe}_{1} (\underset{x \in n}{\sum_{P}} M) = {coe}_{1} (\underset{x \in \emptyset}{\sum_{P}} M)$
12	11	fveq1d	$⊢ n = \emptyset \to {coe}_{1} (\underset{x \in n}{\sum_{P}} M) (K) = {coe}_{1} (\underset{x \in \emptyset}{\sum_{P}} M) (K)$
13		mpteq1	$⊢ n = \emptyset \to (x \in n ⟼ {coe}_{1} (M) (K)) = (x \in \emptyset ⟼ {coe}_{1} (M) (K))$
14	13	oveq2d	$⊢ n = \emptyset \to \underset{x \in n}{\sum_{R}} {coe}_{1} (M) (K) = \underset{x \in \emptyset}{\sum_{R}} {coe}_{1} (M) (K)$
15	12 14	eqeq12d	$⊢ n = \emptyset \to ({coe}_{1} (\underset{x \in n}{\sum_{P}} M) (K) = \underset{x \in n}{\sum_{R}} {coe}_{1} (M) (K) \leftrightarrow {coe}_{1} (\underset{x \in \emptyset}{\sum_{P}} M) (K) = \underset{x \in \emptyset}{\sum_{R}} {coe}_{1} (M) (K))$
16	8 15	imbi12d	$⊢ n = \emptyset \to (((φ \land \forall x \in n M \in B) \to {coe}_{1} (\underset{x \in n}{\sum_{P}} M) (K) = \underset{x \in n}{\sum_{R}} {coe}_{1} (M) (K)) \leftrightarrow ((φ \land \forall x \in \emptyset M \in B) \to {coe}_{1} (\underset{x \in \emptyset}{\sum_{P}} M) (K) = \underset{x \in \emptyset}{\sum_{R}} {coe}_{1} (M) (K)))$
17		raleq	$⊢ n = m \to (\forall x \in n M \in B \leftrightarrow \forall x \in m M \in B)$
18	17	anbi2d	$⊢ n = m \to ((φ \land \forall x \in n M \in B) \leftrightarrow (φ \land \forall x \in m M \in B))$
19		mpteq1	$⊢ n = m \to (x \in n ⟼ M) = (x \in m ⟼ M)$
20	19	oveq2d	$⊢ n = m \to \underset{x \in n}{\sum_{P}} M = \underset{x \in m}{\sum_{P}} M$
21	20	fveq2d	$⊢ n = m \to {coe}_{1} (\underset{x \in n}{\sum_{P}} M) = {coe}_{1} (\underset{x \in m}{\sum_{P}} M)$
22	21	fveq1d	$⊢ n = m \to {coe}_{1} (\underset{x \in n}{\sum_{P}} M) (K) = {coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K)$
23		mpteq1	$⊢ n = m \to (x \in n ⟼ {coe}_{1} (M) (K)) = (x \in m ⟼ {coe}_{1} (M) (K))$
24	23	oveq2d	$⊢ n = m \to \underset{x \in n}{\sum_{R}} {coe}_{1} (M) (K) = \underset{x \in m}{\sum_{R}} {coe}_{1} (M) (K)$
25	22 24	eqeq12d	$⊢ n = m \to ({coe}_{1} (\underset{x \in n}{\sum_{P}} M) (K) = \underset{x \in n}{\sum_{R}} {coe}_{1} (M) (K) \leftrightarrow {coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) = \underset{x \in m}{\sum_{R}} {coe}_{1} (M) (K))$
26	18 25	imbi12d	$⊢ n = m \to (((φ \land \forall x \in n M \in B) \to {coe}_{1} (\underset{x \in n}{\sum_{P}} M) (K) = \underset{x \in n}{\sum_{R}} {coe}_{1} (M) (K)) \leftrightarrow ((φ \land \forall x \in m M \in B) \to {coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) = \underset{x \in m}{\sum_{R}} {coe}_{1} (M) (K)))$
27		raleq	$⊢ n = m \cup \{a\} \to (\forall x \in n M \in B \leftrightarrow \forall x \in (m \cup \{a\}) M \in B)$
28	27	anbi2d	$⊢ n = m \cup \{a\} \to ((φ \land \forall x \in n M \in B) \leftrightarrow (φ \land \forall x \in (m \cup \{a\}) M \in B))$
29		mpteq1	$⊢ n = m \cup \{a\} \to (x \in n ⟼ M) = (x \in (m \cup \{a\}) ⟼ M)$
30	29	oveq2d	$⊢ n = m \cup \{a\} \to \underset{x \in n}{\sum_{P}} M = \underset{x \in m \cup \{a\}}{\sum_{P}} M$
31	30	fveq2d	$⊢ n = m \cup \{a\} \to {coe}_{1} (\underset{x \in n}{\sum_{P}} M) = {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M)$
32	31	fveq1d	$⊢ n = m \cup \{a\} \to {coe}_{1} (\underset{x \in n}{\sum_{P}} M) (K) = {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (K)$
33		mpteq1	$⊢ n = m \cup \{a\} \to (x \in n ⟼ {coe}_{1} (M) (K)) = (x \in (m \cup \{a\}) ⟼ {coe}_{1} (M) (K))$
34	33	oveq2d	$⊢ n = m \cup \{a\} \to \underset{x \in n}{\sum_{R}} {coe}_{1} (M) (K) = \underset{x \in m \cup \{a\}}{\sum_{R}} {coe}_{1} (M) (K)$
35	32 34	eqeq12d	$⊢ n = m \cup \{a\} \to ({coe}_{1} (\underset{x \in n}{\sum_{P}} M) (K) = \underset{x \in n}{\sum_{R}} {coe}_{1} (M) (K) \leftrightarrow {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (K) = \underset{x \in m \cup \{a\}}{\sum_{R}} {coe}_{1} (M) (K))$
36	28 35	imbi12d	$⊢ n = m \cup \{a\} \to (((φ \land \forall x \in n M \in B) \to {coe}_{1} (\underset{x \in n}{\sum_{P}} M) (K) = \underset{x \in n}{\sum_{R}} {coe}_{1} (M) (K)) \leftrightarrow ((φ \land \forall x \in (m \cup \{a\}) M \in B) \to {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (K) = \underset{x \in m \cup \{a\}}{\sum_{R}} {coe}_{1} (M) (K)))$
37		raleq	$⊢ n = N \to (\forall x \in n M \in B \leftrightarrow \forall x \in N M \in B)$
38	37	anbi2d	$⊢ n = N \to ((φ \land \forall x \in n M \in B) \leftrightarrow (φ \land \forall x \in N M \in B))$
39		mpteq1	$⊢ n = N \to (x \in n ⟼ M) = (x \in N ⟼ M)$
40	39	oveq2d	$⊢ n = N \to \underset{x \in n}{\sum_{P}} M = \underset{x \in N}{\sum_{P}} M$
41	40	fveq2d	$⊢ n = N \to {coe}_{1} (\underset{x \in n}{\sum_{P}} M) = {coe}_{1} (\underset{x \in N}{\sum_{P}} M)$
42	41	fveq1d	$⊢ n = N \to {coe}_{1} (\underset{x \in n}{\sum_{P}} M) (K) = {coe}_{1} (\underset{x \in N}{\sum_{P}} M) (K)$
43		mpteq1	$⊢ n = N \to (x \in n ⟼ {coe}_{1} (M) (K)) = (x \in N ⟼ {coe}_{1} (M) (K))$
44	43	oveq2d	$⊢ n = N \to \underset{x \in n}{\sum_{R}} {coe}_{1} (M) (K) = \underset{x \in N}{\sum_{R}} {coe}_{1} (M) (K)$
45	42 44	eqeq12d	$⊢ n = N \to ({coe}_{1} (\underset{x \in n}{\sum_{P}} M) (K) = \underset{x \in n}{\sum_{R}} {coe}_{1} (M) (K) \leftrightarrow {coe}_{1} (\underset{x \in N}{\sum_{P}} M) (K) = \underset{x \in N}{\sum_{R}} {coe}_{1} (M) (K))$
46	38 45	imbi12d	$⊢ n = N \to (((φ \land \forall x \in n M \in B) \to {coe}_{1} (\underset{x \in n}{\sum_{P}} M) (K) = \underset{x \in n}{\sum_{R}} {coe}_{1} (M) (K)) \leftrightarrow ((φ \land \forall x \in N M \in B) \to {coe}_{1} (\underset{x \in N}{\sum_{P}} M) (K) = \underset{x \in N}{\sum_{R}} {coe}_{1} (M) (K)))$
47		mpt0	$⊢ (x \in \emptyset ⟼ M) = \emptyset$
48	47	oveq2i	$⊢ \underset{x \in \emptyset}{\sum_{P}} M = \sum_{P} \emptyset$
49		eqid	$⊢ 0_{P} = 0_{P}$
50	49	gsum0	$⊢ \sum_{P} \emptyset = 0_{P}$
51	48 50	eqtri	$⊢ \underset{x \in \emptyset}{\sum_{P}} M = 0_{P}$
52	51	fveq2i	$⊢ {coe}_{1} (\underset{x \in \emptyset}{\sum_{P}} M) = {coe}_{1} (0_{P})$
53	52	a1i	$⊢ φ \to {coe}_{1} (\underset{x \in \emptyset}{\sum_{P}} M) = {coe}_{1} (0_{P})$
54	53	fveq1d	$⊢ φ \to {coe}_{1} (\underset{x \in \emptyset}{\sum_{P}} M) (K) = {coe}_{1} (0_{P}) (K)$
55		eqid	$⊢ 0_{R} = 0_{R}$
56	1 49 55	coe1z	$⊢ R \in Ring \to {coe}_{1} (0_{P}) = ℕ_{0} \times \{0_{R}\}$
57	3 56	syl	$⊢ φ \to {coe}_{1} (0_{P}) = ℕ_{0} \times \{0_{R}\}$
58	57	fveq1d	$⊢ φ \to {coe}_{1} (0_{P}) (K) = (ℕ_{0} \times \{0_{R}\}) (K)$
59		fvex	$⊢ 0_{R} \in V$
60		fvconst2g	$⊢ (0_{R} \in V \land K \in ℕ_{0}) \to (ℕ_{0} \times \{0_{R}\}) (K) = 0_{R}$
61	59 4 60	sylancr	$⊢ φ \to (ℕ_{0} \times \{0_{R}\}) (K) = 0_{R}$
62	54 58 61	3eqtrd	$⊢ φ \to {coe}_{1} (\underset{x \in \emptyset}{\sum_{P}} M) (K) = 0_{R}$
63		mpt0	$⊢ (x \in \emptyset ⟼ {coe}_{1} (M) (K)) = \emptyset$
64	63	oveq2i	$⊢ \underset{x \in \emptyset}{\sum_{R}} {coe}_{1} (M) (K) = \sum_{R} \emptyset$
65	55	gsum0	$⊢ \sum_{R} \emptyset = 0_{R}$
66	64 65	eqtri	$⊢ \underset{x \in \emptyset}{\sum_{R}} {coe}_{1} (M) (K) = 0_{R}$
67	62 66	eqtr4di	$⊢ φ \to {coe}_{1} (\underset{x \in \emptyset}{\sum_{P}} M) (K) = \underset{x \in \emptyset}{\sum_{R}} {coe}_{1} (M) (K)$
68	67	adantr	$⊢ (φ \land \forall x \in \emptyset M \in B) \to {coe}_{1} (\underset{x \in \emptyset}{\sum_{P}} M) (K) = \underset{x \in \emptyset}{\sum_{R}} {coe}_{1} (M) (K)$
69	1 2 3 4	coe1fzgsumdlem	$⊢ (m \in Fin \land \neg a \in m \land φ) \to ((\forall x \in m M \in B \to {coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) = \underset{x \in m}{\sum_{R}} {coe}_{1} (M) (K)) \to (\forall x \in (m \cup \{a\}) M \in B \to {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (K) = \underset{x \in m \cup \{a\}}{\sum_{R}} {coe}_{1} (M) (K)))$
70	69	3expia	$⊢ (m \in Fin \land \neg a \in m) \to (φ \to ((\forall x \in m M \in B \to {coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) = \underset{x \in m}{\sum_{R}} {coe}_{1} (M) (K)) \to (\forall x \in (m \cup \{a\}) M \in B \to {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (K) = \underset{x \in m \cup \{a\}}{\sum_{R}} {coe}_{1} (M) (K))))$
71	70	a2d	$⊢ (m \in Fin \land \neg a \in m) \to ((φ \to (\forall x \in m M \in B \to {coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) = \underset{x \in m}{\sum_{R}} {coe}_{1} (M) (K))) \to (φ \to (\forall x \in (m \cup \{a\}) M \in B \to {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (K) = \underset{x \in m \cup \{a\}}{\sum_{R}} {coe}_{1} (M) (K))))$
72		impexp	$⊢ ((φ \land \forall x \in m M \in B) \to {coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) = \underset{x \in m}{\sum_{R}} {coe}_{1} (M) (K)) \leftrightarrow (φ \to (\forall x \in m M \in B \to {coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) = \underset{x \in m}{\sum_{R}} {coe}_{1} (M) (K)))$
73		impexp	$⊢ ((φ \land \forall x \in (m \cup \{a\}) M \in B) \to {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (K) = \underset{x \in m \cup \{a\}}{\sum_{R}} {coe}_{1} (M) (K)) \leftrightarrow (φ \to (\forall x \in (m \cup \{a\}) M \in B \to {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (K) = \underset{x \in m \cup \{a\}}{\sum_{R}} {coe}_{1} (M) (K)))$
74	71 72 73	3imtr4g	$⊢ (m \in Fin \land \neg a \in m) \to (((φ \land \forall x \in m M \in B) \to {coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) = \underset{x \in m}{\sum_{R}} {coe}_{1} (M) (K)) \to ((φ \land \forall x \in (m \cup \{a\}) M \in B) \to {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (K) = \underset{x \in m \cup \{a\}}{\sum_{R}} {coe}_{1} (M) (K)))$
75	16 26 36 46 68 74	findcard2s	$⊢ N \in Fin \to ((φ \land \forall x \in N M \in B) \to {coe}_{1} (\underset{x \in N}{\sum_{P}} M) (K) = \underset{x \in N}{\sum_{R}} {coe}_{1} (M) (K))$
76	75	expd	$⊢ N \in Fin \to (φ \to (\forall x \in N M \in B \to {coe}_{1} (\underset{x \in N}{\sum_{P}} M) (K) = \underset{x \in N}{\sum_{R}} {coe}_{1} (M) (K)))$
77	6 76	mpcom	$⊢ φ \to (\forall x \in N M \in B \to {coe}_{1} (\underset{x \in N}{\sum_{P}} M) (K) = \underset{x \in N}{\sum_{R}} {coe}_{1} (M) (K))$
78	5 77	mpd	$⊢ φ \to {coe}_{1} (\underset{x \in N}{\sum_{P}} M) (K) = \underset{x \in N}{\sum_{R}} {coe}_{1} (M) (K)$

Metamath Proof Explorer

Theorem coe1fzgsumd

Proof