dpjidcl

Description: The key property of projections: the sum of all the projections of A is A . (Contributed by Mario Carneiro, 26-Apr-2016) (Revised by AV, 14-Jul-2019)

	Ref	Expression
Hypotheses	dpjfval.1	$⊢ φ \to G dom DProd S$
	dpjfval.2	$⊢ φ \to dom S = I$
	dpjfval.p	$⊢ P = G dProj S$
	dpjidcl.3	$⊢ φ \to A \in (G DProd S)$
	dpjidcl.0	$⊢ \underset{˙}{0} = 0_{G}$
	dpjidcl.w	$⊢ W = \{h \in \underset{i \in I}{⨉} S (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
Assertion	dpjidcl	$⊢ φ \to ((x \in I ⟼ P (x) (A)) \in W \land A = \underset{x \in I}{\sum_{G}} P (x) (A))$

Proof

Step	Hyp	Ref	Expression
1		dpjfval.1	$⊢ φ \to G dom DProd S$
2		dpjfval.2	$⊢ φ \to dom S = I$
3		dpjfval.p	$⊢ P = G dProj S$
4		dpjidcl.3	$⊢ φ \to A \in (G DProd S)$
5		dpjidcl.0	$⊢ \underset{˙}{0} = 0_{G}$
6		dpjidcl.w	$⊢ W = \{h \in \underset{i \in I}{⨉} S (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
7	5 6	eldprd	$⊢ dom S = I \to (A \in (G DProd S) \leftrightarrow (G dom DProd S \land \exists f \in W A = \sum_{G} f))$
8	2 7	syl	$⊢ φ \to (A \in (G DProd S) \leftrightarrow (G dom DProd S \land \exists f \in W A = \sum_{G} f))$
9	4 8	mpbid	$⊢ φ \to (G dom DProd S \land \exists f \in W A = \sum_{G} f)$
10	9	simprd	$⊢ φ \to \exists f \in W A = \sum_{G} f$
11	1	adantr	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to G dom DProd S$
12	2	adantr	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to dom S = I$
13	1	ad2antrr	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to G dom DProd S$
14	2	ad2antrr	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to dom S = I$
15		simpr	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to x \in I$
16	13 14 3 15	dpjf	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to P (x) : G DProd S ⟶ S (x)$
17	4	ad2antrr	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to A \in (G DProd S)$
18	16 17	ffvelrnd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to P (x) (A) \in S (x)$
19	1 2	dprddomcld	$⊢ φ \to I \in V$
20	19	mptexd	$⊢ φ \to (x \in I ⟼ P (x) (A)) \in V$
21	20	adantr	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to (x \in I ⟼ P (x) (A)) \in V$
22		funmpt	$⊢ Fun (x \in I ⟼ P (x) (A))$
23	22	a1i	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to Fun (x \in I ⟼ P (x) (A))$
24		simprl	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to f \in W$
25	6 11 12 24	dprdffsupp	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to {finSupp}_{\underset{˙}{0}} (f)$
26		eldifi	$⊢ x \in (I ∖ {supp}_{\underset{˙}{0}} (f)) \to x \in I$
27		eqid	$⊢ {proj}_{1} (G) = {proj}_{1} (G)$
28	13 14 3 27 15	dpjval	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to P (x) = S (x) {proj}_{1} (G) (G DProd ({S ↾}_{(I ∖ \{x\})}))$
29	28	fveq1d	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to P (x) (A) = (S (x) {proj}_{1} (G) (G DProd ({S ↾}_{(I ∖ \{x\})}))) (A)$
30	26 29	sylan2	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \to P (x) (A) = (S (x) {proj}_{1} (G) (G DProd ({S ↾}_{(I ∖ \{x\})}))) (A)$
31		simplrr	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \to A = \sum_{G} f$
32		eqid	$⊢ {Base}_{G} = {Base}_{G}$
33		eqid	$⊢ Cntz (G) = Cntz (G)$
34		dprdgrp	$⊢ G dom DProd S \to G \in Grp$
35		grpmnd	$⊢ G \in Grp \to G \in Mnd$
36	11 34 35	3syl	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to G \in Mnd$
37	36	adantr	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \to G \in Mnd$
38	19	ad2antrr	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \to I \in V$
39	6 11 12 24 32	dprdff	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to f : I ⟶ {Base}_{G}$
40	39	adantr	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \to f : I ⟶ {Base}_{G}$
41	24	adantr	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to f \in W$
42	6 13 14 41 33	dprdfcntz	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to ran f \subseteq Cntz (G) (ran f)$
43	26 42	sylan2	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \to ran f \subseteq Cntz (G) (ran f)$
44		snssi	$⊢ x \in (I ∖ {supp}_{\underset{˙}{0}} (f)) \to \{x\} \subseteq I ∖ {supp}_{\underset{˙}{0}} (f)$
45	44	adantl	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \to \{x\} \subseteq I ∖ {supp}_{\underset{˙}{0}} (f)$
46	45	difss2d	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \to \{x\} \subseteq I$
47		suppssdm	$⊢ f supp \underset{˙}{0} \subseteq dom f$
48	47 39	fssdm	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to f supp \underset{˙}{0} \subseteq I$
49	48	adantr	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \to f supp \underset{˙}{0} \subseteq I$
50		ssconb	$⊢ (\{x\} \subseteq I \land f supp \underset{˙}{0} \subseteq I) \to (\{x\} \subseteq I ∖ {supp}_{\underset{˙}{0}} (f) \leftrightarrow f supp \underset{˙}{0} \subseteq I ∖ \{x\})$
51	46 49 50	syl2anc	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \to (\{x\} \subseteq I ∖ {supp}_{\underset{˙}{0}} (f) \leftrightarrow f supp \underset{˙}{0} \subseteq I ∖ \{x\})$
52	45 51	mpbid	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \to f supp \underset{˙}{0} \subseteq I ∖ \{x\}$
53	25	adantr	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \to {finSupp}_{\underset{˙}{0}} (f)$
54	32 5 33 37 38 40 43 52 53	gsumzres	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \to \sum_{G} ({f ↾}_{(I ∖ \{x\})}) = \sum_{G} f$
55	31 54	eqtr4d	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \to A = \sum_{G} ({f ↾}_{(I ∖ \{x\})})$
56		eqid	$⊢ \{h \in \underset{i \in I ∖ \{x\}}{⨉} ({S ↾}_{(I ∖ \{x\})}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} = \{h \in \underset{i \in I ∖ \{x\}}{⨉} ({S ↾}_{(I ∖ \{x\})}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
57		difss	$⊢ I ∖ \{x\} \subseteq I$
58	57	a1i	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to I ∖ \{x\} \subseteq I$
59	13 14 58	dprdres	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to (G dom DProd ({S ↾}_{(I ∖ \{x\})}) \land G DProd ({S ↾}_{(I ∖ \{x\})}) \subseteq G DProd S)$
60	59	simpld	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to G dom DProd ({S ↾}_{(I ∖ \{x\})})$
61	13 14	dprdf2	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to S : I ⟶ SubGrp (G)$
62		fssres	$⊢ (S : I ⟶ SubGrp (G) \land I ∖ \{x\} \subseteq I) \to ({S ↾}_{(I ∖ \{x\})}) : I ∖ \{x\} ⟶ SubGrp (G)$
63	61 57 62	sylancl	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to ({S ↾}_{(I ∖ \{x\})}) : I ∖ \{x\} ⟶ SubGrp (G)$
64	63	fdmd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to dom ({S ↾}_{(I ∖ \{x\})}) = I ∖ \{x\}$
65	39	adantr	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to f : I ⟶ {Base}_{G}$
66	65	feqmptd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to f = (k \in I ⟼ f (k))$
67	66	reseq1d	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to {f ↾}_{(I ∖ \{x\})} = {(k \in I ⟼ f (k)) ↾}_{(I ∖ \{x\})}$
68		resmpt	$⊢ I ∖ \{x\} \subseteq I \to {(k \in I ⟼ f (k)) ↾}_{(I ∖ \{x\})} = (k \in (I ∖ \{x\}) ⟼ f (k))$
69	57 68	ax-mp	$⊢ {(k \in I ⟼ f (k)) ↾}_{(I ∖ \{x\})} = (k \in (I ∖ \{x\}) ⟼ f (k))$
70	67 69	eqtrdi	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to {f ↾}_{(I ∖ \{x\})} = (k \in (I ∖ \{x\}) ⟼ f (k))$
71		eldifi	$⊢ k \in (I ∖ \{x\}) \to k \in I$
72	6 13 14 41	dprdfcl	$⊢ (((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \land k \in I) \to f (k) \in S (k)$
73	71 72	sylan2	$⊢ (((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \land k \in (I ∖ \{x\})) \to f (k) \in S (k)$
74		fvres	$⊢ k \in (I ∖ \{x\}) \to ({S ↾}_{(I ∖ \{x\})}) (k) = S (k)$
75	74	adantl	$⊢ (((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \land k \in (I ∖ \{x\})) \to ({S ↾}_{(I ∖ \{x\})}) (k) = S (k)$
76	73 75	eleqtrrd	$⊢ (((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \land k \in (I ∖ \{x\})) \to f (k) \in ({S ↾}_{(I ∖ \{x\})}) (k)$
77		difexg	$⊢ I \in V \to I ∖ \{x\} \in V$
78	19 77	syl	$⊢ φ \to I ∖ \{x\} \in V$
79	78	mptexd	$⊢ φ \to (k \in (I ∖ \{x\}) ⟼ f (k)) \in V$
80	79	ad2antrr	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to (k \in (I ∖ \{x\}) ⟼ f (k)) \in V$
81		funmpt	$⊢ Fun (k \in (I ∖ \{x\}) ⟼ f (k))$
82	81	a1i	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to Fun (k \in (I ∖ \{x\}) ⟼ f (k))$
83	25	adantr	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to {finSupp}_{\underset{˙}{0}} (f)$
84		ssdif	$⊢ I ∖ \{x\} \subseteq I \to (I ∖ \{x\}) ∖ {supp}_{\underset{˙}{0}} (f) \subseteq I ∖ {supp}_{\underset{˙}{0}} (f)$
85	57 84	ax-mp	$⊢ (I ∖ \{x\}) ∖ {supp}_{\underset{˙}{0}} (f) \subseteq I ∖ {supp}_{\underset{˙}{0}} (f)$
86	85	sseli	$⊢ k \in ((I ∖ \{x\}) ∖ {supp}_{\underset{˙}{0}} (f)) \to k \in (I ∖ {supp}_{\underset{˙}{0}} (f))$
87		ssidd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to f supp \underset{˙}{0} \subseteq f supp \underset{˙}{0}$
88	19	ad2antrr	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to I \in V$
89	5	fvexi	$⊢ \underset{˙}{0} \in V$
90	89	a1i	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to \underset{˙}{0} \in V$
91	65 87 88 90	suppssr	$⊢ (((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \land k \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \to f (k) = \underset{˙}{0}$
92	86 91	sylan2	$⊢ (((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \land k \in ((I ∖ \{x\}) ∖ {supp}_{\underset{˙}{0}} (f))) \to f (k) = \underset{˙}{0}$
93	78	ad2antrr	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to I ∖ \{x\} \in V$
94	92 93	suppss2	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to (k \in (I ∖ \{x\}) ⟼ f (k)) supp \underset{˙}{0} \subseteq f supp \underset{˙}{0}$
95		fsuppsssupp	$⊢ (((k \in (I ∖ \{x\}) ⟼ f (k)) \in V \land Fun (k \in (I ∖ \{x\}) ⟼ f (k))) \land ({finSupp}_{\underset{˙}{0}} (f) \land (k \in (I ∖ \{x\}) ⟼ f (k)) supp \underset{˙}{0} \subseteq f supp \underset{˙}{0})) \to {finSupp}_{\underset{˙}{0}} ((k \in (I ∖ \{x\}) ⟼ f (k)))$
96	80 82 83 94 95	syl22anc	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to {finSupp}_{\underset{˙}{0}} ((k \in (I ∖ \{x\}) ⟼ f (k)))$
97	56 60 64 76 96	dprdwd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to (k \in (I ∖ \{x\}) ⟼ f (k)) \in \{h \in \underset{i \in I ∖ \{x\}}{⨉} ({S ↾}_{(I ∖ \{x\})}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
98	70 97	eqeltrd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to {f ↾}_{(I ∖ \{x\})} \in \{h \in \underset{i \in I ∖ \{x\}}{⨉} ({S ↾}_{(I ∖ \{x\})}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
99	5 56 60 64 98	eldprdi	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to \sum_{G} ({f ↾}_{(I ∖ \{x\})}) \in (G DProd ({S ↾}_{(I ∖ \{x\})}))$
100	26 99	sylan2	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \to \sum_{G} ({f ↾}_{(I ∖ \{x\})}) \in (G DProd ({S ↾}_{(I ∖ \{x\})}))$
101	55 100	eqeltrd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \to A \in (G DProd ({S ↾}_{(I ∖ \{x\})}))$
102		eqid	$⊢ +_{G} = +_{G}$
103		eqid	$⊢ LSSum (G) = LSSum (G)$
104	61 15	ffvelrnd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to S (x) \in SubGrp (G)$
105		dprdsubg	$⊢ G dom DProd ({S ↾}_{(I ∖ \{x\})}) \to G DProd ({S ↾}_{(I ∖ \{x\})}) \in SubGrp (G)$
106	60 105	syl	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to G DProd ({S ↾}_{(I ∖ \{x\})}) \in SubGrp (G)$
107	13 14 15 5	dpjdisj	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to S (x) \cap (G DProd ({S ↾}_{(I ∖ \{x\})})) = \{\underset{˙}{0}\}$
108	13 14 15 33	dpjcntz	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to S (x) \subseteq Cntz (G) (G DProd ({S ↾}_{(I ∖ \{x\})}))$
109	102 103 5 33 104 106 107 108 27	pj1rid	$⊢ (((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \land A \in (G DProd ({S ↾}_{(I ∖ \{x\})}))) \to (S (x) {proj}_{1} (G) (G DProd ({S ↾}_{(I ∖ \{x\})}))) (A) = \underset{˙}{0}$
110	26 109	sylanl2	$⊢ (((φ \land (f \in W \land A = \sum_{G} f)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \land A \in (G DProd ({S ↾}_{(I ∖ \{x\})}))) \to (S (x) {proj}_{1} (G) (G DProd ({S ↾}_{(I ∖ \{x\})}))) (A) = \underset{˙}{0}$
111	101 110	mpdan	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \to (S (x) {proj}_{1} (G) (G DProd ({S ↾}_{(I ∖ \{x\})}))) (A) = \underset{˙}{0}$
112	30 111	eqtrd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \to P (x) (A) = \underset{˙}{0}$
113	19	adantr	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to I \in V$
114	112 113	suppss2	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to (x \in I ⟼ P (x) (A)) supp \underset{˙}{0} \subseteq f supp \underset{˙}{0}$
115		fsuppsssupp	$⊢ (((x \in I ⟼ P (x) (A)) \in V \land Fun (x \in I ⟼ P (x) (A))) \land ({finSupp}_{\underset{˙}{0}} (f) \land (x \in I ⟼ P (x) (A)) supp \underset{˙}{0} \subseteq f supp \underset{˙}{0})) \to {finSupp}_{\underset{˙}{0}} ((x \in I ⟼ P (x) (A)))$
116	21 23 25 114 115	syl22anc	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to {finSupp}_{\underset{˙}{0}} ((x \in I ⟼ P (x) (A)))$
117	6 11 12 18 116	dprdwd	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to (x \in I ⟼ P (x) (A)) \in W$
118		simprr	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to A = \sum_{G} f$
119	39	feqmptd	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to f = (x \in I ⟼ f (x))$
120		simplrr	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to A = \sum_{G} f$
121	13 34 35	3syl	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to G \in Mnd$
122	6 13 14 41	dprdffsupp	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to {finSupp}_{\underset{˙}{0}} (f)$
123		disjdif	$⊢ \{x\} \cap (I ∖ \{x\}) = \emptyset$
124	123	a1i	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to \{x\} \cap (I ∖ \{x\}) = \emptyset$
125		undif2	$⊢ \{x\} \cup (I ∖ \{x\}) = \{x\} \cup I$
126	15	snssd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to \{x\} \subseteq I$
127		ssequn1	$⊢ \{x\} \subseteq I \leftrightarrow \{x\} \cup I = I$
128	126 127	sylib	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to \{x\} \cup I = I$
129	125 128	syl5req	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to I = \{x\} \cup (I ∖ \{x\})$
130	32 5 102 33 121 88 65 42 122 124 129	gsumzsplit	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to \sum_{G} f = (\sum_{G}, ({f ↾}_{\{x\}})) +_{G} (\sum_{G}, ({f ↾}_{(I ∖ \{x\})}))$
131	65 126	feqresmpt	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to {f ↾}_{\{x\}} = (k \in \{x\} ⟼ f (k))$
132	131	oveq2d	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to \sum_{G} ({f ↾}_{\{x\}}) = \underset{k \in \{x\}}{\sum_{G}} f (k)$
133	65 15	ffvelrnd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to f (x) \in {Base}_{G}$
134		fveq2	$⊢ k = x \to f (k) = f (x)$
135	32 134	gsumsn	$⊢ (G \in Mnd \land x \in I \land f (x) \in {Base}_{G}) \to \underset{k \in \{x\}}{\sum_{G}} f (k) = f (x)$
136	121 15 133 135	syl3anc	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to \underset{k \in \{x\}}{\sum_{G}} f (k) = f (x)$
137	132 136	eqtrd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to \sum_{G} ({f ↾}_{\{x\}}) = f (x)$
138	137	oveq1d	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to (\sum_{G}, ({f ↾}_{\{x\}})) +_{G} (\sum_{G}, ({f ↾}_{(I ∖ \{x\})})) = f (x) +_{G} (\sum_{G}, ({f ↾}_{(I ∖ \{x\})}))$
139	120 130 138	3eqtrd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to A = f (x) +_{G} (\sum_{G}, ({f ↾}_{(I ∖ \{x\})}))$
140	13 14 15 103	dpjlsm	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to G DProd S = S (x) LSSum (G) (G DProd ({S ↾}_{(I ∖ \{x\})}))$
141	17 140	eleqtrd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to A \in (S (x) LSSum (G) (G DProd ({S ↾}_{(I ∖ \{x\})})))$
142	6 11 12 24	dprdfcl	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to f (x) \in S (x)$
143	102 103 5 33 104 106 107 108 27 141 142 99	pj1eq	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to (A = f (x) +_{G} (\sum_{G}, ({f ↾}_{(I ∖ \{x\})})) \leftrightarrow ((S (x) {proj}_{1} (G) (G DProd ({S ↾}_{(I ∖ \{x\})}))) (A) = f (x) \land ((G DProd ({S ↾}_{(I ∖ \{x\})})) {proj}_{1} (G) S (x)) (A) = \sum_{G} ({f ↾}_{(I ∖ \{x\})})))$
144	139 143	mpbid	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to ((S (x) {proj}_{1} (G) (G DProd ({S ↾}_{(I ∖ \{x\})}))) (A) = f (x) \land ((G DProd ({S ↾}_{(I ∖ \{x\})})) {proj}_{1} (G) S (x)) (A) = \sum_{G} ({f ↾}_{(I ∖ \{x\})}))$
145	144	simpld	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to (S (x) {proj}_{1} (G) (G DProd ({S ↾}_{(I ∖ \{x\})}))) (A) = f (x)$
146	29 145	eqtrd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to P (x) (A) = f (x)$
147	146	mpteq2dva	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to (x \in I ⟼ P (x) (A)) = (x \in I ⟼ f (x))$
148	119 147	eqtr4d	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to f = (x \in I ⟼ P (x) (A))$
149	148	oveq2d	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to \sum_{G} f = \underset{x \in I}{\sum_{G}} P (x) (A)$
150	118 149	eqtrd	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to A = \underset{x \in I}{\sum_{G}} P (x) (A)$
151	117 150	jca	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to ((x \in I ⟼ P (x) (A)) \in W \land A = \underset{x \in I}{\sum_{G}} P (x) (A))$
152	10 151	rexlimddv	$⊢ φ \to ((x \in I ⟼ P (x) (A)) \in W \land A = \underset{x \in I}{\sum_{G}} P (x) (A))$

Metamath Proof Explorer

Theorem dpjidcl

Proof