Theorem dpjrid

Description: The Y -th index projection annihilates elements of other factors. (Contributed by Mario Carneiro, 26-Apr-2016)

	Ref	Expression
Hypotheses	dpjfval.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
	dpjfval.2	$$⊢\phi \to \mathrm{dom}S=I$$
	dpjfval.p	$$⊢P=G\mathrm{dProj}S$$
	dpjlid.3	$$⊢\phi \to X\in I$$
	dpjlid.4	$$⊢\phi \to A\in S\left(X\right)$$
	dpjrid.0	$$⊢\underset{\dot{}}{0}=0_G$$
	dpjrid.5	$$⊢\phi \to Y\in I$$
	dpjrid.6	$$⊢\phi \to Y\ne X$$
Assertion	dpjrid	$$⊢\phi \to P\left(Y\right)\left(A\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		dpjfval.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
2		dpjfval.2	$$⊢\phi \to \mathrm{dom}S=I$$
3		dpjfval.p	$$⊢P=G\mathrm{dProj}S$$
4		dpjlid.3	$$⊢\phi \to X\in I$$
5		dpjlid.4	$$⊢\phi \to A\in S\left(X\right)$$
6		dpjrid.0	$$⊢\underset{\dot{}}{0}=0_G$$
7		dpjrid.5	$$⊢\phi \to Y\in I$$
8		dpjrid.6	$$⊢\phi \to Y\ne X$$
9		fveq2	$$⊢x=Y\to P\left(x\right)=P\left(Y\right)$$
10	9	fveq1d	$$⊢x=Y\to P\left(x\right)\left(A\right)=P\left(Y\right)\left(A\right)$$
11		eqeq1	$$⊢x=Y\to \left(x=X\leftrightarrow Y=X\right)$$
12	11	ifbid	$$⊢x=Y\to if\left(x=X,A,\underset{\dot{}}{0}\right)=if\left(Y=X,A,\underset{\dot{}}{0}\right)$$
13	10 12	eqeq12d	$$⊢x=Y\to \left(P\left(x\right)\left(A\right)=if\left(x=X,A,\underset{\dot{}}{0}\right)\leftrightarrow P\left(Y\right)\left(A\right)=if\left(Y=X,A,\underset{\dot{}}{0}\right)\right)$$
14		eqid	$$⊢\left\{h\in \underset{i\in I}{⨉}S\left(i\right)|{finSupp}_{\underset{\dot{}}{0}}\left(h\right)\right\}=\left\{h\in \underset{i\in I}{⨉}S\left(i\right)|{finSupp}_{\underset{\dot{}}{0}}\left(h\right)\right\}$$
15		eqid	$$⊢\left(x\in I⟼if\left(x=X,A,\underset{\dot{}}{0}\right)\right)=\left(x\in I⟼if\left(x=X,A,\underset{\dot{}}{0}\right)\right)$$
16	6 14 1 2 4 5 15	dprdfid	$$⊢\phi \to \left(\left(x\in I⟼if\left(x=X,A,\underset{\dot{}}{0}\right)\right)\in \left\{h\in \underset{i\in I}{⨉}S\left(i\right)|{finSupp}_{\underset{\dot{}}{0}}\left(h\right)\right\}\wedge \underset{x\in I}{{\sum }_G}if\left(x=X,A,\underset{\dot{}}{0}\right)=A\right)$$
17	16	simprd	$$⊢\phi \to \underset{x\in I}{{\sum }_G}if\left(x=X,A,\underset{\dot{}}{0}\right)=A$$
18	17	eqcomd	$$⊢\phi \to A=\underset{x\in I}{{\sum }_G}if\left(x=X,A,\underset{\dot{}}{0}\right)$$
19	1 2 4	dprdub	$$⊢\phi \to S\left(X\right)\subseteq G\mathrm{DProd}S$$
20	19 5	sseldd	$$⊢\phi \to A\in \left(G\mathrm{DProd}S\right)$$
21	16	simpld	$$⊢\phi \to \left(x\in I⟼if\left(x=X,A,\underset{\dot{}}{0}\right)\right)\in \left\{h\in \underset{i\in I}{⨉}S\left(i\right)|{finSupp}_{\underset{\dot{}}{0}}\left(h\right)\right\}$$
22	1 2 3 20 6 14 21	dpjeq	$$⊢\phi \to \left(A=\underset{x\in I}{{\sum }_G}if\left(x=X,A,\underset{\dot{}}{0}\right)\leftrightarrow \forall x\in IP\left(x\right)\left(A\right)=if\left(x=X,A,\underset{\dot{}}{0}\right)\right)$$
23	18 22	mpbid	$$⊢\phi \to \forall x\in IP\left(x\right)\left(A\right)=if\left(x=X,A,\underset{\dot{}}{0}\right)$$
24	13 23 7	rspcdva	$$⊢\phi \to P\left(Y\right)\left(A\right)=if\left(Y=X,A,\underset{\dot{}}{0}\right)$$
25		ifnefalse	$$⊢Y\ne X\to if\left(Y=X,A,\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
26	8 25	syl	$$⊢\phi \to if\left(Y=X,A,\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
27	24 26	eqtrd	$$⊢\phi \to P\left(Y\right)\left(A\right)=\underset{\dot{}}{0}$$