gsumcom2

Description: Two-dimensional commutation of a group sum. Note that while A and D are constants w.r.t. j , k , C ( j ) and E ( k ) are not. (Contributed by Mario Carneiro, 28-Dec-2014)

	Ref	Expression
Hypotheses	gsum2d2.b	$⊢ B = {Base}_{G}$
	gsum2d2.z	$⊢ \underset{˙}{0} = 0_{G}$
	gsum2d2.g	$⊢ φ \to G \in CMnd$
	gsum2d2.a	$⊢ φ \to A \in V$
	gsum2d2.r	$⊢ (φ \land j \in A) \to C \in W$
	gsum2d2.f	$⊢ (φ \land (j \in A \land k \in C)) \to X \in B$
	gsum2d2.u	$⊢ φ \to U \in Fin$
	gsum2d2.n	$⊢ (φ \land ((j \in A \land k \in C) \land \neg j U k)) \to X = \underset{˙}{0}$
	gsumcom2.d	$⊢ φ \to D \in Y$
	gsumcom2.c	$⊢ φ \to ((j \in A \land k \in C) \leftrightarrow (k \in D \land j \in E))$
Assertion	gsumcom2	$⊢ φ \to \sum_{G} (j \in A, k \in C ⟼ X) = \sum_{G} (k \in D, j \in E ⟼ X)$

Proof

Step	Hyp	Ref	Expression
1		gsum2d2.b	$⊢ B = {Base}_{G}$
2		gsum2d2.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsum2d2.g	$⊢ φ \to G \in CMnd$
4		gsum2d2.a	$⊢ φ \to A \in V$
5		gsum2d2.r	$⊢ (φ \land j \in A) \to C \in W$
6		gsum2d2.f	$⊢ (φ \land (j \in A \land k \in C)) \to X \in B$
7		gsum2d2.u	$⊢ φ \to U \in Fin$
8		gsum2d2.n	$⊢ (φ \land ((j \in A \land k \in C) \land \neg j U k)) \to X = \underset{˙}{0}$
9		gsumcom2.d	$⊢ φ \to D \in Y$
10		gsumcom2.c	$⊢ φ \to ((j \in A \land k \in C) \leftrightarrow (k \in D \land j \in E))$
11		vsnex	$⊢ \{j\} \in V$
12		xpexg	$⊢ (\{j\} \in V \land C \in W) \to \{j\} \times C \in V$
13	11 5 12	sylancr	$⊢ (φ \land j \in A) \to \{j\} \times C \in V$
14	13	ralrimiva	$⊢ φ \to \forall j \in A \{j\} \times C \in V$
15		iunexg	$⊢ (A \in V \land \forall j \in A \{j\} \times C \in V) \to ⋃_{j \in A} (\{j\} \times C) \in V$
16	4 14 15	syl2anc	$⊢ φ \to ⋃_{j \in A} (\{j\} \times C) \in V$
17	6	ralrimivva	$⊢ φ \to \forall j \in A \forall k \in C X \in B$
18		eqid	$⊢ (j \in A, k \in C ⟼ X) = (j \in A, k \in C ⟼ X)$
19	18	fmpox	$⊢ \forall j \in A \forall k \in C X \in B \leftrightarrow (j \in A, k \in C ⟼ X) : ⋃_{j \in A} (\{j\} \times C) ⟶ B$
20	17 19	sylib	$⊢ φ \to (j \in A, k \in C ⟼ X) : ⋃_{j \in A} (\{j\} \times C) ⟶ B$
21	1 2 3 4 5 6 7 8	gsum2d2lem	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((j \in A, k \in C ⟼ X))$
22		relxp	$⊢ Rel (\{k\} \times E)$
23	22	rgenw	$⊢ \forall k \in D Rel (\{k\} \times E)$
24		reliun	$⊢ Rel ⋃_{k \in D} (\{k\} \times E) \leftrightarrow \forall k \in D Rel (\{k\} \times E)$
25	23 24	mpbir	$⊢ Rel ⋃_{k \in D} (\{k\} \times E)$
26		cnvf1o	$⊢ Rel ⋃_{k \in D} (\{k\} \times E) \to (z \in ⋃_{k \in D} (\{k\} \times E) ⟼ ⋃ {\{z\}}^{-1}) : ⋃_{k \in D} (\{k\} \times E) \underset{1-1 onto}{⟶} {⋃_{k \in D} (\{k\} \times E)}^{-1}$
27	25 26	ax-mp	$⊢ (z \in ⋃_{k \in D} (\{k\} \times E) ⟼ ⋃ {\{z\}}^{-1}) : ⋃_{k \in D} (\{k\} \times E) \underset{1-1 onto}{⟶} {⋃_{k \in D} (\{k\} \times E)}^{-1}$
28		relxp	$⊢ Rel (\{j\} \times C)$
29	28	rgenw	$⊢ \forall j \in A Rel (\{j\} \times C)$
30		reliun	$⊢ Rel ⋃_{j \in A} (\{j\} \times C) \leftrightarrow \forall j \in A Rel (\{j\} \times C)$
31	29 30	mpbir	$⊢ Rel ⋃_{j \in A} (\{j\} \times C)$
32		relcnv	$⊢ Rel {⋃_{k \in D} (\{k\} \times E)}^{-1}$
33		nfv	$⊢ Ⅎ k φ$
34		nfv	$⊢ Ⅎ k ⟨x, y⟩ \in ⋃_{j \in A} (\{j\} \times C)$
35		nfiu1	$⊢ \underline{Ⅎ} k ⋃_{k \in D} (\{k\} \times E)$
36	35	nfcnv	$⊢ \underline{Ⅎ} k {⋃_{k \in D} (\{k\} \times E)}^{-1}$
37	36	nfel2	$⊢ Ⅎ k ⟨x, y⟩ \in {⋃_{k \in D} (\{k\} \times E)}^{-1}$
38	34 37	nfbi	$⊢ Ⅎ k (⟨x, y⟩ \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow ⟨x, y⟩ \in {⋃_{k \in D} (\{k\} \times E)}^{-1})$
39	33 38	nfim	$⊢ Ⅎ k (φ \to (⟨x, y⟩ \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow ⟨x, y⟩ \in {⋃_{k \in D} (\{k\} \times E)}^{-1}))$
40		opeq2	$⊢ k = y \to ⟨x, k⟩ = ⟨x, y⟩$
41	40	eleq1d	$⊢ k = y \to (⟨x, k⟩ \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow ⟨x, y⟩ \in ⋃_{j \in A} (\{j\} \times C))$
42	40	eleq1d	$⊢ k = y \to (⟨x, k⟩ \in {⋃_{k \in D} (\{k\} \times E)}^{-1} \leftrightarrow ⟨x, y⟩ \in {⋃_{k \in D} (\{k\} \times E)}^{-1})$
43	41 42	bibi12d	$⊢ k = y \to ((⟨x, k⟩ \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow ⟨x, k⟩ \in {⋃_{k \in D} (\{k\} \times E)}^{-1}) \leftrightarrow (⟨x, y⟩ \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow ⟨x, y⟩ \in {⋃_{k \in D} (\{k\} \times E)}^{-1}))$
44	43	imbi2d	$⊢ k = y \to ((φ \to (⟨x, k⟩ \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow ⟨x, k⟩ \in {⋃_{k \in D} (\{k\} \times E)}^{-1})) \leftrightarrow (φ \to (⟨x, y⟩ \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow ⟨x, y⟩ \in {⋃_{k \in D} (\{k\} \times E)}^{-1})))$
45		nfv	$⊢ Ⅎ j φ$
46		nfiu1	$⊢ \underline{Ⅎ} j ⋃_{j \in A} (\{j\} \times C)$
47	46	nfel2	$⊢ Ⅎ j ⟨x, k⟩ \in ⋃_{j \in A} (\{j\} \times C)$
48		nfv	$⊢ Ⅎ j ⟨x, k⟩ \in {⋃_{k \in D} (\{k\} \times E)}^{-1}$
49	47 48	nfbi	$⊢ Ⅎ j (⟨x, k⟩ \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow ⟨x, k⟩ \in {⋃_{k \in D} (\{k\} \times E)}^{-1})$
50	45 49	nfim	$⊢ Ⅎ j (φ \to (⟨x, k⟩ \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow ⟨x, k⟩ \in {⋃_{k \in D} (\{k\} \times E)}^{-1}))$
51		opeq1	$⊢ j = x \to ⟨j, k⟩ = ⟨x, k⟩$
52	51	eleq1d	$⊢ j = x \to (⟨j, k⟩ \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow ⟨x, k⟩ \in ⋃_{j \in A} (\{j\} \times C))$
53	51	eleq1d	$⊢ j = x \to (⟨j, k⟩ \in {⋃_{k \in D} (\{k\} \times E)}^{-1} \leftrightarrow ⟨x, k⟩ \in {⋃_{k \in D} (\{k\} \times E)}^{-1})$
54	52 53	bibi12d	$⊢ j = x \to ((⟨j, k⟩ \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow ⟨j, k⟩ \in {⋃_{k \in D} (\{k\} \times E)}^{-1}) \leftrightarrow (⟨x, k⟩ \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow ⟨x, k⟩ \in {⋃_{k \in D} (\{k\} \times E)}^{-1}))$
55	54	imbi2d	$⊢ j = x \to ((φ \to (⟨j, k⟩ \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow ⟨j, k⟩ \in {⋃_{k \in D} (\{k\} \times E)}^{-1})) \leftrightarrow (φ \to (⟨x, k⟩ \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow ⟨x, k⟩ \in {⋃_{k \in D} (\{k\} \times E)}^{-1})))$
56		opeliunxp	$⊢ ⟨j, k⟩ \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow (j \in A \land k \in C)$
57		opeliunxp	$⊢ ⟨k, j⟩ \in ⋃_{k \in D} (\{k\} \times E) \leftrightarrow (k \in D \land j \in E)$
58	10 56 57	3bitr4g	$⊢ φ \to (⟨j, k⟩ \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow ⟨k, j⟩ \in ⋃_{k \in D} (\{k\} \times E))$
59		vex	$⊢ j \in V$
60		vex	$⊢ k \in V$
61	59 60	opelcnv	$⊢ ⟨j, k⟩ \in {⋃_{k \in D} (\{k\} \times E)}^{-1} \leftrightarrow ⟨k, j⟩ \in ⋃_{k \in D} (\{k\} \times E)$
62	58 61	bitr4di	$⊢ φ \to (⟨j, k⟩ \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow ⟨j, k⟩ \in {⋃_{k \in D} (\{k\} \times E)}^{-1})$
63	50 55 62	chvarfv	$⊢ φ \to (⟨x, k⟩ \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow ⟨x, k⟩ \in {⋃_{k \in D} (\{k\} \times E)}^{-1})$
64	39 44 63	chvarfv	$⊢ φ \to (⟨x, y⟩ \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow ⟨x, y⟩ \in {⋃_{k \in D} (\{k\} \times E)}^{-1})$
65	31 32 64	eqrelrdv	$⊢ φ \to ⋃_{j \in A} (\{j\} \times C) = {⋃_{k \in D} (\{k\} \times E)}^{-1}$
66	65	f1oeq3d	$⊢ φ \to ((z \in ⋃_{k \in D} (\{k\} \times E) ⟼ ⋃ {\{z\}}^{-1}) : ⋃_{k \in D} (\{k\} \times E) \underset{1-1 onto}{⟶} ⋃_{j \in A} (\{j\} \times C) \leftrightarrow (z \in ⋃_{k \in D} (\{k\} \times E) ⟼ ⋃ {\{z\}}^{-1}) : ⋃_{k \in D} (\{k\} \times E) \underset{1-1 onto}{⟶} {⋃_{k \in D} (\{k\} \times E)}^{-1})$
67	27 66	mpbiri	$⊢ φ \to (z \in ⋃_{k \in D} (\{k\} \times E) ⟼ ⋃ {\{z\}}^{-1}) : ⋃_{k \in D} (\{k\} \times E) \underset{1-1 onto}{⟶} ⋃_{j \in A} (\{j\} \times C)$
68	1 2 3 16 20 21 67	gsumf1o	$⊢ φ \to \sum_{G} (j \in A, k \in C ⟼ X) = \sum_{G} ((j \in A, k \in C ⟼ X) \circ (z \in ⋃_{k \in D} (\{k\} \times E) ⟼ ⋃ {\{z\}}^{-1}))$
69		sneq	$⊢ z = ⟨x, y⟩ \to \{z\} = \{⟨x, y⟩\}$
70	69	cnveqd	$⊢ z = ⟨x, y⟩ \to {\{z\}}^{-1} = {\{⟨x, y⟩\}}^{-1}$
71	70	unieqd	$⊢ z = ⟨x, y⟩ \to ⋃ {\{z\}}^{-1} = ⋃ {\{⟨x, y⟩\}}^{-1}$
72		opswap	$⊢ ⋃ {\{⟨x, y⟩\}}^{-1} = ⟨y, x⟩$
73	71 72	eqtrdi	$⊢ z = ⟨x, y⟩ \to ⋃ {\{z\}}^{-1} = ⟨y, x⟩$
74	73	fveq2d	$⊢ z = ⟨x, y⟩ \to (j \in A, k \in C ⟼ X) (⋃ {\{z\}}^{-1}) = (j \in A, k \in C ⟼ X) (⟨y, x⟩)$
75		df-ov	$⊢ y (j \in A, k \in C ⟼ X) x = (j \in A, k \in C ⟼ X) (⟨y, x⟩)$
76	74 75	eqtr4di	$⊢ z = ⟨x, y⟩ \to (j \in A, k \in C ⟼ X) (⋃ {\{z\}}^{-1}) = y (j \in A, k \in C ⟼ X) x$
77	76	mpomptx	$⊢ (z \in ⋃_{x \in D} (\{x\} \times ⦋ x / k ⦌ E) ⟼ (j \in A, k \in C ⟼ X) (⋃ {\{z\}}^{-1})) = (x \in D, y \in ⦋ x / k ⦌ E ⟼ y (j \in A, k \in C ⟼ X) x)$
78		nfcv	$⊢ \underline{Ⅎ} x (\{k\} \times E)$
79		nfcv	$⊢ \underline{Ⅎ} k \{x\}$
80		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ x / k ⦌ E$
81	79 80	nfxp	$⊢ \underline{Ⅎ} k (\{x\} \times ⦋ x / k ⦌ E)$
82		sneq	$⊢ k = x \to \{k\} = \{x\}$
83		csbeq1a	$⊢ k = x \to E = ⦋ x / k ⦌ E$
84	82 83	xpeq12d	$⊢ k = x \to \{k\} \times E = \{x\} \times ⦋ x / k ⦌ E$
85	78 81 84	cbviun	$⊢ ⋃_{k \in D} (\{k\} \times E) = ⋃_{x \in D} (\{x\} \times ⦋ x / k ⦌ E)$
86	85	mpteq1i	$⊢ (z \in ⋃_{k \in D} (\{k\} \times E) ⟼ (j \in A, k \in C ⟼ X) (⋃ {\{z\}}^{-1})) = (z \in ⋃_{x \in D} (\{x\} \times ⦋ x / k ⦌ E) ⟼ (j \in A, k \in C ⟼ X) (⋃ {\{z\}}^{-1}))$
87		nfcv	$⊢ \underline{Ⅎ} x E$
88		nfcv	$⊢ \underline{Ⅎ} x (j (j \in A, k \in C ⟼ X) k)$
89		nfcv	$⊢ \underline{Ⅎ} y (j (j \in A, k \in C ⟼ X) k)$
90		nfcv	$⊢ \underline{Ⅎ} k y$
91		nfmpo2	$⊢ \underline{Ⅎ} k (j \in A, k \in C ⟼ X)$
92		nfcv	$⊢ \underline{Ⅎ} k x$
93	90 91 92	nfov	$⊢ \underline{Ⅎ} k (y (j \in A, k \in C ⟼ X) x)$
94		nfcv	$⊢ \underline{Ⅎ} j y$
95		nfmpo1	$⊢ \underline{Ⅎ} j (j \in A, k \in C ⟼ X)$
96		nfcv	$⊢ \underline{Ⅎ} j x$
97	94 95 96	nfov	$⊢ \underline{Ⅎ} j (y (j \in A, k \in C ⟼ X) x)$
98		oveq2	$⊢ k = x \to j (j \in A, k \in C ⟼ X) k = j (j \in A, k \in C ⟼ X) x$
99		oveq1	$⊢ j = y \to j (j \in A, k \in C ⟼ X) x = y (j \in A, k \in C ⟼ X) x$
100	98 99	sylan9eq	$⊢ (k = x \land j = y) \to j (j \in A, k \in C ⟼ X) k = y (j \in A, k \in C ⟼ X) x$
101	87 80 88 89 93 97 83 100	cbvmpox	$⊢ (k \in D, j \in E ⟼ j (j \in A, k \in C ⟼ X) k) = (x \in D, y \in ⦋ x / k ⦌ E ⟼ y (j \in A, k \in C ⟼ X) x)$
102	77 86 101	3eqtr4i	$⊢ (z \in ⋃_{k \in D} (\{k\} \times E) ⟼ (j \in A, k \in C ⟼ X) (⋃ {\{z\}}^{-1})) = (k \in D, j \in E ⟼ j (j \in A, k \in C ⟼ X) k)$
103		f1of	$⊢ (z \in ⋃_{k \in D} (\{k\} \times E) ⟼ ⋃ {\{z\}}^{-1}) : ⋃_{k \in D} (\{k\} \times E) \underset{1-1 onto}{⟶} ⋃_{j \in A} (\{j\} \times C) \to (z \in ⋃_{k \in D} (\{k\} \times E) ⟼ ⋃ {\{z\}}^{-1}) : ⋃_{k \in D} (\{k\} \times E) ⟶ ⋃_{j \in A} (\{j\} \times C)$
104	67 103	syl	$⊢ φ \to (z \in ⋃_{k \in D} (\{k\} \times E) ⟼ ⋃ {\{z\}}^{-1}) : ⋃_{k \in D} (\{k\} \times E) ⟶ ⋃_{j \in A} (\{j\} \times C)$
105		eqid	$⊢ (z \in ⋃_{k \in D} (\{k\} \times E) ⟼ ⋃ {\{z\}}^{-1}) = (z \in ⋃_{k \in D} (\{k\} \times E) ⟼ ⋃ {\{z\}}^{-1})$
106	105	fmpt	$⊢ \forall z \in ⋃_{k \in D} (\{k\} \times E) ⋃ {\{z\}}^{-1} \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow (z \in ⋃_{k \in D} (\{k\} \times E) ⟼ ⋃ {\{z\}}^{-1}) : ⋃_{k \in D} (\{k\} \times E) ⟶ ⋃_{j \in A} (\{j\} \times C)$
107	104 106	sylibr	$⊢ φ \to \forall z \in ⋃_{k \in D} (\{k\} \times E) ⋃ {\{z\}}^{-1} \in ⋃_{j \in A} (\{j\} \times C)$
108		eqidd	$⊢ φ \to (z \in ⋃_{k \in D} (\{k\} \times E) ⟼ ⋃ {\{z\}}^{-1}) = (z \in ⋃_{k \in D} (\{k\} \times E) ⟼ ⋃ {\{z\}}^{-1})$
109	20	feqmptd	$⊢ φ \to (j \in A, k \in C ⟼ X) = (x \in ⋃_{j \in A} (\{j\} \times C) ⟼ (j \in A, k \in C ⟼ X) (x))$
110		fveq2	$⊢ x = ⋃ {\{z\}}^{-1} \to (j \in A, k \in C ⟼ X) (x) = (j \in A, k \in C ⟼ X) (⋃ {\{z\}}^{-1})$
111	107 108 109 110	fmptcof	$⊢ φ \to (j \in A, k \in C ⟼ X) \circ (z \in ⋃_{k \in D} (\{k\} \times E) ⟼ ⋃ {\{z\}}^{-1}) = (z \in ⋃_{k \in D} (\{k\} \times E) ⟼ (j \in A, k \in C ⟼ X) (⋃ {\{z\}}^{-1}))$
112	6	ex	$⊢ φ \to ((j \in A \land k \in C) \to X \in B)$
113	18	ovmpt4g	$⊢ (j \in A \land k \in C \land X \in B) \to j (j \in A, k \in C ⟼ X) k = X$
114	113	3expia	$⊢ (j \in A \land k \in C) \to (X \in B \to j (j \in A, k \in C ⟼ X) k = X)$
115	112 114	sylcom	$⊢ φ \to ((j \in A \land k \in C) \to j (j \in A, k \in C ⟼ X) k = X)$
116	10 115	sylbird	$⊢ φ \to ((k \in D \land j \in E) \to j (j \in A, k \in C ⟼ X) k = X)$
117	116	3impib	$⊢ (φ \land k \in D \land j \in E) \to j (j \in A, k \in C ⟼ X) k = X$
118	117	eqcomd	$⊢ (φ \land k \in D \land j \in E) \to X = j (j \in A, k \in C ⟼ X) k$
119	118	mpoeq3dva	$⊢ φ \to (k \in D, j \in E ⟼ X) = (k \in D, j \in E ⟼ j (j \in A, k \in C ⟼ X) k)$
120	102 111 119	3eqtr4a	$⊢ φ \to (j \in A, k \in C ⟼ X) \circ (z \in ⋃_{k \in D} (\{k\} \times E) ⟼ ⋃ {\{z\}}^{-1}) = (k \in D, j \in E ⟼ X)$
121	120	oveq2d	$⊢ φ \to \sum_{G} ((j \in A, k \in C ⟼ X) \circ (z \in ⋃_{k \in D} (\{k\} \times E) ⟼ ⋃ {\{z\}}^{-1})) = \sum_{G} (k \in D, j \in E ⟼ X)$
122	68 121	eqtrd	$⊢ φ \to \sum_{G} (j \in A, k \in C ⟼ X) = \sum_{G} (k \in D, j \in E ⟼ X)$

Metamath Proof Explorer

Theorem gsumcom2

Proof