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	ffvelcdmd	$⊢ ((φ \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	19	difexd	$⊢ φ \to I ∖ \{x\} \in V$
78	77	mptexd	$⊢ φ \to (k \in (I ∖ \{x\}) ⟼ f (k)) \in V$
79	78	ad2antrr	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to (k \in (I ∖ \{x\}) ⟼ f (k)) \in V$
80		funmpt	$⊢ Fun (k \in (I ∖ \{x\}) ⟼ f (k))$
81	80	a1i	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to Fun (k \in (I ∖ \{x\}) ⟼ f (k))$
82	25	adantr	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to {finSupp}_{\underset{˙}{0}} (f)$
83		ssdif	$⊢ I ∖ \{x\} \subseteq I \to (I ∖ \{x\}) ∖ {supp}_{\underset{˙}{0}} (f) \subseteq I ∖ {supp}_{\underset{˙}{0}} (f)$
84	57 83	ax-mp	$⊢ (I ∖ \{x\}) ∖ {supp}_{\underset{˙}{0}} (f) \subseteq I ∖ {supp}_{\underset{˙}{0}} (f)$
85	84	sseli	$⊢ k \in ((I ∖ \{x\}) ∖ {supp}_{\underset{˙}{0}} (f)) \to k \in (I ∖ {supp}_{\underset{˙}{0}} (f))$
86		ssidd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to f supp \underset{˙}{0} \subseteq f supp \underset{˙}{0}$
87	19	ad2antrr	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to I \in V$
88	5	fvexi	$⊢ \underset{˙}{0} \in V$
89	88	a1i	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to \underset{˙}{0} \in V$
90	65 86 87 89	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}$
91	85 90	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}$
92	77	ad2antrr	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to I ∖ \{x\} \in V$
93	91 92	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}$
94		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)))$
95	79 81 82 93 94	syl22anc	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to {finSupp}_{\underset{˙}{0}} ((k \in (I ∖ \{x\}) ⟼ f (k)))$
96	56 60 64 76 95	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)\}$
97	70 96	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)\}$
98	5 56 60 64 97	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\})}))$
99	26 98	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\})}))$
100	55 99	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\})}))$
101		eqid	$⊢ +_{G} = +_{G}$
102		eqid	$⊢ LSSum (G) = LSSum (G)$
103	61 15	ffvelcdmd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to S (x) \in SubGrp (G)$
104		dprdsubg	$⊢ G dom DProd ({S ↾}_{(I ∖ \{x\})}) \to G DProd ({S ↾}_{(I ∖ \{x\})}) \in SubGrp (G)$
105	60 104	syl	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to G DProd ({S ↾}_{(I ∖ \{x\})}) \in SubGrp (G)$
106	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}\}$
107	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\})}))$
108	101 102 5 33 103 105 106 107 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}$
109	26 108	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}$
110	100 109	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}$
111	30 110	eqtrd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \to P (x) (A) = \underset{˙}{0}$
112	19	adantr	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to I \in V$
113	111 112	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}$
114		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)))$
115	21 23 25 113 114	syl22anc	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to {finSupp}_{\underset{˙}{0}} ((x \in I ⟼ P (x) (A)))$
116	6 11 12 18 115	dprdwd	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to (x \in I ⟼ P (x) (A)) \in W$
117		simprr	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to A = \sum_{G} f$
118	39	feqmptd	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to f = (x \in I ⟼ f (x))$
119		simplrr	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to A = \sum_{G} f$
120	13 34 35	3syl	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to G \in Mnd$
121	6 13 14 41	dprdffsupp	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to {finSupp}_{\underset{˙}{0}} (f)$
122		disjdif	$⊢ \{x\} \cap (I ∖ \{x\}) = \emptyset$
123	122	a1i	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to \{x\} \cap (I ∖ \{x\}) = \emptyset$
124		undif2	$⊢ \{x\} \cup (I ∖ \{x\}) = \{x\} \cup I$
125	15	snssd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to \{x\} \subseteq I$
126		ssequn1	$⊢ \{x\} \subseteq I \leftrightarrow \{x\} \cup I = I$
127	125 126	sylib	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to \{x\} \cup I = I$
128	124 127	eqtr2id	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to I = \{x\} \cup (I ∖ \{x\})$
129	32 5 101 33 120 87 65 42 121 123 128	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\})}))$
130	65 125	feqresmpt	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to {f ↾}_{\{x\}} = (k \in \{x\} ⟼ f (k))$
131	130	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)$
132	65 15	ffvelcdmd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to f (x) \in {Base}_{G}$
133		fveq2	$⊢ k = x \to f (k) = f (x)$
134	32 133	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)$
135	120 15 132 134	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)$
136	131 135	eqtrd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to \sum_{G} ({f ↾}_{\{x\}}) = f (x)$
137	136	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\})}))$
138	119 129 137	3eqtrd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to A = f (x) +_{G} (\sum_{G}, ({f ↾}_{(I ∖ \{x\})}))$
139	13 14 15 102	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\})}))$
140	17 139	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\})})))$
141	6 11 12 24	dprdfcl	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to f (x) \in S (x)$
142	101 102 5 33 103 105 106 107 27 140 141 98	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\})})))$
143	138 142	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\})}))$
144	143	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)$
145	29 144	eqtrd	$⊢ ((φ \land (f \in W \land A = \sum_{G} f)) \land x \in I) \to P (x) (A) = f (x)$
146	145	mpteq2dva	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to (x \in I ⟼ P (x) (A)) = (x \in I ⟼ f (x))$
147	118 146	eqtr4d	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to f = (x \in I ⟼ P (x) (A))$
148	147	oveq2d	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to \sum_{G} f = \underset{x \in I}{\sum_{G}} P (x) (A)$
149	117 148	eqtrd	$⊢ (φ \land (f \in W \land A = \sum_{G} f)) \to A = \underset{x \in I}{\sum_{G}} P (x) (A)$
150	116 149	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))$
151	10 150	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