Theorem dpjlsm

Description: The two subgroups that appear in dpjval add to the full direct product. (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$$
	dpjlsm.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
Assertion	dpjlsm	$$⊢\phi \to G\mathrm{DProd}S=S\left(X\right)\underset{\dot{}}{\oplus }\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		dpjlsm.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
5	1 2	dprdf2	$$⊢\phi \to S:I⟶\mathrm{SubGrp}\left(G\right)$$
6		disjdif	$$⊢\left\{X\right\}\cap \left(I\setminus \left\{X\right\}\right)=\varnothing$$
7	6	a1i	$$⊢\phi \to \left\{X\right\}\cap \left(I\setminus \left\{X\right\}\right)=\varnothing$$
8		undif2	$$⊢\left\{X\right\}\cup \left(I\setminus \left\{X\right\}\right)=\left\{X\right\}\cup I$$
9	3	snssd	$$⊢\phi \to \left\{X\right\}\subseteq I$$
10		ssequn1	$$⊢\left\{X\right\}\subseteq I\leftrightarrow \left\{X\right\}\cup I=I$$
11	9 10	sylib	$$⊢\phi \to \left\{X\right\}\cup I=I$$
12	8 11	syl5req	$$⊢\phi \to I=\left\{X\right\}\cup \left(I\setminus \left\{X\right\}\right)$$
13	5 7 12 4 1	dprdsplit	$$⊢\phi \to G\mathrm{DProd}S=\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left\{X\right\}}\right)\right)\underset{\dot{}}{\oplus }\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)$$
14	1 2 3	dpjlem	$$⊢\phi \to G\mathrm{DProd}\left({S\upharpoonright }_{\left\{X\right\}}\right)=S\left(X\right)$$
15	14	oveq1d	$$⊢\phi \to \left(G\mathrm{DProd}\left({S\upharpoonright }_{\left\{X\right\}}\right)\right)\underset{\dot{}}{\oplus }\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)=S\left(X\right)\underset{\dot{}}{\oplus }\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)$$
16	13 15	eqtrd	$$⊢\phi \to G\mathrm{DProd}S=S\left(X\right)\underset{\dot{}}{\oplus }\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)$$