Theorem dpjghm

Description: The direct product is the binary subgroup product ("sum") of the direct products of the partition. (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$$
Assertion	dpjghm	$$⊢\phi \to P\left(X\right)\in \left(\left(G{\upharpoonright }_{𝑠}\left(G\mathrm{DProd}S\right)\right)\mathrm{GrpHom}G\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		dpjlid.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	pj1ghm	$$⊢\phi \to 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)\in \left(\left(G{\upharpoonright }_{𝑠}\left(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)\right)\right)\mathrm{GrpHom}G\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	21	oveq2d	$$⊢\phi \to G{\upharpoonright }_{𝑠}\left(G\mathrm{DProd}S\right)=G{\upharpoonright }_{𝑠}\left(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)\right)$$
23	22	oveq1d	$$⊢\phi \to \left(G{\upharpoonright }_{𝑠}\left(G\mathrm{DProd}S\right)\right)\mathrm{GrpHom}G=\left(G{\upharpoonright }_{𝑠}\left(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)\right)\right)\mathrm{GrpHom}G$$
24	19 20 23	3eltr4d	$$⊢\phi \to P\left(X\right)\in \left(\left(G{\upharpoonright }_{𝑠}\left(G\mathrm{DProd}S\right)\right)\mathrm{GrpHom}G\right)$$