Theorem dpjlid

Description: The X -th index projection acts as the identity on elements of the X -th factor. (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)$$
Assertion	dpjlid	$$⊢\phi \to P\left(X\right)\left(A\right)=A$$

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		eqid	$$⊢{proj}_1\left(G\right)={proj}_1\left(G\right)$$
7	1 2 3 6 4	dpjval	$$⊢\phi \to P\left(X\right)=S\left(X\right){proj}_1\left(G\right)\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)$$
8	7	fveq1d	$$⊢\phi \to P\left(X\right)\left(A\right)=\left(S\left(X\right){proj}_1\left(G\right)\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)\right)\left(A\right)$$
9		eqid	$$⊢{+}_G={+}_G$$
10		eqid	$$⊢\mathrm{LSSum}\left(G\right)=\mathrm{LSSum}\left(G\right)$$
11		eqid	$$⊢0_G=0_G$$
12		eqid	$$⊢\mathrm{Cntz}\left(G\right)=\mathrm{Cntz}\left(G\right)$$
13	1 2	dprdf2	$$⊢\phi \to S:I⟶\mathrm{SubGrp}\left(G\right)$$
14	13 4	ffvelcdmd	$$⊢\phi \to S\left(X\right)\in \mathrm{SubGrp}\left(G\right)$$
15		difssd	$$⊢\phi \to I\setminus \left\{X\right\}\subseteq I$$
16	1 2 15	dprdres	$$⊢\phi \to \left(G\mathrm{dom}\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\wedge G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\subseteq G\mathrm{DProd}S\right)$$
17	16	simpld	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)$$
18		dprdsubg	$$⊢G\mathrm{dom}\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\to G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\in \mathrm{SubGrp}\left(G\right)$$
19	17 18	syl	$$⊢\phi \to G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\in \mathrm{SubGrp}\left(G\right)$$
20	1 2 4 11	dpjdisj	$$⊢\phi \to S\left(X\right)\cap \left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)=\left\{0_G\right\}$$
21	1 2 4 12	dpjcntz	$$⊢\phi \to S\left(X\right)\subseteq \mathrm{Cntz}\left(G\right)\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)$$
22	9 10 11 12 14 19 20 21 6	pj1lid	$$⊢\left(\phi \wedge A\in S\left(X\right)\right)\to \left(S\left(X\right){proj}_1\left(G\right)\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)\right)\left(A\right)=A$$
23	5 22	mpdan	$$⊢\phi \to \left(S\left(X\right){proj}_1\left(G\right)\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)\right)\left(A\right)=A$$
24	8 23	eqtrd	$$⊢\phi \to P\left(X\right)\left(A\right)=A$$