Theorem dprdcntz

Description: The function S is a family having pairwise commuting values. (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$$
	dprdcntz.4	$$⊢\phi \to Y\in I$$
	dprdcntz.5	$$⊢\phi \to X\ne Y$$
	dprdcntz.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
Assertion	dprdcntz	$$⊢\phi \to S\left(X\right)\subseteq Z\left(S\left(Y\right)\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		dprdcntz.4	$$⊢\phi \to Y\in I$$
5		dprdcntz.5	$$⊢\phi \to X\ne Y$$
6		dprdcntz.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
7		2fveq3	$$⊢y=Y\to Z\left(S\left(y\right)\right)=Z\left(S\left(Y\right)\right)$$
8	7	sseq2d	$$⊢y=Y\to \left(S\left(X\right)\subseteq Z\left(S\left(y\right)\right)\leftrightarrow S\left(X\right)\subseteq Z\left(S\left(Y\right)\right)\right)$$
9		sneq	$$⊢x=X\to \left\{x\right\}=\left\{X\right\}$$
10	9	difeq2d	$$⊢x=X\to I\setminus \left\{x\right\}=I\setminus \left\{X\right\}$$
11		fveq2	$$⊢x=X\to S\left(x\right)=S\left(X\right)$$
12	11	sseq1d	$$⊢x=X\to \left(S\left(x\right)\subseteq Z\left(S\left(y\right)\right)\leftrightarrow S\left(X\right)\subseteq Z\left(S\left(y\right)\right)\right)$$
13	10 12	raleqbidv	$$⊢x=X\to \left(\forall y\in \left(I\setminus \left\{x\right\}\right)S\left(x\right)\subseteq Z\left(S\left(y\right)\right)\leftrightarrow \forall y\in \left(I\setminus \left\{X\right\}\right)S\left(X\right)\subseteq Z\left(S\left(y\right)\right)\right)$$
14	1 2	dprddomcld	$$⊢\phi \to I\in \mathrm{V}$$
15		eqid	$$⊢0_G=0_G$$
16		eqid	$$⊢\mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)=\mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)$$
17	6 15 16	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 Z\left(S\left(y\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)=\left\{0_G\right\}\right)\right)\right)$$
18	14 2 17	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 Z\left(S\left(y\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)=\left\{0_G\right\}\right)\right)\right)$$
19	1 18	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 Z\left(S\left(y\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)=\left\{0_G\right\}\right)\right)$$
20	19	simp3d	$$⊢\phi \to \forall x\in I\left(\forall y\in \left(I\setminus \left\{x\right\}\right)S\left(x\right)\subseteq Z\left(S\left(y\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)=\left\{0_G\right\}\right)$$
21		simpl	$$⊢\left(\forall y\in \left(I\setminus \left\{x\right\}\right)S\left(x\right)\subseteq Z\left(S\left(y\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)=\left\{0_G\right\}\right)\to \forall y\in \left(I\setminus \left\{x\right\}\right)S\left(x\right)\subseteq Z\left(S\left(y\right)\right)$$
22	21	ralimi	$$⊢\forall x\in I\left(\forall y\in \left(I\setminus \left\{x\right\}\right)S\left(x\right)\subseteq Z\left(S\left(y\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)=\left\{0_G\right\}\right)\to \forall x\in I\forall y\in \left(I\setminus \left\{x\right\}\right)S\left(x\right)\subseteq Z\left(S\left(y\right)\right)$$
23	20 22	syl	$$⊢\phi \to \forall x\in I\forall y\in \left(I\setminus \left\{x\right\}\right)S\left(x\right)\subseteq Z\left(S\left(y\right)\right)$$
24	13 23 3	rspcdva	$$⊢\phi \to \forall y\in \left(I\setminus \left\{X\right\}\right)S\left(X\right)\subseteq Z\left(S\left(y\right)\right)$$
25	5	necomd	$$⊢\phi \to Y\ne X$$
26		eldifsn	$$⊢Y\in \left(I\setminus \left\{X\right\}\right)\leftrightarrow \left(Y\in I\wedge Y\ne X\right)$$
27	4 25 26	sylanbrc	$$⊢\phi \to Y\in \left(I\setminus \left\{X\right\}\right)$$
28	8 24 27	rspcdva	$$⊢\phi \to S\left(X\right)\subseteq Z\left(S\left(Y\right)\right)$$