Theorem dprddisj

Description: The function S is a family having trivial intersections. (Contributed by Mario Carneiro, 25-Apr-2016)

	Ref	Expression
Hypotheses	dprdcntz.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
	dprdcntz.2	$$⊢\phi \to \mathrm{dom}S=I$$
	dprdcntz.3	$$⊢\phi \to X\in I$$
	dprddisj.0	$$⊢\underset{\dot{}}{0}=0_G$$
	dprddisj.k	$$⊢K=\mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)$$
Assertion	dprddisj	$$⊢\phi \to S\left(X\right)\cap K\left(\bigcup S\left[I\setminus \left\{X\right\}\right]\right)=\left\{\underset{\dot{}}{0}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dprdcntz.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
2		dprdcntz.2	$$⊢\phi \to \mathrm{dom}S=I$$
3		dprdcntz.3	$$⊢\phi \to X\in I$$
4		dprddisj.0	$$⊢\underset{\dot{}}{0}=0_G$$
5		dprddisj.k	$$⊢K=\mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)$$
6		fveq2	$$⊢x=X\to S\left(x\right)=S\left(X\right)$$
7		sneq	$$⊢x=X\to \left\{x\right\}=\left\{X\right\}$$
8	7	difeq2d	$$⊢x=X\to I\setminus \left\{x\right\}=I\setminus \left\{X\right\}$$
9	8	imaeq2d	$$⊢x=X\to S\left[I\setminus \left\{x\right\}\right]=S\left[I\setminus \left\{X\right\}\right]$$
10	9	unieqd	$$⊢x=X\to \bigcup S\left[I\setminus \left\{x\right\}\right]=\bigcup S\left[I\setminus \left\{X\right\}\right]$$
11	10	fveq2d	$$⊢x=X\to K\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)=K\left(\bigcup S\left[I\setminus \left\{X\right\}\right]\right)$$
12	6 11	ineq12d	$$⊢x=X\to S\left(x\right)\cap K\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)=S\left(X\right)\cap K\left(\bigcup S\left[I\setminus \left\{X\right\}\right]\right)$$
13	12	eqeq1d	$$⊢x=X\to \left(S\left(x\right)\cap K\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow S\left(X\right)\cap K\left(\bigcup S\left[I\setminus \left\{X\right\}\right]\right)=\left\{\underset{\dot{}}{0}\right\}\right)$$
14	1 2	dprddomcld	$$⊢\phi \to I\in \mathrm{V}$$
15		eqid	$$⊢\mathrm{Cntz}\left(G\right)=\mathrm{Cntz}\left(G\right)$$
16	15 4 5	dmdprd	$$⊢\left(I\in \mathrm{V}\wedge \mathrm{dom}S=I\right)\to \left(G\mathrm{dom}\mathrm{DProd}S\leftrightarrow \left(G\in \mathrm{Grp}\wedge S:I⟶\mathrm{SubGrp}\left(G\right)\wedge \forall x\in I\left(\forall y\in \left(I\setminus \left\{x\right\}\right)S\left(x\right)\subseteq \mathrm{Cntz}\left(G\right)\left(S\left(y\right)\right)\wedge S\left(x\right)\cap K\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)=\left\{\underset{\dot{}}{0}\right\}\right)\right)\right)$$
17	14 2 16	syl2anc	$$⊢\phi \to \left(G\mathrm{dom}\mathrm{DProd}S\leftrightarrow \left(G\in \mathrm{Grp}\wedge S:I⟶\mathrm{SubGrp}\left(G\right)\wedge \forall x\in I\left(\forall y\in \left(I\setminus \left\{x\right\}\right)S\left(x\right)\subseteq \mathrm{Cntz}\left(G\right)\left(S\left(y\right)\right)\wedge S\left(x\right)\cap K\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)=\left\{\underset{\dot{}}{0}\right\}\right)\right)\right)$$
18	1 17	mpbid	$$⊢\phi \to \left(G\in \mathrm{Grp}\wedge S:I⟶\mathrm{SubGrp}\left(G\right)\wedge \forall x\in I\left(\forall y\in \left(I\setminus \left\{x\right\}\right)S\left(x\right)\subseteq \mathrm{Cntz}\left(G\right)\left(S\left(y\right)\right)\wedge S\left(x\right)\cap K\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)=\left\{\underset{\dot{}}{0}\right\}\right)\right)$$
19	18	simp3d	$$⊢\phi \to \forall x\in I\left(\forall y\in \left(I\setminus \left\{x\right\}\right)S\left(x\right)\subseteq \mathrm{Cntz}\left(G\right)\left(S\left(y\right)\right)\wedge S\left(x\right)\cap K\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)=\left\{\underset{\dot{}}{0}\right\}\right)$$
20		simpr	$$⊢\left(\forall y\in \left(I\setminus \left\{x\right\}\right)S\left(x\right)\subseteq \mathrm{Cntz}\left(G\right)\left(S\left(y\right)\right)\wedge S\left(x\right)\cap K\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)=\left\{\underset{\dot{}}{0}\right\}\right)\to S\left(x\right)\cap K\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)=\left\{\underset{\dot{}}{0}\right\}$$
21	20	ralimi	$$⊢\forall x\in I\left(\forall y\in \left(I\setminus \left\{x\right\}\right)S\left(x\right)\subseteq \mathrm{Cntz}\left(G\right)\left(S\left(y\right)\right)\wedge S\left(x\right)\cap K\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)=\left\{\underset{\dot{}}{0}\right\}\right)\to \forall x\in IS\left(x\right)\cap K\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)=\left\{\underset{\dot{}}{0}\right\}$$
22	19 21	syl	$$⊢\phi \to \forall x\in IS\left(x\right)\cap K\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)=\left\{\underset{\dot{}}{0}\right\}$$
23	13 22 3	rspcdva	$$⊢\phi \to S\left(X\right)\cap K\left(\bigcup S\left[I\setminus \left\{X\right\}\right]\right)=\left\{\underset{\dot{}}{0}\right\}$$