fsumvma

Description: Rewrite a sum over the von Mangoldt function as a sum over prime powers. (Contributed by Mario Carneiro, 15-Apr-2016)

	Ref	Expression
Hypotheses	fsumvma.1	$⊢ x = p^{k} \to B = C$
	fsumvma.2	$⊢ φ \to A \in Fin$
	fsumvma.3	$⊢ φ \to A \subseteq ℕ$
	fsumvma.4	$⊢ φ \to P \in Fin$
	fsumvma.5	$⊢ φ \to ((p \in P \land k \in K) \leftrightarrow ((p \in ℙ \land k \in ℕ) \land p^{k} \in A))$
	fsumvma.6	$⊢ (φ \land x \in A) \to B \in ℂ$
	fsumvma.7	$⊢ (φ \land (x \in A \land Λ (x) = 0)) \to B = 0$
Assertion	fsumvma	$⊢ φ \to \sum_{x \in A} B = \sum_{p \in P} \sum_{k \in K} C$

Proof

Step	Hyp	Ref	Expression
1		fsumvma.1	$⊢ x = p^{k} \to B = C$
2		fsumvma.2	$⊢ φ \to A \in Fin$
3		fsumvma.3	$⊢ φ \to A \subseteq ℕ$
4		fsumvma.4	$⊢ φ \to P \in Fin$
5		fsumvma.5	$⊢ φ \to ((p \in P \land k \in K) \leftrightarrow ((p \in ℙ \land k \in ℕ) \land p^{k} \in A))$
6		fsumvma.6	$⊢ (φ \land x \in A) \to B \in ℂ$
7		fsumvma.7	$⊢ (φ \land (x \in A \land Λ (x) = 0)) \to B = 0$
8		fvexd	$⊢ z = ⟨p, k⟩ \to^(z) \in V$
9		fveq2	$⊢ z = ⟨p, k⟩ \to^(z) =^(⟨p, k⟩)$
10		df-ov	$⊢ p^{k} =^(⟨p, k⟩)$
11	9 10	eqtr4di	$⊢ z = ⟨p, k⟩ \to^(z) = p^{k}$
12	11	eqeq2d	$⊢ z = ⟨p, k⟩ \to (x =^(z) \leftrightarrow x = p^{k})$
13	12	biimpa	$⊢ (z = ⟨p, k⟩ \land x =^(z)) \to x = p^{k}$
14	13 1	syl	$⊢ (z = ⟨p, k⟩ \land x =^(z)) \to B = C$
15	8 14	csbied	$⊢ z = ⟨p, k⟩ \to ⦋^(z) / x ⦌ B = C$
16	2	adantr	$⊢ (φ \land p \in P) \to A \in Fin$
17	5	biimpd	$⊢ φ \to ((p \in P \land k \in K) \to ((p \in ℙ \land k \in ℕ) \land p^{k} \in A))$
18	17	impl	$⊢ ((φ \land p \in P) \land k \in K) \to ((p \in ℙ \land k \in ℕ) \land p^{k} \in A)$
19	18	simprd	$⊢ ((φ \land p \in P) \land k \in K) \to p^{k} \in A$
20	19	ex	$⊢ (φ \land p \in P) \to (k \in K \to p^{k} \in A)$
21	18	simpld	$⊢ ((φ \land p \in P) \land k \in K) \to (p \in ℙ \land k \in ℕ)$
22	21	simpld	$⊢ ((φ \land p \in P) \land k \in K) \to p \in ℙ$
23	22	adantrr	$⊢ ((φ \land p \in P) \land (k \in K \land z \in K)) \to p \in ℙ$
24	21	simprd	$⊢ ((φ \land p \in P) \land k \in K) \to k \in ℕ$
25	24	adantrr	$⊢ ((φ \land p \in P) \land (k \in K \land z \in K)) \to k \in ℕ$
26	24	ex	$⊢ (φ \land p \in P) \to (k \in K \to k \in ℕ)$
27	26	ssrdv	$⊢ (φ \land p \in P) \to K \subseteq ℕ$
28	27	sselda	$⊢ ((φ \land p \in P) \land z \in K) \to z \in ℕ$
29	28	adantrl	$⊢ ((φ \land p \in P) \land (k \in K \land z \in K)) \to z \in ℕ$
30		eqid	$⊢ p = p$
31		prmexpb	$⊢ ((p \in ℙ \land p \in ℙ) \land (k \in ℕ \land z \in ℕ)) \to (p^{k} = p^{z} \leftrightarrow (p = p \land k = z))$
32	31	baibd	$⊢ (((p \in ℙ \land p \in ℙ) \land (k \in ℕ \land z \in ℕ)) \land p = p) \to (p^{k} = p^{z} \leftrightarrow k = z)$
33	30 32	mpan2	$⊢ ((p \in ℙ \land p \in ℙ) \land (k \in ℕ \land z \in ℕ)) \to (p^{k} = p^{z} \leftrightarrow k = z)$
34	23 23 25 29 33	syl22anc	$⊢ ((φ \land p \in P) \land (k \in K \land z \in K)) \to (p^{k} = p^{z} \leftrightarrow k = z)$
35	34	ex	$⊢ (φ \land p \in P) \to ((k \in K \land z \in K) \to (p^{k} = p^{z} \leftrightarrow k = z))$
36	20 35	dom2lem	$⊢ (φ \land p \in P) \to (k \in K ⟼ p^{k}) : K \underset{1-1}{⟶} A$
37		f1fi	$⊢ (A \in Fin \land (k \in K ⟼ p^{k}) : K \underset{1-1}{⟶} A) \to K \in Fin$
38	16 36 37	syl2anc	$⊢ (φ \land p \in P) \to K \in Fin$
39	1	eleq1d	$⊢ x = p^{k} \to (B \in ℂ \leftrightarrow C \in ℂ)$
40	6	ralrimiva	$⊢ φ \to \forall x \in A B \in ℂ$
41	40	adantr	$⊢ (φ \land (p \in P \land k \in K)) \to \forall x \in A B \in ℂ$
42	5	simplbda	$⊢ (φ \land (p \in P \land k \in K)) \to p^{k} \in A$
43	39 41 42	rspcdva	$⊢ (φ \land (p \in P \land k \in K)) \to C \in ℂ$
44	15 4 38 43	fsum2d	$⊢ φ \to \sum_{p \in P} \sum_{k \in K} C = \sum_{z \in ⋃_{p \in P} (\{p\} \times K)} ⦋^(z) / x ⦌ B$
45		nfcv	$⊢ \underline{Ⅎ} y B$
46		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ B$
47		csbeq1a	$⊢ x = y \to B = ⦋ y / x ⦌ B$
48	45 46 47	cbvsumi	$⊢ \sum_{x \in ran (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a))} B = \sum_{y \in ran (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a))} ⦋ y / x ⦌ B$
49		csbeq1	$⊢ y =^(z) \to ⦋ y / x ⦌ B = ⦋^(z) / x ⦌ B$
50		snfi	$⊢ \{p\} \in Fin$
51		xpfi	$⊢ (\{p\} \in Fin \land K \in Fin) \to \{p\} \times K \in Fin$
52	50 38 51	sylancr	$⊢ (φ \land p \in P) \to \{p\} \times K \in Fin$
53	52	ralrimiva	$⊢ φ \to \forall p \in P \{p\} \times K \in Fin$
54		iunfi	$⊢ (P \in Fin \land \forall p \in P \{p\} \times K \in Fin) \to ⋃_{p \in P} (\{p\} \times K) \in Fin$
55	4 53 54	syl2anc	$⊢ φ \to ⋃_{p \in P} (\{p\} \times K) \in Fin$
56		fvex	$⊢^(a) \in V$
57	56	2a1i	$⊢ φ \to (a \in ⋃_{p \in P} (\{p\} \times K) \to^(a) \in V)$
58		eliunxp	$⊢ a \in ⋃_{p \in P} (\{p\} \times K) \leftrightarrow \exists p \exists k (a = ⟨p, k⟩ \land (p \in P \land k \in K))$
59	5	simprbda	$⊢ (φ \land (p \in P \land k \in K)) \to (p \in ℙ \land k \in ℕ)$
60		opelxp	$⊢ ⟨p, k⟩ \in (ℙ \times ℕ) \leftrightarrow (p \in ℙ \land k \in ℕ)$
61	59 60	sylibr	$⊢ (φ \land (p \in P \land k \in K)) \to ⟨p, k⟩ \in (ℙ \times ℕ)$
62		eleq1	$⊢ a = ⟨p, k⟩ \to (a \in (ℙ \times ℕ) \leftrightarrow ⟨p, k⟩ \in (ℙ \times ℕ))$
63	61 62	syl5ibrcom	$⊢ (φ \land (p \in P \land k \in K)) \to (a = ⟨p, k⟩ \to a \in (ℙ \times ℕ))$
64	63	impancom	$⊢ (φ \land a = ⟨p, k⟩) \to ((p \in P \land k \in K) \to a \in (ℙ \times ℕ))$
65	64	expimpd	$⊢ φ \to ((a = ⟨p, k⟩ \land (p \in P \land k \in K)) \to a \in (ℙ \times ℕ))$
66	65	exlimdvv	$⊢ φ \to (\exists p \exists k (a = ⟨p, k⟩ \land (p \in P \land k \in K)) \to a \in (ℙ \times ℕ))$
67	58 66	syl5bi	$⊢ φ \to (a \in ⋃_{p \in P} (\{p\} \times K) \to a \in (ℙ \times ℕ))$
68	67	ssrdv	$⊢ φ \to ⋃_{p \in P} (\{p\} \times K) \subseteq ℙ \times ℕ$
69	68	sseld	$⊢ φ \to (b \in ⋃_{p \in P} (\{p\} \times K) \to b \in (ℙ \times ℕ))$
70	67 69	anim12d	$⊢ φ \to ((a \in ⋃_{p \in P} (\{p\} \times K) \land b \in ⋃_{p \in P} (\{p\} \times K)) \to (a \in (ℙ \times ℕ) \land b \in (ℙ \times ℕ)))$
71		1st2nd2	$⊢ a \in (ℙ \times ℕ) \to a = ⟨1^{st} (a), 2^{nd} (a)⟩$
72	71	fveq2d	$⊢ a \in (ℙ \times ℕ) \to^(a) =^(⟨1^{st} (a), 2^{nd} (a)⟩)$
73		df-ov	$⊢ {1^{st} (a)}^{2^{nd} (a)} =^(⟨1^{st} (a), 2^{nd} (a)⟩)$
74	72 73	eqtr4di	$⊢ a \in (ℙ \times ℕ) \to^(a) = {1^{st} (a)}^{2^{nd} (a)}$
75		1st2nd2	$⊢ b \in (ℙ \times ℕ) \to b = ⟨1^{st} (b), 2^{nd} (b)⟩$
76	75	fveq2d	$⊢ b \in (ℙ \times ℕ) \to^(b) =^(⟨1^{st} (b), 2^{nd} (b)⟩)$
77		df-ov	$⊢ {1^{st} (b)}^{2^{nd} (b)} =^(⟨1^{st} (b), 2^{nd} (b)⟩)$
78	76 77	eqtr4di	$⊢ b \in (ℙ \times ℕ) \to^(b) = {1^{st} (b)}^{2^{nd} (b)}$
79	74 78	eqeqan12d	$⊢ (a \in (ℙ \times ℕ) \land b \in (ℙ \times ℕ)) \to (^(a) =^(b) \leftrightarrow {1^{st} (a)}^{2^{nd} (a)} = {1^{st} (b)}^{2^{nd} (b)})$
80		xp1st	$⊢ a \in (ℙ \times ℕ) \to 1^{st} (a) \in ℙ$
81		xp2nd	$⊢ a \in (ℙ \times ℕ) \to 2^{nd} (a) \in ℕ$
82	80 81	jca	$⊢ a \in (ℙ \times ℕ) \to (1^{st} (a) \in ℙ \land 2^{nd} (a) \in ℕ)$
83		xp1st	$⊢ b \in (ℙ \times ℕ) \to 1^{st} (b) \in ℙ$
84		xp2nd	$⊢ b \in (ℙ \times ℕ) \to 2^{nd} (b) \in ℕ$
85	83 84	jca	$⊢ b \in (ℙ \times ℕ) \to (1^{st} (b) \in ℙ \land 2^{nd} (b) \in ℕ)$
86		prmexpb	$⊢ ((1^{st} (a) \in ℙ \land 1^{st} (b) \in ℙ) \land (2^{nd} (a) \in ℕ \land 2^{nd} (b) \in ℕ)) \to ({1^{st} (a)}^{2^{nd} (a)} = {1^{st} (b)}^{2^{nd} (b)} \leftrightarrow (1^{st} (a) = 1^{st} (b) \land 2^{nd} (a) = 2^{nd} (b)))$
87	86	an4s	$⊢ ((1^{st} (a) \in ℙ \land 2^{nd} (a) \in ℕ) \land (1^{st} (b) \in ℙ \land 2^{nd} (b) \in ℕ)) \to ({1^{st} (a)}^{2^{nd} (a)} = {1^{st} (b)}^{2^{nd} (b)} \leftrightarrow (1^{st} (a) = 1^{st} (b) \land 2^{nd} (a) = 2^{nd} (b)))$
88	82 85 87	syl2an	$⊢ (a \in (ℙ \times ℕ) \land b \in (ℙ \times ℕ)) \to ({1^{st} (a)}^{2^{nd} (a)} = {1^{st} (b)}^{2^{nd} (b)} \leftrightarrow (1^{st} (a) = 1^{st} (b) \land 2^{nd} (a) = 2^{nd} (b)))$
89		xpopth	$⊢ (a \in (ℙ \times ℕ) \land b \in (ℙ \times ℕ)) \to ((1^{st} (a) = 1^{st} (b) \land 2^{nd} (a) = 2^{nd} (b)) \leftrightarrow a = b)$
90	79 88 89	3bitrd	$⊢ (a \in (ℙ \times ℕ) \land b \in (ℙ \times ℕ)) \to (^(a) =^(b) \leftrightarrow a = b)$
91	70 90	syl6	$⊢ φ \to ((a \in ⋃_{p \in P} (\{p\} \times K) \land b \in ⋃_{p \in P} (\{p\} \times K)) \to (^(a) =^(b) \leftrightarrow a = b))$
92	57 91	dom2lem	$⊢ φ \to (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a)) : ⋃_{p \in P} (\{p\} \times K) \underset{1-1}{⟶} V$
93		f1f1orn	$⊢ (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a)) : ⋃_{p \in P} (\{p\} \times K) \underset{1-1}{⟶} V \to (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a)) : ⋃_{p \in P} (\{p\} \times K) \underset{1-1 onto}{⟶} ran (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a))$
94	92 93	syl	$⊢ φ \to (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a)) : ⋃_{p \in P} (\{p\} \times K) \underset{1-1 onto}{⟶} ran (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a))$
95		fveq2	$⊢ a = z \to^(a) =^(z)$
96		eqid	$⊢ (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a)) = (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a))$
97		fvex	$⊢^(z) \in V$
98	95 96 97	fvmpt	$⊢ z \in ⋃_{p \in P} (\{p\} \times K) \to (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a)) (z) =^(z)$
99	98	adantl	$⊢ (φ \land z \in ⋃_{p \in P} (\{p\} \times K)) \to (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a)) (z) =^(z)$
100		fveq2	$⊢ a = ⟨p, k⟩ \to^(a) =^(⟨p, k⟩)$
101	100 10	eqtr4di	$⊢ a = ⟨p, k⟩ \to^(a) = p^{k}$
102	101	eleq1d	$⊢ a = ⟨p, k⟩ \to (^(a) \in A \leftrightarrow p^{k} \in A)$
103	42 102	syl5ibrcom	$⊢ (φ \land (p \in P \land k \in K)) \to (a = ⟨p, k⟩ \to^(a) \in A)$
104	103	impancom	$⊢ (φ \land a = ⟨p, k⟩) \to ((p \in P \land k \in K) \to^(a) \in A)$
105	104	expimpd	$⊢ φ \to ((a = ⟨p, k⟩ \land (p \in P \land k \in K)) \to^(a) \in A)$
106	105	exlimdvv	$⊢ φ \to (\exists p \exists k (a = ⟨p, k⟩ \land (p \in P \land k \in K)) \to^(a) \in A)$
107	58 106	syl5bi	$⊢ φ \to (a \in ⋃_{p \in P} (\{p\} \times K) \to^(a) \in A)$
108	107	imp	$⊢ (φ \land a \in ⋃_{p \in P} (\{p\} \times K)) \to^(a) \in A$
109	108	fmpttd	$⊢ φ \to (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a)) : ⋃_{p \in P} (\{p\} \times K) ⟶ A$
110	109	frnd	$⊢ φ \to ran (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a)) \subseteq A$
111	110	sselda	$⊢ (φ \land y \in ran (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a))) \to y \in A$
112	46	nfel1	$⊢ Ⅎ x ⦋ y / x ⦌ B \in ℂ$
113	47	eleq1d	$⊢ x = y \to (B \in ℂ \leftrightarrow ⦋ y / x ⦌ B \in ℂ)$
114	112 113	rspc	$⊢ y \in A \to (\forall x \in A B \in ℂ \to ⦋ y / x ⦌ B \in ℂ)$
115	40 114	mpan9	$⊢ (φ \land y \in A) \to ⦋ y / x ⦌ B \in ℂ$
116	111 115	syldan	$⊢ (φ \land y \in ran (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a))) \to ⦋ y / x ⦌ B \in ℂ$
117	49 55 94 99 116	fsumf1o	$⊢ φ \to \sum_{y \in ran (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a))} ⦋ y / x ⦌ B = \sum_{z \in ⋃_{p \in P} (\{p\} \times K)} ⦋^(z) / x ⦌ B$
118	48 117	syl5eq	$⊢ φ \to \sum_{x \in ran (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a))} B = \sum_{z \in ⋃_{p \in P} (\{p\} \times K)} ⦋^(z) / x ⦌ B$
119	110	sselda	$⊢ (φ \land x \in ran (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a))) \to x \in A$
120	119 6	syldan	$⊢ (φ \land x \in ran (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a))) \to B \in ℂ$
121		eldif	$⊢ x \in (A ∖ ran (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a))) \leftrightarrow (x \in A \land \neg x \in ran (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a)))$
122	96 56	elrnmpti	$⊢ x \in ran (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a)) \leftrightarrow \exists a \in ⋃_{p \in P} (\{p\} \times K) x =^(a)$
123	101	eqeq2d	$⊢ a = ⟨p, k⟩ \to (x =^(a) \leftrightarrow x = p^{k})$
124	123	rexiunxp	$⊢ \exists a \in ⋃_{p \in P} (\{p\} \times K) x =^(a) \leftrightarrow \exists p \in P \exists k \in K x = p^{k}$
125	122 124	bitri	$⊢ x \in ran (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a)) \leftrightarrow \exists p \in P \exists k \in K x = p^{k}$
126		simpr	$⊢ ((φ \land x \in A) \land x = p^{k}) \to x = p^{k}$
127		simplr	$⊢ ((φ \land x \in A) \land x = p^{k}) \to x \in A$
128	126 127	eqeltrrd	$⊢ ((φ \land x \in A) \land x = p^{k}) \to p^{k} \in A$
129	5	rbaibd	$⊢ (φ \land p^{k} \in A) \to ((p \in P \land k \in K) \leftrightarrow (p \in ℙ \land k \in ℕ))$
130	129	adantlr	$⊢ ((φ \land x \in A) \land p^{k} \in A) \to ((p \in P \land k \in K) \leftrightarrow (p \in ℙ \land k \in ℕ))$
131	128 130	syldan	$⊢ ((φ \land x \in A) \land x = p^{k}) \to ((p \in P \land k \in K) \leftrightarrow (p \in ℙ \land k \in ℕ))$
132	131	pm5.32da	$⊢ (φ \land x \in A) \to ((x = p^{k} \land (p \in P \land k \in K)) \leftrightarrow (x = p^{k} \land (p \in ℙ \land k \in ℕ)))$
133		ancom	$⊢ ((p \in P \land k \in K) \land x = p^{k}) \leftrightarrow (x = p^{k} \land (p \in P \land k \in K))$
134		ancom	$⊢ ((p \in ℙ \land k \in ℕ) \land x = p^{k}) \leftrightarrow (x = p^{k} \land (p \in ℙ \land k \in ℕ))$
135	132 133 134	3bitr4g	$⊢ (φ \land x \in A) \to (((p \in P \land k \in K) \land x = p^{k}) \leftrightarrow ((p \in ℙ \land k \in ℕ) \land x = p^{k}))$
136	135	2exbidv	$⊢ (φ \land x \in A) \to (\exists p \exists k ((p \in P \land k \in K) \land x = p^{k}) \leftrightarrow \exists p \exists k ((p \in ℙ \land k \in ℕ) \land x = p^{k}))$
137		r2ex	$⊢ \exists p \in P \exists k \in K x = p^{k} \leftrightarrow \exists p \exists k ((p \in P \land k \in K) \land x = p^{k})$
138		r2ex	$⊢ \exists p \in ℙ \exists k \in ℕ x = p^{k} \leftrightarrow \exists p \exists k ((p \in ℙ \land k \in ℕ) \land x = p^{k})$
139	136 137 138	3bitr4g	$⊢ (φ \land x \in A) \to (\exists p \in P \exists k \in K x = p^{k} \leftrightarrow \exists p \in ℙ \exists k \in ℕ x = p^{k})$
140	3	sselda	$⊢ (φ \land x \in A) \to x \in ℕ$
141		isppw2	$⊢ x \in ℕ \to (Λ (x) \neq 0 \leftrightarrow \exists p \in ℙ \exists k \in ℕ x = p^{k})$
142	140 141	syl	$⊢ (φ \land x \in A) \to (Λ (x) \neq 0 \leftrightarrow \exists p \in ℙ \exists k \in ℕ x = p^{k})$
143	139 142	bitr4d	$⊢ (φ \land x \in A) \to (\exists p \in P \exists k \in K x = p^{k} \leftrightarrow Λ (x) \neq 0)$
144	125 143	syl5bb	$⊢ (φ \land x \in A) \to (x \in ran (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a)) \leftrightarrow Λ (x) \neq 0)$
145	144	necon2bbid	$⊢ (φ \land x \in A) \to (Λ (x) = 0 \leftrightarrow \neg x \in ran (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a)))$
146	145	pm5.32da	$⊢ φ \to ((x \in A \land Λ (x) = 0) \leftrightarrow (x \in A \land \neg x \in ran (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a))))$
147	7	ex	$⊢ φ \to ((x \in A \land Λ (x) = 0) \to B = 0)$
148	146 147	sylbird	$⊢ φ \to ((x \in A \land \neg x \in ran (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a))) \to B = 0)$
149	121 148	syl5bi	$⊢ φ \to (x \in (A ∖ ran (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a))) \to B = 0)$
150	149	imp	$⊢ (φ \land x \in (A ∖ ran (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a)))) \to B = 0$
151	110 120 150 2	fsumss	$⊢ φ \to \sum_{x \in ran (a \in ⋃_{p \in P} (\{p\} \times K) ⟼^(a))} B = \sum_{x \in A} B$
152	44 118 151	3eqtr2rd	$⊢ φ \to \sum_{x \in A} B = \sum_{p \in P} \sum_{k \in K} C$

Metamath Proof Explorer

Theorem fsumvma

Proof