Theorem fsum0diag 7258

Description: Two ways to express "the sum of A(j) x. B(k) where j + k <_ N."

Assertion

Ref	Expression
fsum0diag	|- ((N e. NN0 /\ A.j e. (0...N)A e. CC /\ A.k e. (0...N)B e. CC) -> sum_j e. (0...N)sum_k e. (0...(N - j))(A x. B) = sum_k e. (0...N)sum_j e. (0...k)(A x. [_(k - j) / k]_B))

Distinct variable groups:   A,k   B,j   j,k,N

Proof of Theorem fsum0diag

Step	Hyp	Ref	Expression
1		fsum0diaglem2 7257	. . 3 |- (n e. NN0 -> (((A.j e. (0...n)A e. CC /\ A.k e. (0...n)B e. CC) -> sum_j e. (0...n)sum_k e. (0...(n - j))(A x. B) = sum_k e. (0...n)sum_j e. (0...k)(A x. [_(k - j) / k]_B)) -> ((A.j e. (0...(n + 1))A e. CC /\ A.k e. (0...(n + 1))B e. CC) -> sum_j e. (0...(n + 1))sum_k e. (0...((n + 1) - j))(A x. B) = sum_k e. (0...(n + 1))sum_j e. (0...k)(A x. [_(k - j) / k]_B))))
2		oprex 3989	. . . . . 6 |- ([_0 / j]_A x. [_0 / k]_B) e. V
3		0z 6148	. . . . . 6 |- 0 e. ZZ
4		ax-17 973	. . . . . . . . . 10 |- (m e. 0 -> A.j m e. 0)
5	4	hbcsb1g 2027	. . . . . . . . 9 |- (0 e. ZZ -> (m e. [_0 / j]_A -> A.j m e. [_0 / j]_A))
6	3, 5	ax-mp 7	. . . . . . . 8 |- (m e. [_0 / j]_A -> A.j m e. [_0 / j]_A)
7		ax-17 973	. . . . . . . 8 |- (m e. x. -> A.j m e. x. )
8		ax-17 973	. . . . . . . 8 |- (m e. [_0 / k]_B -> A.j m e. [_0 / k]_B)
9	6, 7, 8	hbopr 3987	. . . . . . 7 |- (m e. ([_0 / j]_A x. [_0 / k]_B) -> A.j m e. ([_0 / j]_A x. [_0 / k]_B))
10		csbeq1a 2009	. . . . . . . 8 |- (j = 0 -> A = [_0 / j]_A)
11	10	opreq1d 3981	. . . . . . 7 |- (j = 0 -> (A x. [_0 / k]_B) = ([_0 / j]_A x. [_0 / k]_B))
12	9, 11	fsum1f 7007	. . . . . 6 |- ((([_0 / j]_A x. [_0 / k]_B) e. V /\ 0 e. ZZ) -> sum_j e. (0...0)(A x. [_0 / k]_B) = ([_0 / j]_A x. [_0 / k]_B))
13	2, 3, 12	mp2an 699	. . . . 5 |- sum_j e. (0...0)(A x. [_0 / k]_B) = ([_0 / j]_A x. [_0 / k]_B)
14		sumex 6981	. . . . . 6 |- sum_j e. (0...0)(A x. [_0 / k]_B) e. V
15		ax-17 973	. . . . . . . 8 |- (m e. (0...0) -> A.k m e. (0...0))
16		ax-17 973	. . . . . . . . 9 |- (m e. A -> A.k m e. A)
17		ax-17 973	. . . . . . . . 9 |- (m e. x. -> A.k m e. x. )
18		ax-17 973	. . . . . . . . . . 11 |- (m e. 0 -> A.k m e. 0)
19	18	hbcsb1g 2027	. . . . . . . . . 10 |- (0 e. ZZ -> (m e. [_0 / k]_B -> A.k m e. [_0 / k]_B))
20	3, 19	ax-mp 7	. . . . . . . . 9 |- (m e. [_0 / k]_B -> A.k m e. [_0 / k]_B)
21	16, 17, 20	hbopr 3987	. . . . . . . 8 |- (m e. (A x. [_0 / k]_B) -> A.k m e. (A x. [_0 / k]_B))
22	15, 21	hbsum 6984	. . . . . . 7 |- (m e. sum_j e. (0...0)(A x. [_0 / k]_B) -> A.k m e. sum_j e. (0...0)(A x. [_0 / k]_B))
23		opreq2 3975	. . . . . . . 8 |- (k = 0 -> (0...k) = (0...0))
24		opreq12 3976	. . . . . . . . . . . 12 |- ((k = 0 /\ j = 0) -> (k - j) = (0 - 0))
25		0cn 5340	. . . . . . . . . . . . 13 |- 0 e. CC
26	25	subid 5403	. . . . . . . . . . . 12 |- (0 - 0) = 0
27	24, 26	syl6eq 1526	. . . . . . . . . . 11 |- ((k = 0 /\ j = 0) -> (k - j) = 0)
28	27	csbeq1d 2007	. . . . . . . . . 10 |- ((k = 0 /\ j = 0) -> [_(k - j) / k]_B = [_0 / k]_B)
29	28	opreq2d 3982	. . . . . . . . 9 |- ((k = 0 /\ j = 0) -> (A x. [_(k - j) / k]_B) = (A x. [_0 / k]_B))
30		elfz1eqt 6493	. . . . . . . . 9 |- (j e. (0...0) -> j = 0)
31	29, 30	sylan2 453	. . . . . . . 8 |- ((k = 0 /\ j e. (0...0)) -> (A x. [_(k - j) / k]_B) = (A x. [_0 / k]_B))
32	23, 31	sumeq12rdv 6996	. . . . . . 7 |- (k = 0 -> sum_j e. (0...k)(A x. [_(k - j) / k]_B) = sum_j e. (0...0)(A x. [_0 / k]_B))
33	22, 32	fsum1f 7007	. . . . . 6 |- ((sum_j e. (0...0)(A x. [_0 / k]_B) e. V /\ 0 e. ZZ) -> sum_k e. (0...0)sum_j e. (0...k)(A x. [_(k - j) / k]_B) = sum_j e. (0...0)(A x. [_0 / k]_B))
34	14, 3, 33	mp2an 699	. . . . 5 |- sum_k e. (0...0)sum_j e. (0...k)(A x. [_(k - j) / k]_B) = sum_j e. (0...0)(A x. [_0 / k]_B)
35		sumex 6981	. . . . . . 7 |- sum_k e. (0...0)([_0 / j]_A x. B) e. V
36		ax-17 973	. . . . . . . . 9 |- (m e. (0...0) -> A.j m e. (0...0))
37		ax-17 973	. . . . . . . . . 10 |- (m e. B -> A.j m e. B)
38	6, 7, 37	hbopr 3987	. . . . . . . . 9 |- (m e. ([_0 / j]_A x. B) -> A.j m e. ([_0 / j]_A x. B))
39	36, 38	hbsum 6984	. . . . . . . 8 |- (m e. sum_k e. (0...0)([_0 / j]_A x. B) -> A.j m e. sum_k e. (0...0)([_0 / j]_A x. B))
40		opreq2 3975	. . . . . . . . . . 11 |- (j = 0 -> (0 - j) = (0 - 0))
41	40, 26	syl6eq 1526	. . . . . . . . . 10 |- (j = 0 -> (0 - j) = 0)
42	41	opreq2d 3982	. . . . . . . . 9 |- (j = 0 -> (0...(0 - j)) = (0...0))
43	10	opreq1d 3981	. . . . . . . . . 10 |- (j = 0 -> (A x. B) = ([_0 / j]_A x. B))
44	43	adantr 391	. . . . . . . . 9 |- ((j = 0 /\ k e. (0...0)) -> (A x. B) = ([_0 / j]_A x. B))
45	42, 44	sumeq12rdv 6996	. . . . . . . 8 |- (j = 0 -> sum_k e. (0...(0 - j))(A x. B) = sum_k e. (0...0)([_0 / j]_A x. B))
46	39, 45	fsum1f 7007	. . . . . . 7 |- ((sum_k e. (0...0)([_0 / j]_A x. B) e. V /\ 0 e. ZZ) -> sum_j e. (0...0)sum_k e. (0...(0 - j))(A x. B) = sum_k e. (0...0)([_0 / j]_A x. B))
47	35, 3, 46	mp2an 699	. . . . . 6 |- sum_j e. (0...0)sum_k e. (0...(0 - j))(A x. B) = sum_k e. (0...0)([_0 / j]_A x. B)
48		ax-17 973	. . . . . . . . 9 |- (m e. [_0 / j]_A -> A.k m e. [_0 / j]_A)
49	48, 17, 20	hbopr 3987	. . . . . . . 8 |- (m e. ([_0 / j]_A x. [_0 / k]_B) -> A.k m e. ([_0 / j]_A x. [_0 / k]_B))
50		csbeq1a 2009	. . . . . . . . 9 |- (k = 0 -> B = [_0 / k]_B)
51	50	opreq2d 3982	. . . . . . . 8 |- (k = 0 -> ([_0 / j]_A x. B) = ([_0 / j]_A x. [_0 / k]_B))
52	49, 51	fsum1f 7007	. . . . . . 7 |- ((([_0 / j]_A x. [_0 / k]_B) e. V /\ 0 e. ZZ) -> sum_k e. (0...0)([_0 / j]_A x. B) = ([_0 / j]_A x. [_0 / k]_B))
53	2, 3, 52	mp2an 699	. . . . . 6 |- sum_k e. (0...0)([_0 / j]_A x. B) = ([_0 / j]_A x. [_0 / k]_B)
54	47, 53	eqtr 1498	. . . . 5 |- sum_j e. (0...0)sum_k e. (0...(0 - j))(A x. B) = ([_0 / j]_A x. [_0 / k]_B)
55	13, 34, 54	3eqtr4r 1509	. . . 4 |- sum_j e. (0...0)sum_k e. (0...(0 - j))(A x. B) = sum_k e. (0...0)sum_j e. (0...k)(A x. [_(k - j) / k]_B)
56	55	a1i 8	. . 3 |- ((A.j e. (0...0)A e. CC /\ A.k e. (0...0)B e. CC) -> sum_j e. (0...0)sum_k e. (0...(0 - j))(A x. B) = sum_k e. (0...0)sum_j e. (0...k)(A x. [_(k - j) / k]_B))
57		opreq2 3975	. . . . . 6 |- (m = 0 -> (0...m) = (0...0))
58	57	raleq1d 1792	. . . . 5 |- (m = 0 -> (A.j e. (0...m)A e. CC