Theorem dpjcntz

Description: The two subgroups that appear in dpjval commute. (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$$
	dpjlem.3	$$⊢\phi \to X\in I$$
	dpjcntz.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
Assertion	dpjcntz	$$⊢\phi \to S\left(X\right)\subseteq Z\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\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		dpjlem.3	$$⊢\phi \to X\in I$$
4		dpjcntz.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
5	1 2 3	dpjlem	$$⊢\phi \to G\mathrm{DProd}\left({S\upharpoonright }_{\left\{X\right\}}\right)=S\left(X\right)$$
6	1 2	dprdf2	$$⊢\phi \to S:I⟶\mathrm{SubGrp}\left(G\right)$$
7		disjdif	$$⊢\left\{X\right\}\cap \left(I\setminus \left\{X\right\}\right)=\varnothing$$
8	7	a1i	$$⊢\phi \to \left\{X\right\}\cap \left(I\setminus \left\{X\right\}\right)=\varnothing$$
9		undif2	$$⊢\left\{X\right\}\cup \left(I\setminus \left\{X\right\}\right)=\left\{X\right\}\cup I$$
10	3	snssd	$$⊢\phi \to \left\{X\right\}\subseteq I$$
11		ssequn1	$$⊢\left\{X\right\}\subseteq I\leftrightarrow \left\{X\right\}\cup I=I$$
12	10 11	sylib	$$⊢\phi \to \left\{X\right\}\cup I=I$$
13	9 12	syl5req	$$⊢\phi \to I=\left\{X\right\}\cup \left(I\setminus \left\{X\right\}\right)$$
14		eqid	$$⊢0_G=0_G$$
15	6 8 13 4 14	dmdprdsplit	$$⊢\phi \to \left(G\mathrm{dom}\mathrm{DProd}S\leftrightarrow \left(\left(G\mathrm{dom}\mathrm{DProd}\left({S\upharpoonright }_{\left\{X\right\}}\right)\wedge G\mathrm{dom}\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)\wedge G\mathrm{DProd}\left({S\upharpoonright }_{\left\{X\right\}}\right)\subseteq Z\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)\wedge \left(G\mathrm{DProd}\left({S\upharpoonright }_{\left\{X\right\}}\right)\right)\cap \left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)=\left\{0_G\right\}\right)\right)$$
16	1 15	mpbid	$$⊢\phi \to \left(\left(G\mathrm{dom}\mathrm{DProd}\left({S\upharpoonright }_{\left\{X\right\}}\right)\wedge G\mathrm{dom}\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)\wedge G\mathrm{DProd}\left({S\upharpoonright }_{\left\{X\right\}}\right)\subseteq Z\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)\wedge \left(G\mathrm{DProd}\left({S\upharpoonright }_{\left\{X\right\}}\right)\right)\cap \left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)=\left\{0_G\right\}\right)$$
17	16	simp2d	$$⊢\phi \to G\mathrm{DProd}\left({S\upharpoonright }_{\left\{X\right\}}\right)\subseteq Z\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)$$
18	5 17	eqsstrrd	$$⊢\phi \to S\left(X\right)\subseteq Z\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)$$