Theorem fsumcnv

Description: Transform a region of summation by using the converse operation. (Contributed by Mario Carneiro, 23-Apr-2014)

	Ref	Expression
Hypotheses	fsumcnv.1	$$⊢x=⟨j,k⟩\to B=D$$
	fsumcnv.2	$$⊢y=⟨k,j⟩\to C=D$$
	fsumcnv.3	$$⊢\phi \to A\in \mathrm{Fin}$$
	fsumcnv.4	$$⊢\phi \to \mathrm{Rel}A$$
	fsumcnv.5	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℂ$$
Assertion	fsumcnv	$$⊢\phi \to \sum _{x\in A}B=\sum _{y\in A^{-1}}C$$

Proof

Step	Hyp	Ref	Expression
1		fsumcnv.1	$$⊢x=⟨j,k⟩\to B=D$$
2		fsumcnv.2	$$⊢y=⟨k,j⟩\to C=D$$
3		fsumcnv.3	$$⊢\phi \to A\in \mathrm{Fin}$$
4		fsumcnv.4	$$⊢\phi \to \mathrm{Rel}A$$
5		fsumcnv.5	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℂ$$
6		csbeq1a	$$⊢x=⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩\to B=⦋⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩/x⦌B$$
7		fvex	$$⊢2^{nd}\left(y\right)\in \mathrm{V}$$
8		fvex	$$⊢1^{st}\left(y\right)\in \mathrm{V}$$
9		opex	$$⊢⟨j,k⟩\in \mathrm{V}$$
10	9 1	csbie	$$⊢⦋⟨j,k⟩/x⦌B=D$$
11		opeq12	$$⊢\left(j=2^{nd}\left(y\right)\wedge k=1^{st}\left(y\right)\right)\to ⟨j,k⟩=⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩$$
12	11	csbeq1d	$$⊢\left(j=2^{nd}\left(y\right)\wedge k=1^{st}\left(y\right)\right)\to ⦋⟨j,k⟩/x⦌B=⦋⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩/x⦌B$$
13	10 12	eqtr3id	$$⊢\left(j=2^{nd}\left(y\right)\wedge k=1^{st}\left(y\right)\right)\to D=⦋⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩/x⦌B$$
14	7 8 13	csbie2	$$⊢⦋2^{nd}\left(y\right)/j⦌⦋1^{st}\left(y\right)/k⦌D=⦋⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩/x⦌B$$
15	6 14	eqtr4di	$$⊢x=⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩\to B=⦋2^{nd}\left(y\right)/j⦌⦋1^{st}\left(y\right)/k⦌D$$
16		cnvfi	$$⊢A\in \mathrm{Fin}\to A^{-1}\in \mathrm{Fin}$$
17	3 16	syl	$$⊢\phi \to A^{-1}\in \mathrm{Fin}$$
18		relcnv	$$⊢\mathrm{Rel}{A}^{-1}$$
19		cnvf1o	$$⊢\mathrm{Rel}{A}^{-1}\to \left(z\in A^{-1}⟼\bigcup {\left\{z\right\}}^{-1}\right):A^{-1}\underset{1-1\; onto}{⟶}{A^{-1}}^{-1}$$
20	18 19	ax-mp	$$⊢\left(z\in A^{-1}⟼\bigcup {\left\{z\right\}}^{-1}\right):A^{-1}\underset{1-1\; onto}{⟶}{A^{-1}}^{-1}$$
21		dfrel2	$$⊢\mathrm{Rel}A\leftrightarrow {A^{-1}}^{-1}=A$$
22	4 21	sylib	$$⊢\phi \to {A^{-1}}^{-1}=A$$
23	22	f1oeq3d	$$⊢\phi \to \left(\left(z\in A^{-1}⟼\bigcup {\left\{z\right\}}^{-1}\right):A^{-1}\underset{1-1\; onto}{⟶}{A^{-1}}^{-1}\leftrightarrow \left(z\in A^{-1}⟼\bigcup {\left\{z\right\}}^{-1}\right):A^{-1}\underset{1-1\; onto}{⟶}A\right)$$
24	20 23	mpbii	$$⊢\phi \to \left(z\in A^{-1}⟼\bigcup {\left\{z\right\}}^{-1}\right):A^{-1}\underset{1-1\; onto}{⟶}A$$
25		1st2nd	$$⊢\left(\mathrm{Rel}{A}^{-1}\wedge y\in A^{-1}\right)\to y=⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩$$
26	18 25	mpan	$$⊢y\in A^{-1}\to y=⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩$$
27	26	fveq2d	$$⊢y\in A^{-1}\to \left(z\in A^{-1}⟼\bigcup {\left\{z\right\}}^{-1}\right)\left(y\right)=\left(z\in A^{-1}⟼\bigcup {\left\{z\right\}}^{-1}\right)\left(⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩\right)$$
28		id	$$⊢y\in A^{-1}\to y\in A^{-1}$$
29	26 28	eqeltrrd	$$⊢y\in A^{-1}\to ⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩\in A^{-1}$$
30		sneq	$$⊢z=⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩\to \left\{z\right\}=\left\{⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩\right\}$$
31	30	cnveqd	$$⊢z=⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩\to {\left\{z\right\}}^{-1}={\left\{⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩\right\}}^{-1}$$
32	31	unieqd	$$⊢z=⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩\to \bigcup {\left\{z\right\}}^{-1}=\bigcup {\left\{⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩\right\}}^{-1}$$
33		opswap	$$⊢\bigcup {\left\{⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩\right\}}^{-1}=⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩$$
34	32 33	eqtrdi	$$⊢z=⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩\to \bigcup {\left\{z\right\}}^{-1}=⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩$$
35		eqid	$$⊢\left(z\in A^{-1}⟼\bigcup {\left\{z\right\}}^{-1}\right)=\left(z\in A^{-1}⟼\bigcup {\left\{z\right\}}^{-1}\right)$$
36		opex	$$⊢⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩\in \mathrm{V}$$
37	34 35 36	fvmpt	$$⊢⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩\in A^{-1}\to \left(z\in A^{-1}⟼\bigcup {\left\{z\right\}}^{-1}\right)\left(⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩\right)=⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩$$
38	29 37	syl	$$⊢y\in A^{-1}\to \left(z\in A^{-1}⟼\bigcup {\left\{z\right\}}^{-1}\right)\left(⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩\right)=⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩$$
39	27 38	eqtrd	$$⊢y\in A^{-1}\to \left(z\in A^{-1}⟼\bigcup {\left\{z\right\}}^{-1}\right)\left(y\right)=⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩$$
40	39	adantl	$$⊢\left(\phi \wedge y\in A^{-1}\right)\to \left(z\in A^{-1}⟼\bigcup {\left\{z\right\}}^{-1}\right)\left(y\right)=⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩$$
41	15 17 24 40 5	fsumf1o	$$⊢\phi \to \sum _{x\in A}B=\sum _{y\in A^{-1}}⦋2^{nd}\left(y\right)/j⦌⦋1^{st}\left(y\right)/k⦌D$$
42		csbeq1a	$$⊢y=⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩\to C=⦋⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩/y⦌C$$
43	26 42	syl	$$⊢y\in A^{-1}\to C=⦋⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩/y⦌C$$
44		opex	$$⊢⟨k,j⟩\in \mathrm{V}$$
45	44 2	csbie	$$⊢⦋⟨k,j⟩/y⦌C=D$$
46		opeq12	$$⊢\left(k=1^{st}\left(y\right)\wedge j=2^{nd}\left(y\right)\right)\to ⟨k,j⟩=⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩$$
47	46	ancoms	$$⊢\left(j=2^{nd}\left(y\right)\wedge k=1^{st}\left(y\right)\right)\to ⟨k,j⟩=⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩$$
48	47	csbeq1d	$$⊢\left(j=2^{nd}\left(y\right)\wedge k=1^{st}\left(y\right)\right)\to ⦋⟨k,j⟩/y⦌C=⦋⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩/y⦌C$$
49	45 48	eqtr3id	$$⊢\left(j=2^{nd}\left(y\right)\wedge k=1^{st}\left(y\right)\right)\to D=⦋⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩/y⦌C$$
50	7 8 49	csbie2	$$⊢⦋2^{nd}\left(y\right)/j⦌⦋1^{st}\left(y\right)/k⦌D=⦋⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩/y⦌C$$
51	43 50	eqtr4di	$$⊢y\in A^{-1}\to C=⦋2^{nd}\left(y\right)/j⦌⦋1^{st}\left(y\right)/k⦌D$$
52	51	sumeq2i	$$⊢\sum _{y\in A^{-1}}C=\sum _{y\in A^{-1}}⦋2^{nd}\left(y\right)/j⦌⦋1^{st}\left(y\right)/k⦌D$$
53	41 52	eqtr4di	$$⊢\phi \to \sum _{x\in A}B=\sum _{y\in A^{-1}}C$$