Theorem csbfsumlem 6972

Description: Lemma for csbfsum 6973.

Hypotheses

Ref	Expression
csbfsumlem.1	|- A e. V
csbfsumlem.2	|- B e. V

Assertion

Ref	Expression
csbfsumlem	|- (N e. (ZZ>` M) -> [_A / x]_sum_k e. (M...N)B = sum_k e. (M...N)[_A / x]_B)

Distinct variable groups:   x,k,A   x,M,k   x,N

Proof of Theorem csbfsumlem

Step	Hyp	Ref	Expression
1		csbfsumlem.1	. . . 4 |- A e. V
2		opreq2 3960	. . . . . 6 |- (n = M -> (M...n) = (M...M))
3	2	sumeq1d 6936	. . . . 5 |- (n = M -> sum_k e. (M...n)B = sum_k e. (M...M)B)
4	3	csbeq2dv 2015	. . . 4 |- ((n = M /\ A e. V) -> [_A / x]_sum_k e. (M...n)B = [_A / x]_sum_k e. (M...M)B)
5	1, 4	mpan2 695	. . 3 |- (n = M -> [_A / x]_sum_k e. (M...n)B = [_A / x]_sum_k e. (M...M)B)
6	2	sumeq1d 6936	. . 3 |- (n = M -> sum_k e. (M...n)[_A / x]_B = sum_k e. (M...M)[_A / x]_B)
7	5, 6	eqeq12d 1486	. 2 |- (n = M -> ([_A / x]_sum_k e. (M...n)B = sum_k e. (M...n)[_A / x]_B <-> [_A / x]_sum_k e. (M...M)B = sum_k e. (M...M)[_A / x]_B))
8		opreq2 3960	. . . . . 6 |- (n = m -> (M...n) = (M...m))
9	8	sumeq1d 6936	. . . . 5 |- (n = m -> sum_k e. (M...n)B = sum_k e. (M...m)B)
10	9	csbeq2dv 2015	. . . 4 |- ((n = m /\ A e. V) -> [_A / x]_sum_k e. (M...n)B = [_A / x]_sum_k e. (M...m)B)
11	1, 10	mpan2 695	. . 3 |- (n = m -> [_A / x]_sum_k e. (M...n)B = [_A / x]_sum_k e. (M...m)B)
12	8	sumeq1d 6936	. . 3 |- (n = m -> sum_k e. (M...n)[_A / x]_B = sum_k e. (M...m)[_A / x]_B)
13	11, 12	eqeq12d 1486	. 2 |- (n = m -> ([_A / x]_sum_k e. (M...n)B = sum_k e. (M...n)[_A / x]_B <-> [_A / x]_sum_k e. (M...m)B = sum_k e. (M...m)[_A / x]_B))
14		opreq2 3960	. . . . . 6 |- (n = (m + 1) -> (M...n) = (M...(m + 1)))
15	14	sumeq1d 6936	. . . . 5 |- (n = (m + 1) -> sum_k e. (M...n)B = sum_k e. (M...(m + 1))B)
16	15	csbeq2dv 2015	. . . 4 |- ((n = (m + 1) /\ A e. V) -> [_A / x]_sum_k e. (M...n)B = [_A / x]_sum_k e. (M...(m + 1))B)
17	1, 16	mpan2 695	. . 3 |- (n = (m + 1) -> [_A / x]_sum_k e. (M...n)B = [_A / x]_sum_k e. (M...(m + 1))B)
18	14	sumeq1d 6936	. . 3 |- (n = (m + 1) -> sum_k e. (M...n)[_A / x]_B = sum_k e. (M...(m + 1))[_A / x]_B)
19	17, 18	eqeq12d 1486	. 2 |- (n = (m + 1) -> ([_A / x]_sum_k e. (M...n)B = sum_k e. (M...n)[_A / x]_B <-> [_A / x]_sum_k e. (M...(m + 1))B = sum_k e. (M...(m + 1))[_A / x]_B))
20		opreq2 3960	. . . . . 6 |- (n = N -> (M...n) = (M...N))
21	20	sumeq1d 6936	. . . . 5 |- (n = N -> sum_k e. (M...n)B = sum_k e. (M...N)B)
22	21	csbeq2dv 2015	. . . 4 |- ((n = N /\ A e. V) -> [_A / x]_sum_k e. (M...n)B = [_A / x]_sum_k e. (M...N)B)
23	1, 22	mpan2 695	. . 3 |- (n = N -> [_A / x]_sum_k e. (M...n)B = [_A / x]_sum_k e. (M...N)B)
24	20	sumeq1d 6936	. . 3 |- (n = N -> sum_k e. (M...n)[_A / x]_B = sum_k e. (M...N)[_A / x]_B)
25	23, 24	eqeq12d 1486	. 2 |- (n = N -> ([_A / x]_sum_k e. (M...n)B = sum_k e. (M...n)[_A / x]_B <-> [_A / x]_sum_k e. (M...N)B = sum_k e. (M...N)[_A / x]_B))
26		csbcomg 2013	. . . 4 |- ((A e. V /\ M e. ZZ) -> [_A / x]_[_M / k]_B = [_M / k]_[_A / x]_B)
27	1, 26	mpan 694	. . 3 |- (M e. ZZ -> [_A / x]_[_M / k]_B = [_M / k]_[_A / x]_B)
28		csbfsumlem.2	. . . . . 6 |- B e. V
29	28	fsum1slem 6954	. . . . 5 |- (M e. ZZ -> sum_k e. (M...M)B = [_M / k]_B)
30	29	csbeq2dv 2015	. . . 4 |- ((M e. ZZ /\ A e. V) -> [_A / x]_sum_k e. (M...M)B = [_A / x]_[_M / k]_B)
31	1, 30	mpan2 695	. . 3 |- (M e. ZZ -> [_A / x]_sum_k e. (M...M)B = [_A / x]_[_M / k]_B)
32	1, 28	csbex 2005	. . . 4 |- [_A / x]_B e. V
33	32	fsum1slem 6954	. . 3 |- (M e. ZZ -> sum_k e. (M...M)[_A / x]_B = [_M / k]_[_A / x]_B)
34	27, 31, 33	3eqtr4d 1514	. 2 |- (M e. ZZ -> [_A / x]_sum_k e. (M...M)B = sum_k e. (M...M)[_A / x]_B)
35		pm3.27 323	. . . . 5 |- ((m e. (ZZ>` M) /\ [_A / x]_sum_k e. (M...m)B = sum_k e. (M...m)[_A / x]_B) -> [_A / x]_sum_k e. (M...m)B = sum_k e. (M...m)[_A / x]_B)
36	35	opreq1d 3966	. . . 4 |- ((m e. (ZZ>` M) /\ [_A / x]_sum_k e. (M...m)B = sum_k e. (M...m)[_A / x]_B) -> ([_A / x]_sum_k e. (M...m)B + [_(m + 1) / k]_[_A / x]_B) = (sum_k e. (M...m)[_A / x]_B + [_(m + 1) / k]_[_A / x]_B))
37	28	fsump1slem 6958	. . . . . . . 8 |- (m e. (ZZ>` M) -> sum_k e. (M...(m + 1))B = (sum_k e. (M...m)B + [_(m + 1) / k]_B))
38	37	csbeq2dv 2015	. . . . . . 7 |- ((m e. (ZZ>` M) /\ A e. V) -> [_A / x]_sum_k e. (M...(m + 1))B = [_A / x]_(sum_k e. (M...m)B + [_(m + 1) / k]_B))
39	1, 38	mpan2 695	. . . . . 6 |- (m e. (ZZ>` M) -> [_A / x]_sum_k e. (M...(m + 1))B = [_A / x]_(sum_k e. (M...m)B + [_(m + 1) / k]_B))
40		csbopr12g 3978	. . . . . . . 8 |- (A e. V -> [_A / x]_(sum_k e. (M...m)B + [_(m + 1) / k]_B) = ([_A / x]_sum_k e. (M...m)B + [_A / x]_[_(m + 1) / k]_B))
41	1, 40	ax-mp 7	. . . . . . 7 |- [_A / x]_(sum_k e. (M...m)B + [_(m + 1) / k]_B) = ([_A / x]_sum_k e. (M...m)B + [_A / x]_[_(m + 1) / k]_B)
42		oprex 3974	. . . . . . . . 9 |- (m + 1) e. V
43		csbcomg 2013	. . . . . . . . 9 |- ((A e. V /\ (m + 1) e. V) -> [_A / x]_[_(m + 1) / k]_B = [_(m + 1) / k]_[_A / x]_B)
44	1, 42, 43	mp2an 696	. . . . . . . 8 |- [_A / x]_[_(m + 1) / k]_B = [_(m + 1) / k]_[_A / x]_B
45	44	opreq2i 3963	. . . . . . 7 |- ([_A / x]_sum_k e. (M...m)B + [_A / x]_[_(m + 1) / k]_B) = ([_A / x]_sum_k e. (M...m)B + [_(m + 1) / k]_[_A / x]_B)
46	41, 45	eqtr 1492	. . . . . 6 |- [_A / x]_(sum_k e. (M...m)B + [_(m + 1) / k]_B) = ([_A / x]_sum_k e. (M...m)B + [_(m + 1) / k]_[_A / x]_B)
47	39, 46	syl6eq 1520	. . . . 5 |- (m e. (ZZ>` M) -> [_A / x]_sum_k e. (M...(m + 1))B = ([_A / x]_sum_k e. (M...m)B + [_(m + 1) / k]_[_A / x]_B))
48	47	adantr 389	. . . 4 |- ((m e. (ZZ>` M) /\ [_A / x]_sum_k e. (M...m)B = sum_k e. (M...m)[_A / x]_B) -> [_A