psrgsum

Description: Finite commutative sums of power series are taken componentwise. (Contributed by Thierry Arnoux, 16-Mar-2026)

	Ref	Expression
Hypotheses	psrgsum.s	$⊢ S = I mPwSer R$
	psrgsum.b	$⊢ B = {Base}_{S}$
	psrgsum.r	$⊢ φ \to R \in Ring$
	psrgsum.i	$⊢ φ \to I \in V$
	psrgsum.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
	psrgsum.a	$⊢ φ \to A \in Fin$
	psrgsum.f	$⊢ φ \to F : A ⟶ B$
Assertion	psrgsum	$⊢ φ \to \sum_{S} F = (y \in D ⟼ \underset{k \in A}{\sum_{R}} F (k) (y))$

Proof

Step	Hyp	Ref	Expression
1		psrgsum.s	$⊢ S = I mPwSer R$
2		psrgsum.b	$⊢ B = {Base}_{S}$
3		psrgsum.r	$⊢ φ \to R \in Ring$
4		psrgsum.i	$⊢ φ \to I \in V$
5		psrgsum.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
6		psrgsum.a	$⊢ φ \to A \in Fin$
7		psrgsum.f	$⊢ φ \to F : A ⟶ B$
8	7	feqmptd	$⊢ φ \to F = (k \in A ⟼ F (k))$
9	8	oveq2d	$⊢ φ \to \sum_{S} F = \underset{k \in A}{\sum_{S}} F (k)$
10		mpteq1	$⊢ a = \emptyset \to (k \in a ⟼ F (k)) = (k \in \emptyset ⟼ F (k))$
11	10	oveq2d	$⊢ a = \emptyset \to \underset{k \in a}{\sum_{S}} F (k) = \underset{k \in \emptyset}{\sum_{S}} F (k)$
12		mpteq1	$⊢ a = \emptyset \to (k \in a ⟼ F (k) (y)) = (k \in \emptyset ⟼ F (k) (y))$
13	12	oveq2d	$⊢ a = \emptyset \to \underset{k \in a}{\sum_{R}} F (k) (y) = \underset{k \in \emptyset}{\sum_{R}} F (k) (y)$
14	13	mpteq2dv	$⊢ a = \emptyset \to (y \in D ⟼ \underset{k \in a}{\sum_{R}} F (k) (y)) = (y \in D ⟼ \underset{k \in \emptyset}{\sum_{R}} F (k) (y))$
15	11 14	eqeq12d	$⊢ a = \emptyset \to (\underset{k \in a}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in a}{\sum_{R}} F (k) (y)) \leftrightarrow \underset{k \in \emptyset}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in \emptyset}{\sum_{R}} F (k) (y)))$
16		mpteq1	$⊢ a = b \to (k \in a ⟼ F (k)) = (k \in b ⟼ F (k))$
17	16	oveq2d	$⊢ a = b \to \underset{k \in a}{\sum_{S}} F (k) = \underset{k \in b}{\sum_{S}} F (k)$
18		mpteq1	$⊢ a = b \to (k \in a ⟼ F (k) (y)) = (k \in b ⟼ F (k) (y))$
19	18	oveq2d	$⊢ a = b \to \underset{k \in a}{\sum_{R}} F (k) (y) = \underset{k \in b}{\sum_{R}} F (k) (y)$
20	19	mpteq2dv	$⊢ a = b \to (y \in D ⟼ \underset{k \in a}{\sum_{R}} F (k) (y)) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))$
21	17 20	eqeq12d	$⊢ a = b \to (\underset{k \in a}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in a}{\sum_{R}} F (k) (y)) \leftrightarrow \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y)))$
22		mpteq1	$⊢ a = b \cup \{f\} \to (k \in a ⟼ F (k)) = (k \in (b \cup \{f\}) ⟼ F (k))$
23		fveq2	$⊢ k = l \to F (k) = F (l)$
24	23	cbvmptv	$⊢ (k \in (b \cup \{f\}) ⟼ F (k)) = (l \in (b \cup \{f\}) ⟼ F (l))$
25	22 24	eqtrdi	$⊢ a = b \cup \{f\} \to (k \in a ⟼ F (k)) = (l \in (b \cup \{f\}) ⟼ F (l))$
26	25	oveq2d	$⊢ a = b \cup \{f\} \to \underset{k \in a}{\sum_{S}} F (k) = \underset{l \in b \cup \{f\}}{\sum_{S}} F (l)$
27		mpteq1	$⊢ a = b \cup \{f\} \to (k \in a ⟼ F (k) (y)) = (k \in (b \cup \{f\}) ⟼ F (k) (y))$
28	27	oveq2d	$⊢ a = b \cup \{f\} \to \underset{k \in a}{\sum_{R}} F (k) (y) = \underset{k \in b \cup \{f\}}{\sum_{R}} F (k) (y)$
29	28	mpteq2dv	$⊢ a = b \cup \{f\} \to (y \in D ⟼ \underset{k \in a}{\sum_{R}} F (k) (y)) = (y \in D ⟼ \underset{k \in b \cup \{f\}}{\sum_{R}} F (k) (y))$
30	26 29	eqeq12d	$⊢ a = b \cup \{f\} \to (\underset{k \in a}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in a}{\sum_{R}} F (k) (y)) \leftrightarrow \underset{l \in b \cup \{f\}}{\sum_{S}} F (l) = (y \in D ⟼ \underset{k \in b \cup \{f\}}{\sum_{R}} F (k) (y)))$
31		mpteq1	$⊢ a = A \to (k \in a ⟼ F (k)) = (k \in A ⟼ F (k))$
32	31	oveq2d	$⊢ a = A \to \underset{k \in a}{\sum_{S}} F (k) = \underset{k \in A}{\sum_{S}} F (k)$
33		mpteq1	$⊢ a = A \to (k \in a ⟼ F (k) (y)) = (k \in A ⟼ F (k) (y))$
34	33	oveq2d	$⊢ a = A \to \underset{k \in a}{\sum_{R}} F (k) (y) = \underset{k \in A}{\sum_{R}} F (k) (y)$
35	34	mpteq2dv	$⊢ a = A \to (y \in D ⟼ \underset{k \in a}{\sum_{R}} F (k) (y)) = (y \in D ⟼ \underset{k \in A}{\sum_{R}} F (k) (y))$
36	32 35	eqeq12d	$⊢ a = A \to (\underset{k \in a}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in a}{\sum_{R}} F (k) (y)) \leftrightarrow \underset{k \in A}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in A}{\sum_{R}} F (k) (y)))$
37		mpt0	$⊢ (k \in \emptyset ⟼ F (k)) = \emptyset$
38	37	a1i	$⊢ φ \to (k \in \emptyset ⟼ F (k)) = \emptyset$
39	38	oveq2d	$⊢ φ \to \underset{k \in \emptyset}{\sum_{S}} F (k) = \sum_{S} \emptyset$
40		eqid	$⊢ 0_{S} = 0_{S}$
41	40	gsum0	$⊢ \sum_{S} \emptyset = 0_{S}$
42	41	a1i	$⊢ φ \to \sum_{S} \emptyset = 0_{S}$
43		fconstmpt	$⊢ D \times \{0_{R}\} = (y \in D ⟼ 0_{R})$
44	3	ringgrpd	$⊢ φ \to R \in Grp$
45	5	psrbasfsupp	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
46		eqid	$⊢ 0_{R} = 0_{R}$
47	1 4 44 45 46 40	psr0	$⊢ φ \to 0_{S} = D \times \{0_{R}\}$
48		mpt0	$⊢ (k \in \emptyset ⟼ F (k) (y)) = \emptyset$
49	48	oveq2i	$⊢ \underset{k \in \emptyset}{\sum_{R}} F (k) (y) = \sum_{R} \emptyset$
50	46	gsum0	$⊢ \sum_{R} \emptyset = 0_{R}$
51	49 50	eqtri	$⊢ \underset{k \in \emptyset}{\sum_{R}} F (k) (y) = 0_{R}$
52	51	a1i	$⊢ φ \to \underset{k \in \emptyset}{\sum_{R}} F (k) (y) = 0_{R}$
53	52	mpteq2dv	$⊢ φ \to (y \in D ⟼ \underset{k \in \emptyset}{\sum_{R}} F (k) (y)) = (y \in D ⟼ 0_{R})$
54	43 47 53	3eqtr4a	$⊢ φ \to 0_{S} = (y \in D ⟼ \underset{k \in \emptyset}{\sum_{R}} F (k) (y))$
55	39 42 54	3eqtrd	$⊢ φ \to \underset{k \in \emptyset}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in \emptyset}{\sum_{R}} F (k) (y))$
56		ovex	$⊢ {ℕ_{0}}^{I} \in V$
57	5 56	rabex2	$⊢ D \in V$
58		nfv	$⊢ Ⅎ y ((φ \land b \subseteq A) \land f \in (A ∖ b))$
59		ovexd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land y \in D) \to \underset{k \in b}{\sum_{R}} F (k) (y) \in V$
60		eqid	$⊢ (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y)) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))$
61	58 59 60	fnmptd	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y)) Fn D$
62		fvexd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land y \in D) \to F (f) (y) \in V$
63		eqid	$⊢ (y \in D ⟼ F (f) (y)) = (y \in D ⟼ F (f) (y))$
64	58 62 63	fnmptd	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to (y \in D ⟼ F (f) (y)) Fn D$
65		ofmpteq	$⊢ (D \in V \land (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y)) Fn D \land (y \in D ⟼ F (f) (y)) Fn D) \to (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y)) {+_{R}}_{f} (y \in D ⟼ F (f) (y)) = (y \in D ⟼ (\underset{k \in b}{\sum_{R}}, F (k) (y)) +_{R} F (f) (y))$
66	57 61 64 65	mp3an2i	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y)) {+_{R}}_{f} (y \in D ⟼ F (f) (y)) = (y \in D ⟼ (\underset{k \in b}{\sum_{R}}, F (k) (y)) +_{R} F (f) (y))$
67	66	adantr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y)) {+_{R}}_{f} (y \in D ⟼ F (f) (y)) = (y \in D ⟼ (\underset{k \in b}{\sum_{R}}, F (k) (y)) +_{R} F (f) (y))$
68		eqid	$⊢ +_{S} = +_{S}$
69	1 4 3	psrring	$⊢ φ \to S \in Ring$
70	69	ringcmnd	$⊢ φ \to S \in CMnd$
71	70	ad3antrrr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to S \in CMnd$
72	6	ad3antrrr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to A \in Fin$
73		simpllr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to b \subseteq A$
74	72 73	ssfid	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to b \in Fin$
75	7	ad4antr	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \land l \in b) \to F : A ⟶ B$
76	73	sselda	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \land l \in b) \to l \in A$
77	75 76	ffvelcdmd	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \land l \in b) \to F (l) \in B$
78		simplr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to f \in (A ∖ b)$
79	78	eldifbd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to \neg f \in b$
80	7	ad3antrrr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to F : A ⟶ B$
81	78	eldifad	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to f \in A$
82	80 81	ffvelcdmd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to F (f) \in B$
83		fveq2	$⊢ l = f \to F (l) = F (f)$
84	2 68 71 74 77 78 79 82 83	gsumunsn	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to \underset{l \in b \cup \{f\}}{\sum_{S}} F (l) = (\underset{l \in b}{\sum_{S}}, F (l)) +_{S} F (f)$
85		eqid	$⊢ +_{R} = +_{R}$
86	77	fmpttd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to (l \in b ⟼ F (l)) : b ⟶ B$
87		eqid	$⊢ (l \in b ⟼ F (l)) = (l \in b ⟼ F (l))$
88		fvexd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to 0_{S} \in V$
89	87 74 77 88	fsuppmptdm	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to {finSupp}_{0_{S}} ((l \in b ⟼ F (l)))$
90	2 40 71 74 86 89	gsumcl	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to \underset{l \in b}{\sum_{S}} F (l) \in B$
91	1 2 85 68 90 82	psradd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to (\underset{l \in b}{\sum_{S}}, F (l)) +_{S} F (f) = (\underset{l \in b}{\sum_{S}}, F (l)) {+_{R}}_{f} F (f)$
92	23	cbvmptv	$⊢ (k \in b ⟼ F (k)) = (l \in b ⟼ F (l))$
93	92	oveq2i	$⊢ \underset{k \in b}{\sum_{S}} F (k) = \underset{l \in b}{\sum_{S}} F (l)$
94		simpr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))$
95	93 94	eqtr3id	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to \underset{l \in b}{\sum_{S}} F (l) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))$
96		eqid	$⊢ {Base}_{R} = {Base}_{R}$
97	1 96 45 2 82	psrelbas	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to F (f) : D ⟶ {Base}_{R}$
98	97	feqmptd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to F (f) = (y \in D ⟼ F (f) (y))$
99	95 98	oveq12d	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to (\underset{l \in b}{\sum_{S}}, F (l)) {+_{R}}_{f} F (f) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y)) {+_{R}}_{f} (y \in D ⟼ F (f) (y))$
100	84 91 99	3eqtrd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to \underset{l \in b \cup \{f\}}{\sum_{S}} F (l) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y)) {+_{R}}_{f} (y \in D ⟼ F (f) (y))$
101	3	ringcmnd	$⊢ φ \to R \in CMnd$
102	101	ad3antrrr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land y \in D) \to R \in CMnd$
103	6	ad3antrrr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land y \in D) \to A \in Fin$
104		simpllr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land y \in D) \to b \subseteq A$
105	103 104	ssfid	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land y \in D) \to b \in Fin$
106	7	ad4antr	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land y \in D) \land k \in b) \to F : A ⟶ B$
107	104	sselda	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land y \in D) \land k \in b) \to k \in A$
108	106 107	ffvelcdmd	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land y \in D) \land k \in b) \to F (k) \in B$
109	1 96 45 2 108	psrelbas	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land y \in D) \land k \in b) \to F (k) : D ⟶ {Base}_{R}$
110		simplr	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land y \in D) \land k \in b) \to y \in D$
111	109 110	ffvelcdmd	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land y \in D) \land k \in b) \to F (k) (y) \in {Base}_{R}$
112		simplr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land y \in D) \to f \in (A ∖ b)$
113	112	eldifbd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land y \in D) \to \neg f \in b$
114	7	ad2antrr	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to F : A ⟶ B$
115		simpr	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to f \in (A ∖ b)$
116	115	eldifad	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to f \in A$
117	114 116	ffvelcdmd	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to F (f) \in B$
118	1 96 45 2 117	psrelbas	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to F (f) : D ⟶ {Base}_{R}$
119	118	ffvelcdmda	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land y \in D) \to F (f) (y) \in {Base}_{R}$
120		fveq2	$⊢ k = f \to F (k) = F (f)$
121	120	fveq1d	$⊢ k = f \to F (k) (y) = F (f) (y)$
122	96 85 102 105 111 112 113 119 121	gsumunsn	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land y \in D) \to \underset{k \in b \cup \{f\}}{\sum_{R}} F (k) (y) = (\underset{k \in b}{\sum_{R}}, F (k) (y)) +_{R} F (f) (y)$
123	122	mpteq2dva	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to (y \in D ⟼ \underset{k \in b \cup \{f\}}{\sum_{R}} F (k) (y)) = (y \in D ⟼ (\underset{k \in b}{\sum_{R}}, F (k) (y)) +_{R} F (f) (y))$
124	123	adantr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to (y \in D ⟼ \underset{k \in b \cup \{f\}}{\sum_{R}} F (k) (y)) = (y \in D ⟼ (\underset{k \in b}{\sum_{R}}, F (k) (y)) +_{R} F (f) (y))$
125	67 100 124	3eqtr4d	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y))) \to \underset{l \in b \cup \{f\}}{\sum_{S}} F (l) = (y \in D ⟼ \underset{k \in b \cup \{f\}}{\sum_{R}} F (k) (y))$
126	125	ex	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to (\underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y)) \to \underset{l \in b \cup \{f\}}{\sum_{S}} F (l) = (y \in D ⟼ \underset{k \in b \cup \{f\}}{\sum_{R}} F (k) (y)))$
127	126	anasss	$⊢ (φ \land (b \subseteq A \land f \in (A ∖ b))) \to (\underset{k \in b}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in b}{\sum_{R}} F (k) (y)) \to \underset{l \in b \cup \{f\}}{\sum_{S}} F (l) = (y \in D ⟼ \underset{k \in b \cup \{f\}}{\sum_{R}} F (k) (y)))$
128	15 21 30 36 55 127 6	findcard2d	$⊢ φ \to \underset{k \in A}{\sum_{S}} F (k) = (y \in D ⟼ \underset{k \in A}{\sum_{R}} F (k) (y))$
129	9 128	eqtrd	$⊢ φ \to \sum_{S} F = (y \in D ⟼ \underset{k \in A}{\sum_{R}} F (k) (y))$

Metamath Proof Explorer

Theorem psrgsum

Proof