Theorem dmdprdsplit2

Description: The direct product splits into the direct product of any partition of the index set. (Contributed by Mario Carneiro, 25-Apr-2016)

	Ref	Expression
Hypotheses	dprdsplit.2	$$⊢\phi \to S:I⟶\mathrm{SubGrp}\left(G\right)$$
	dprdsplit.i	$$⊢\phi \to C\cap D=\varnothing$$
	dprdsplit.u	$$⊢\phi \to I=C\cup D$$
	dmdprdsplit.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
	dmdprdsplit.0	$$⊢\underset{\dot{}}{0}=0_G$$
	dmdprdsplit2.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}\left({S\upharpoonright }_C\right)$$
	dmdprdsplit2.2	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}\left({S\upharpoonright }_D\right)$$
	dmdprdsplit2.3	$$⊢\phi \to G\mathrm{DProd}\left({S\upharpoonright }_C\right)\subseteq Z\left(G\mathrm{DProd}\left({S\upharpoonright }_D\right)\right)$$
	dmdprdsplit2.4	$$⊢\phi \to \left(G\mathrm{DProd}\left({S\upharpoonright }_C\right)\right)\cap \left(G\mathrm{DProd}\left({S\upharpoonright }_D\right)\right)=\left\{\underset{\dot{}}{0}\right\}$$
Assertion	dmdprdsplit2	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$

Proof

Step	Hyp	Ref	Expression
1		dprdsplit.2	$$⊢\phi \to S:I⟶\mathrm{SubGrp}\left(G\right)$$
2		dprdsplit.i	$$⊢\phi \to C\cap D=\varnothing$$
3		dprdsplit.u	$$⊢\phi \to I=C\cup D$$
4		dmdprdsplit.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
5		dmdprdsplit.0	$$⊢\underset{\dot{}}{0}=0_G$$
6		dmdprdsplit2.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}\left({S\upharpoonright }_C\right)$$
7		dmdprdsplit2.2	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}\left({S\upharpoonright }_D\right)$$
8		dmdprdsplit2.3	$$⊢\phi \to G\mathrm{DProd}\left({S\upharpoonright }_C\right)\subseteq Z\left(G\mathrm{DProd}\left({S\upharpoonright }_D\right)\right)$$
9		dmdprdsplit2.4	$$⊢\phi \to \left(G\mathrm{DProd}\left({S\upharpoonright }_C\right)\right)\cap \left(G\mathrm{DProd}\left({S\upharpoonright }_D\right)\right)=\left\{\underset{\dot{}}{0}\right\}$$
10		eqid	$$⊢\mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)=\mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)$$
11		dprdgrp	$$⊢G\mathrm{dom}\mathrm{DProd}\left({S\upharpoonright }_C\right)\to G\in \mathrm{Grp}$$
12	6 11	syl	$$⊢\phi \to G\in \mathrm{Grp}$$
13		ssun1	$$⊢C\subseteq C\cup D$$
14	13 3	sseqtrrid	$$⊢\phi \to C\subseteq I$$
15	1 14	fssresd	$$⊢\phi \to \left({S\upharpoonright }_C\right):C⟶\mathrm{SubGrp}\left(G\right)$$
16	15	fdmd	$$⊢\phi \to \mathrm{dom}\left({S\upharpoonright }_C\right)=C$$
17	6 16	dprddomcld	$$⊢\phi \to C\in \mathrm{V}$$
18		ssun2	$$⊢D\subseteq C\cup D$$
19	18 3	sseqtrrid	$$⊢\phi \to D\subseteq I$$
20	1 19	fssresd	$$⊢\phi \to \left({S\upharpoonright }_D\right):D⟶\mathrm{SubGrp}\left(G\right)$$
21	20	fdmd	$$⊢\phi \to \mathrm{dom}\left({S\upharpoonright }_D\right)=D$$
22	7 21	dprddomcld	$$⊢\phi \to D\in \mathrm{V}$$
23		unexg	$$⊢\left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right)\to C\cup D\in \mathrm{V}$$
24	17 22 23	syl2anc	$$⊢\phi \to C\cup D\in \mathrm{V}$$
25	3 24	eqeltrd	$$⊢\phi \to I\in \mathrm{V}$$
26	3	eleq2d	$$⊢\phi \to \left(x\in I\leftrightarrow x\in \left(C\cup D\right)\right)$$
27		elun	$$⊢x\in \left(C\cup D\right)\leftrightarrow \left(x\in C\vee x\in D\right)$$
28	26 27	bitrdi	$$⊢\phi \to \left(x\in I\leftrightarrow \left(x\in C\vee x\in D\right)\right)$$
29	1 2 3 4 5 6 7 8 9 10	dmdprdsplit2lem	$$⊢\left(\phi \wedge x\in C\right)\to \left(\left(y\in I\to \left(x\ne y\to S\left(x\right)\subseteq Z\left(S\left(y\right)\right)\right)\right)\wedge S\left(x\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)\subseteq \left\{\underset{\dot{}}{0}\right\}\right)$$
30		incom	$$⊢C\cap D=D\cap C$$
31	30 2	eqtr3id	$$⊢\phi \to D\cap C=\varnothing$$
32		uncom	$$⊢C\cup D=D\cup C$$
33	3 32	eqtrdi	$$⊢\phi \to I=D\cup C$$
34		dprdsubg	$$⊢G\mathrm{dom}\mathrm{DProd}\left({S\upharpoonright }_C\right)\to G\mathrm{DProd}\left({S\upharpoonright }_C\right)\in \mathrm{SubGrp}\left(G\right)$$
35	6 34	syl	$$⊢\phi \to G\mathrm{DProd}\left({S\upharpoonright }_C\right)\in \mathrm{SubGrp}\left(G\right)$$
36		dprdsubg	$$⊢G\mathrm{dom}\mathrm{DProd}\left({S\upharpoonright }_D\right)\to G\mathrm{DProd}\left({S\upharpoonright }_D\right)\in \mathrm{SubGrp}\left(G\right)$$
37	7 36	syl	$$⊢\phi \to G\mathrm{DProd}\left({S\upharpoonright }_D\right)\in \mathrm{SubGrp}\left(G\right)$$
38	4 35 37 8	cntzrecd	$$⊢\phi \to G\mathrm{DProd}\left({S\upharpoonright }_D\right)\subseteq Z\left(G\mathrm{DProd}\left({S\upharpoonright }_C\right)\right)$$
39		incom	$$⊢\left(G\mathrm{DProd}\left({S\upharpoonright }_C\right)\right)\cap \left(G\mathrm{DProd}\left({S\upharpoonright }_D\right)\right)=\left(G\mathrm{DProd}\left({S\upharpoonright }_D\right)\right)\cap \left(G\mathrm{DProd}\left({S\upharpoonright }_C\right)\right)$$
40	39 9	eqtr3id	$$⊢\phi \to \left(G\mathrm{DProd}\left({S\upharpoonright }_D\right)\right)\cap \left(G\mathrm{DProd}\left({S\upharpoonright }_C\right)\right)=\left\{\underset{\dot{}}{0}\right\}$$
41	1 31 33 4 5 7 6 38 40 10	dmdprdsplit2lem	$$⊢\left(\phi \wedge x\in D\right)\to \left(\left(y\in I\to \left(x\ne y\to S\left(x\right)\subseteq Z\left(S\left(y\right)\right)\right)\right)\wedge S\left(x\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)\subseteq \left\{\underset{\dot{}}{0}\right\}\right)$$
42	29 41	jaodan	$$⊢\left(\phi \wedge \left(x\in C\vee x\in D\right)\right)\to \left(\left(y\in I\to \left(x\ne y\to S\left(x\right)\subseteq Z\left(S\left(y\right)\right)\right)\right)\wedge S\left(x\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)\subseteq \left\{\underset{\dot{}}{0}\right\}\right)$$
43	42	simpld	$$⊢\left(\phi \wedge \left(x\in C\vee x\in D\right)\right)\to \left(y\in I\to \left(x\ne y\to S\left(x\right)\subseteq Z\left(S\left(y\right)\right)\right)\right)$$
44	43	ex	$$⊢\phi \to \left(\left(x\in C\vee x\in D\right)\to \left(y\in I\to \left(x\ne y\to S\left(x\right)\subseteq Z\left(S\left(y\right)\right)\right)\right)\right)$$
45	28 44	sylbid	$$⊢\phi \to \left(x\in I\to \left(y\in I\to \left(x\ne y\to S\left(x\right)\subseteq Z\left(S\left(y\right)\right)\right)\right)\right)$$
46	45	3imp2	$$⊢\left(\phi \wedge \left(x\in I\wedge y\in I\wedge x\ne y\right)\right)\to S\left(x\right)\subseteq Z\left(S\left(y\right)\right)$$
47	28	biimpa	$$⊢\left(\phi \wedge x\in I\right)\to \left(x\in C\vee x\in D\right)$$
48	29	simprd	$$⊢\left(\phi \wedge x\in C\right)\to S\left(x\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)\subseteq \left\{\underset{\dot{}}{0}\right\}$$
49	41	simprd	$$⊢\left(\phi \wedge x\in D\right)\to S\left(x\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)\subseteq \left\{\underset{\dot{}}{0}\right\}$$
50	48 49	jaodan	$$⊢\left(\phi \wedge \left(x\in C\vee x\in D\right)\right)\to S\left(x\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)\subseteq \left\{\underset{\dot{}}{0}\right\}$$
51	47 50	syldan	$$⊢\left(\phi \wedge x\in I\right)\to S\left(x\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)\subseteq \left\{\underset{\dot{}}{0}\right\}$$
52	4 5 10 12 25 1 46 51	dmdprdd	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$