Theorem dpjdisj

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