Theorem dprdfid

Description: A function mapping all but one arguments to zero sums to the value of this argument in a direct product. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 14-Jul-2019)

	Ref	Expression
Hypotheses	eldprdi.0	$$⊢\underset{\dot{}}{0}=0_G$$
	eldprdi.w	$$⊢W=\left\{h\in \underset{i\in I}{⨉}S\left(i\right)|{finSupp}_{\underset{\dot{}}{0}}\left(h\right)\right\}$$
	eldprdi.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
	eldprdi.2	$$⊢\phi \to \mathrm{dom}S=I$$
	dprdfid.3	$$⊢\phi \to X\in I$$
	dprdfid.4	$$⊢\phi \to A\in S\left(X\right)$$
	dprdfid.f	$$⊢F=\left(n\in I⟼if\left(n=X,A,\underset{\dot{}}{0}\right)\right)$$
Assertion	dprdfid	$$⊢\phi \to \left(F\in W\wedge {\sum }_{G}F=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		eldprdi.0	$$⊢\underset{\dot{}}{0}=0_G$$
2		eldprdi.w	$$⊢W=\left\{h\in \underset{i\in I}{⨉}S\left(i\right)|{finSupp}_{\underset{\dot{}}{0}}\left(h\right)\right\}$$
3		eldprdi.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
4		eldprdi.2	$$⊢\phi \to \mathrm{dom}S=I$$
5		dprdfid.3	$$⊢\phi \to X\in I$$
6		dprdfid.4	$$⊢\phi \to A\in S\left(X\right)$$
7		dprdfid.f	$$⊢F=\left(n\in I⟼if\left(n=X,A,\underset{\dot{}}{0}\right)\right)$$
8	6	ad2antrr	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge n=X\right)\to A\in S\left(X\right)$$
9		simpr	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge n=X\right)\to n=X$$
10	9	fveq2d	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge n=X\right)\to S\left(n\right)=S\left(X\right)$$
11	8 10	eleqtrrd	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge n=X\right)\to A\in S\left(n\right)$$
12	3 4	dprdf2	$$⊢\phi \to S:I⟶\mathrm{SubGrp}\left(G\right)$$
13	12	ffvelrnda	$$⊢\left(\phi \wedge n\in I\right)\to S\left(n\right)\in \mathrm{SubGrp}\left(G\right)$$
14	1	subg0cl	$$⊢S\left(n\right)\in \mathrm{SubGrp}\left(G\right)\to \underset{\dot{}}{0}\in S\left(n\right)$$
15	13 14	syl	$$⊢\left(\phi \wedge n\in I\right)\to \underset{\dot{}}{0}\in S\left(n\right)$$
16	15	adantr	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge \neg n=X\right)\to \underset{\dot{}}{0}\in S\left(n\right)$$
17	11 16	ifclda	$$⊢\left(\phi \wedge n\in I\right)\to if\left(n=X,A,\underset{\dot{}}{0}\right)\in S\left(n\right)$$
18	3 4	dprddomcld	$$⊢\phi \to I\in \mathrm{V}$$
19	1	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
20	19	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
21		eqid	$$⊢\left(n\in I⟼if\left(n=X,A,\underset{\dot{}}{0}\right)\right)=\left(n\in I⟼if\left(n=X,A,\underset{\dot{}}{0}\right)\right)$$
22	18 20 21	sniffsupp	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(n\in I⟼if\left(n=X,A,\underset{\dot{}}{0}\right)\right)\right)$$
23	2 3 4 17 22	dprdwd	$$⊢\phi \to \left(n\in I⟼if\left(n=X,A,\underset{\dot{}}{0}\right)\right)\in W$$
24	7 23	eqeltrid	$$⊢\phi \to F\in W$$
25		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
26		dprdgrp	$$⊢G\mathrm{dom}\mathrm{DProd}S\to G\in \mathrm{Grp}$$
27		grpmnd	$$⊢G\in \mathrm{Grp}\to G\in \mathrm{Mnd}$$
28	3 26 27	3syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
29	2 3 4 24 25	dprdff	$$⊢\phi \to F:I⟶{\mathrm{Base}}_G$$
30	7	oveq1i	$$⊢F\mathrm{supp}\underset{\dot{}}{0}=\left(n\in I⟼if\left(n=X,A,\underset{\dot{}}{0}\right)\right)\mathrm{supp}\underset{\dot{}}{0}$$
31		eldifsni	$$⊢n\in \left(I\setminus \left\{X\right\}\right)\to n\ne X$$
32	31	adantl	$$⊢\left(\phi \wedge n\in \left(I\setminus \left\{X\right\}\right)\right)\to n\ne X$$
33		ifnefalse	$$⊢n\ne X\to if\left(n=X,A,\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
34	32 33	syl	$$⊢\left(\phi \wedge n\in \left(I\setminus \left\{X\right\}\right)\right)\to if\left(n=X,A,\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
35	34 18	suppss2	$$⊢\phi \to \left(n\in I⟼if\left(n=X,A,\underset{\dot{}}{0}\right)\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{X\right\}$$
36	30 35	eqsstrid	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{X\right\}$$
37	25 1 28 18 5 29 36	gsumpt	$$⊢\phi \to {\sum }_{G}F=F\left(X\right)$$
38		iftrue	$$⊢n=X\to if\left(n=X,A,\underset{\dot{}}{0}\right)=A$$
39	7 38 5 6	fvmptd3	$$⊢\phi \to F\left(X\right)=A$$
40	37 39	eqtrd	$$⊢\phi \to {\sum }_{G}F=A$$
41	24 40	jca	$$⊢\phi \to \left(F\in W\wedge {\sum }_{G}F=A\right)$$