Theorem dpjf

Description: The X -th index projection is a function from the direct product to 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$$
	dpjf.3	$$⊢\phi \to X\in I$$
Assertion	dpjf	$$⊢\phi \to P\left(X\right):G\mathrm{DProd}S⟶S\left(X\right)$$

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		dpjf.3	$$⊢\phi \to X\in I$$
5		eqid	$$⊢{+}_G={+}_G$$
6		eqid	$$⊢\mathrm{LSSum}\left(G\right)=\mathrm{LSSum}\left(G\right)$$
7		eqid	$$⊢0_G=0_G$$
8		eqid	$$⊢\mathrm{Cntz}\left(G\right)=\mathrm{Cntz}\left(G\right)$$
9	1 2	dprdf2	$$⊢\phi \to S:I⟶\mathrm{SubGrp}\left(G\right)$$
10	9 4	ffvelcdmd	$$⊢\phi \to S\left(X\right)\in \mathrm{SubGrp}\left(G\right)$$
11		difssd	$$⊢\phi \to I\setminus \left\{X\right\}\subseteq I$$
12	1 2 11	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)$$
13	12	simpld	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)$$
14		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)$$
15	13 14	syl	$$⊢\phi \to G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\in \mathrm{SubGrp}\left(G\right)$$
16	1 2 4 7	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\}$$
17	1 2 4 8	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)$$
18		eqid	$$⊢{proj}_1\left(G\right)={proj}_1\left(G\right)$$
19	5 6 7 8 10 15 16 17 18	pj1f	$$⊢\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):S\left(X\right)\mathrm{LSSum}\left(G\right)\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)⟶S\left(X\right)$$
20	1 2 3 18 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)$$
21	1 2 4 6	dpjlsm	$$⊢\phi \to G\mathrm{DProd}S=S\left(X\right)\mathrm{LSSum}\left(G\right)\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)$$
22	20 21	feq12d	$$⊢\phi \to \left(P\left(X\right):G\mathrm{DProd}S⟶S\left(X\right)\leftrightarrow \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):S\left(X\right)\mathrm{LSSum}\left(G\right)\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)⟶S\left(X\right)\right)$$
23	19 22	mpbird	$$⊢\phi \to P\left(X\right):G\mathrm{DProd}S⟶S\left(X\right)$$