gsummpt2d

Description: Express a finite sum over a two-dimensional range as a double sum. See also gsum2d . (Contributed by Thierry Arnoux, 27-Apr-2020)

	Ref	Expression
Hypotheses	gsummpt2d.c	$⊢ \underline{Ⅎ} z C$
	gsummpt2d.0	$⊢ Ⅎ y φ$
	gsummpt2d.b	$⊢ B = {Base}_{W}$
	gsummpt2d.1	$⊢ x = ⟨y, z⟩ \to C = D$
	gsummpt2d.r	$⊢ φ \to Rel A$
	gsummpt2d.2	$⊢ φ \to A \in Fin$
	gsummpt2d.m	$⊢ φ \to W \in CMnd$
	gsummpt2d.3	$⊢ (φ \land x \in A) \to C \in B$
Assertion	gsummpt2d	$⊢ φ \to \underset{x \in A}{\sum_{W}} C = \underset{y \in dom A}{\sum_{W}} (\underset{z \in A [\{y\}]}{\sum_{W}}, D)$

Proof

Step	Hyp	Ref	Expression
1		gsummpt2d.c	$⊢ \underline{Ⅎ} z C$
2		gsummpt2d.0	$⊢ Ⅎ y φ$
3		gsummpt2d.b	$⊢ B = {Base}_{W}$
4		gsummpt2d.1	$⊢ x = ⟨y, z⟩ \to C = D$
5		gsummpt2d.r	$⊢ φ \to Rel A$
6		gsummpt2d.2	$⊢ φ \to A \in Fin$
7		gsummpt2d.m	$⊢ φ \to W \in CMnd$
8		gsummpt2d.3	$⊢ (φ \land x \in A) \to C \in B$
9		eqid	$⊢ 0_{W} = 0_{W}$
10	6	dmexd	$⊢ φ \to dom A \in V$
11		1stdm	$⊢ (Rel A \land x \in A) \to 1^{st} (x) \in dom A$
12	5 11	sylan	$⊢ (φ \land x \in A) \to 1^{st} (x) \in dom A$
13		fo1st	$⊢ 1^{st} : V \underset{onto}{⟶} V$
14		fofn	$⊢ 1^{st} : V \underset{onto}{⟶} V \to 1^{st} Fn V$
15		dffn5	$⊢ 1^{st} Fn V \leftrightarrow 1^{st} = (x \in V ⟼ 1^{st} (x))$
16	15	biimpi	$⊢ 1^{st} Fn V \to 1^{st} = (x \in V ⟼ 1^{st} (x))$
17	13 14 16	mp2b	$⊢ 1^{st} = (x \in V ⟼ 1^{st} (x))$
18	17	reseq1i	$⊢ {1^{st} ↾}_{A} = {(x \in V ⟼ 1^{st} (x)) ↾}_{A}$
19		ssv	$⊢ A \subseteq V$
20		resmpt	$⊢ A \subseteq V \to {(x \in V ⟼ 1^{st} (x)) ↾}_{A} = (x \in A ⟼ 1^{st} (x))$
21	19 20	ax-mp	$⊢ {(x \in V ⟼ 1^{st} (x)) ↾}_{A} = (x \in A ⟼ 1^{st} (x))$
22	18 21	eqtri	$⊢ {1^{st} ↾}_{A} = (x \in A ⟼ 1^{st} (x))$
23	3 9 7 6 10 8 12 22	gsummpt2co	$⊢ φ \to \underset{x \in A}{\sum_{W}} C = \underset{y \in dom A}{\sum_{W}} (\underset{x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}]}{\sum_{W}}, C)$
24	7	adantr	$⊢ (φ \land y \in dom A) \to W \in CMnd$
25	6	adantr	$⊢ (φ \land y \in dom A) \to A \in Fin$
26		imaexg	$⊢ A \in Fin \to A [\{y\}] \in V$
27	25 26	syl	$⊢ (φ \land y \in dom A) \to A [\{y\}] \in V$
28	4	adantl	$⊢ ((((φ \land y \in dom A) \land z \in A [\{y\}]) \land x \in A) \land x = ⟨y, z⟩) \to C = D$
29		simp-4l	$⊢ ((((φ \land y \in dom A) \land z \in A [\{y\}]) \land x \in A) \land x = ⟨y, z⟩) \to φ$
30		simplr	$⊢ ((((φ \land y \in dom A) \land z \in A [\{y\}]) \land x \in A) \land x = ⟨y, z⟩) \to x \in A$
31	29 30 8	syl2anc	$⊢ ((((φ \land y \in dom A) \land z \in A [\{y\}]) \land x \in A) \land x = ⟨y, z⟩) \to C \in B$
32	28 31	eqeltrrd	$⊢ ((((φ \land y \in dom A) \land z \in A [\{y\}]) \land x \in A) \land x = ⟨y, z⟩) \to D \in B$
33		vex	$⊢ y \in V$
34		vex	$⊢ z \in V$
35	33 34	elimasn	$⊢ z \in A [\{y\}] \leftrightarrow ⟨y, z⟩ \in A$
36	35	biimpi	$⊢ z \in A [\{y\}] \to ⟨y, z⟩ \in A$
37	36	adantl	$⊢ ((φ \land y \in dom A) \land z \in A [\{y\}]) \to ⟨y, z⟩ \in A$
38		simpr	$⊢ (((φ \land y \in dom A) \land z \in A [\{y\}]) \land x = ⟨y, z⟩) \to x = ⟨y, z⟩$
39	38	eqeq1d	$⊢ (((φ \land y \in dom A) \land z \in A [\{y\}]) \land x = ⟨y, z⟩) \to (x = ⟨y, z⟩ \leftrightarrow ⟨y, z⟩ = ⟨y, z⟩)$
40		eqidd	$⊢ ((φ \land y \in dom A) \land z \in A [\{y\}]) \to ⟨y, z⟩ = ⟨y, z⟩$
41	37 39 40	rspcedvd	$⊢ ((φ \land y \in dom A) \land z \in A [\{y\}]) \to \exists x \in A x = ⟨y, z⟩$
42	32 41	r19.29a	$⊢ ((φ \land y \in dom A) \land z \in A [\{y\}]) \to D \in B$
43	42	fmpttd	$⊢ (φ \land y \in dom A) \to (z \in A [\{y\}] ⟼ D) : A [\{y\}] ⟶ B$
44		eqid	$⊢ (z \in A [\{y\}] ⟼ D) = (z \in A [\{y\}] ⟼ D)$
45		imafi2	$⊢ A \in Fin \to A [\{y\}] \in Fin$
46	6 45	syl	$⊢ φ \to A [\{y\}] \in Fin$
47	46	adantr	$⊢ (φ \land y \in dom A) \to A [\{y\}] \in Fin$
48		fvex	$⊢ 0_{W} \in V$
49	48	a1i	$⊢ (φ \land y \in dom A) \to 0_{W} \in V$
50	44 47 42 49	fsuppmptdm	$⊢ (φ \land y \in dom A) \to {finSupp}_{0_{W}} ((z \in A [\{y\}] ⟼ D))$
51		2ndconst	$⊢ y \in dom A \to ({2^{nd} ↾}_{(\{y\} \times A [\{y\}])}) : \{y\} \times A [\{y\}] \underset{1-1 onto}{⟶} A [\{y\}]$
52	51	adantl	$⊢ (φ \land y \in dom A) \to ({2^{nd} ↾}_{(\{y\} \times A [\{y\}])}) : \{y\} \times A [\{y\}] \underset{1-1 onto}{⟶} A [\{y\}]$
53		1stpreimas	$⊢ (Rel A \land y \in dom A) \to {({1^{st} ↾}_{A})}^{-1} [\{y\}] = \{y\} \times A [\{y\}]$
54	5 53	sylan	$⊢ (φ \land y \in dom A) \to {({1^{st} ↾}_{A})}^{-1} [\{y\}] = \{y\} \times A [\{y\}]$
55	54	reseq2d	$⊢ (φ \land y \in dom A) \to {2^{nd} ↾}_{{({1^{st} ↾}_{A})}^{-1} [\{y\}]} = {2^{nd} ↾}_{(\{y\} \times A [\{y\}])}$
56		f1oeq1	$⊢ {2^{nd} ↾}_{{({1^{st} ↾}_{A})}^{-1} [\{y\}]} = {2^{nd} ↾}_{(\{y\} \times A [\{y\}])} \to (({2^{nd} ↾}_{{({1^{st} ↾}_{A})}^{-1} [\{y\}]}) : \{y\} \times A [\{y\}] \underset{1-1 onto}{⟶} A [\{y\}] \leftrightarrow ({2^{nd} ↾}_{(\{y\} \times A [\{y\}])}) : \{y\} \times A [\{y\}] \underset{1-1 onto}{⟶} A [\{y\}])$
57	55 56	syl	$⊢ (φ \land y \in dom A) \to (({2^{nd} ↾}_{{({1^{st} ↾}_{A})}^{-1} [\{y\}]}) : \{y\} \times A [\{y\}] \underset{1-1 onto}{⟶} A [\{y\}] \leftrightarrow ({2^{nd} ↾}_{(\{y\} \times A [\{y\}])}) : \{y\} \times A [\{y\}] \underset{1-1 onto}{⟶} A [\{y\}])$
58	52 57	mpbird	$⊢ (φ \land y \in dom A) \to ({2^{nd} ↾}_{{({1^{st} ↾}_{A})}^{-1} [\{y\}]}) : \{y\} \times A [\{y\}] \underset{1-1 onto}{⟶} A [\{y\}]$
59	3 9 24 27 43 50 58	gsumf1o	$⊢ (φ \land y \in dom A) \to \underset{z \in A [\{y\}]}{\sum_{W}} D = \sum_{W} ((z \in A [\{y\}] ⟼ D) \circ ({2^{nd} ↾}_{{({1^{st} ↾}_{A})}^{-1} [\{y\}]}))$
60		simpr	$⊢ ((φ \land y \in dom A) \land x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}]) \to x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}]$
61	54	adantr	$⊢ ((φ \land y \in dom A) \land x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}]) \to {({1^{st} ↾}_{A})}^{-1} [\{y\}] = \{y\} \times A [\{y\}]$
62	60 61	eleqtrd	$⊢ ((φ \land y \in dom A) \land x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}]) \to x \in (\{y\} \times A [\{y\}])$
63		xp2nd	$⊢ x \in (\{y\} \times A [\{y\}]) \to 2^{nd} (x) \in A [\{y\}]$
64	62 63	syl	$⊢ ((φ \land y \in dom A) \land x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}]) \to 2^{nd} (x) \in A [\{y\}]$
65	64	ralrimiva	$⊢ (φ \land y \in dom A) \to \forall x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}] 2^{nd} (x) \in A [\{y\}]$
66		fo2nd	$⊢ 2^{nd} : V \underset{onto}{⟶} V$
67		fofn	$⊢ 2^{nd} : V \underset{onto}{⟶} V \to 2^{nd} Fn V$
68		dffn5	$⊢ 2^{nd} Fn V \leftrightarrow 2^{nd} = (x \in V ⟼ 2^{nd} (x))$
69	68	biimpi	$⊢ 2^{nd} Fn V \to 2^{nd} = (x \in V ⟼ 2^{nd} (x))$
70	66 67 69	mp2b	$⊢ 2^{nd} = (x \in V ⟼ 2^{nd} (x))$
71	70	reseq1i	$⊢ {2^{nd} ↾}_{{({1^{st} ↾}_{A})}^{-1} [\{y\}]} = {(x \in V ⟼ 2^{nd} (x)) ↾}_{{({1^{st} ↾}_{A})}^{-1} [\{y\}]}$
72		ssv	$⊢ {({1^{st} ↾}_{A})}^{-1} [\{y\}] \subseteq V$
73		resmpt	$⊢ {({1^{st} ↾}_{A})}^{-1} [\{y\}] \subseteq V \to {(x \in V ⟼ 2^{nd} (x)) ↾}_{{({1^{st} ↾}_{A})}^{-1} [\{y\}]} = (x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}] ⟼ 2^{nd} (x))$
74	72 73	ax-mp	$⊢ {(x \in V ⟼ 2^{nd} (x)) ↾}_{{({1^{st} ↾}_{A})}^{-1} [\{y\}]} = (x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}] ⟼ 2^{nd} (x))$
75	71 74	eqtri	$⊢ {2^{nd} ↾}_{{({1^{st} ↾}_{A})}^{-1} [\{y\}]} = (x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}] ⟼ 2^{nd} (x))$
76	75	a1i	$⊢ (φ \land y \in dom A) \to {2^{nd} ↾}_{{({1^{st} ↾}_{A})}^{-1} [\{y\}]} = (x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}] ⟼ 2^{nd} (x))$
77		eqidd	$⊢ (φ \land y \in dom A) \to (z \in A [\{y\}] ⟼ D) = (z \in A [\{y\}] ⟼ D)$
78	65 76 77	fmptcos	$⊢ (φ \land y \in dom A) \to (z \in A [\{y\}] ⟼ D) \circ ({2^{nd} ↾}_{{({1^{st} ↾}_{A})}^{-1} [\{y\}]}) = (x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}] ⟼ ⦋ 2^{nd} (x) / z ⦌ D)$
79		nfv	$⊢ Ⅎ z ((φ \land y \in dom A) \land x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}])$
80	1	a1i	$⊢ ((φ \land y \in dom A) \land x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}]) \to \underline{Ⅎ} z C$
81	62	adantr	$⊢ (((φ \land y \in dom A) \land x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}]) \land z = 2^{nd} (x)) \to x \in (\{y\} \times A [\{y\}])$
82		xp1st	$⊢ x \in (\{y\} \times A [\{y\}]) \to 1^{st} (x) \in \{y\}$
83	81 82	syl	$⊢ (((φ \land y \in dom A) \land x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}]) \land z = 2^{nd} (x)) \to 1^{st} (x) \in \{y\}$
84		fvex	$⊢ 1^{st} (x) \in V$
85	84	elsn	$⊢ 1^{st} (x) \in \{y\} \leftrightarrow 1^{st} (x) = y$
86	83 85	sylib	$⊢ (((φ \land y \in dom A) \land x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}]) \land z = 2^{nd} (x)) \to 1^{st} (x) = y$
87		simpr	$⊢ (((φ \land y \in dom A) \land x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}]) \land z = 2^{nd} (x)) \to z = 2^{nd} (x)$
88	87	eqcomd	$⊢ (((φ \land y \in dom A) \land x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}]) \land z = 2^{nd} (x)) \to 2^{nd} (x) = z$
89		eqopi	$⊢ (x \in (\{y\} \times A [\{y\}]) \land (1^{st} (x) = y \land 2^{nd} (x) = z)) \to x = ⟨y, z⟩$
90	81 86 88 89	syl12anc	$⊢ (((φ \land y \in dom A) \land x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}]) \land z = 2^{nd} (x)) \to x = ⟨y, z⟩$
91	90 4	syl	$⊢ (((φ \land y \in dom A) \land x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}]) \land z = 2^{nd} (x)) \to C = D$
92	91	eqcomd	$⊢ (((φ \land y \in dom A) \land x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}]) \land z = 2^{nd} (x)) \to D = C$
93	79 80 64 92	csbiedf	$⊢ ((φ \land y \in dom A) \land x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}]) \to ⦋ 2^{nd} (x) / z ⦌ D = C$
94	93	mpteq2dva	$⊢ (φ \land y \in dom A) \to (x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}] ⟼ ⦋ 2^{nd} (x) / z ⦌ D) = (x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}] ⟼ C)$
95	78 94	eqtrd	$⊢ (φ \land y \in dom A) \to (z \in A [\{y\}] ⟼ D) \circ ({2^{nd} ↾}_{{({1^{st} ↾}_{A})}^{-1} [\{y\}]}) = (x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}] ⟼ C)$
96	95	oveq2d	$⊢ (φ \land y \in dom A) \to \sum_{W} ((z \in A [\{y\}] ⟼ D) \circ ({2^{nd} ↾}_{{({1^{st} ↾}_{A})}^{-1} [\{y\}]})) = \underset{x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}]}{\sum_{W}} C$
97	59 96	eqtr2d	$⊢ (φ \land y \in dom A) \to \underset{x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}]}{\sum_{W}} C = \underset{z \in A [\{y\}]}{\sum_{W}} D$
98	2 97	mpteq2da	$⊢ φ \to (y \in dom A ⟼ \underset{x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}]}{\sum_{W}} C) = (y \in dom A ⟼ \underset{z \in A [\{y\}]}{\sum_{W}} D)$
99	98	oveq2d	$⊢ φ \to \underset{y \in dom A}{\sum_{W}} (\underset{x \in {({1^{st} ↾}_{A})}^{-1} [\{y\}]}{\sum_{W}}, C) = \underset{y \in dom A}{\sum_{W}} (\underset{z \in A [\{y\}]}{\sum_{W}}, D)$
100	23 99	eqtrd	$⊢ φ \to \underset{x \in A}{\sum_{W}} C = \underset{y \in dom A}{\sum_{W}} (\underset{z \in A [\{y\}]}{\sum_{W}}, D)$

Metamath Proof Explorer

Theorem gsummpt2d

Proof