Theorem dprdf1o

Description: Rearrange the index set of a direct product family. (Contributed by Mario Carneiro, 25-Apr-2016)

	Ref	Expression
Hypotheses	dprdf1o.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
	dprdf1o.2	$$⊢\phi \to \mathrm{dom}S=I$$
	dprdf1o.3	$$⊢\phi \to F:J\underset{1-1\; onto}{⟶}I$$
Assertion	dprdf1o	$$⊢\phi \to \left(G\mathrm{dom}\mathrm{DProd}\left(S\circ F\right)\wedge G\mathrm{DProd}\left(S\circ F\right)=G\mathrm{DProd}S\right)$$

Proof

Step	Hyp	Ref	Expression
1		dprdf1o.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
2		dprdf1o.2	$$⊢\phi \to \mathrm{dom}S=I$$
3		dprdf1o.3	$$⊢\phi \to F:J\underset{1-1\; onto}{⟶}I$$
4		eqid	$$⊢\mathrm{Cntz}\left(G\right)=\mathrm{Cntz}\left(G\right)$$
5		eqid	$$⊢0_G=0_G$$
6		eqid	$$⊢\mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)=\mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)$$
7		dprdgrp	$$⊢G\mathrm{dom}\mathrm{DProd}S\to G\in \mathrm{Grp}$$
8	1 7	syl	$$⊢\phi \to G\in \mathrm{Grp}$$
9		f1of1	$$⊢F:J\underset{1-1\; onto}{⟶}I\to F:J\underset{1-1}{⟶}I$$
10	3 9	syl	$$⊢\phi \to F:J\underset{1-1}{⟶}I$$
11	1 2	dprddomcld	$$⊢\phi \to I\in \mathrm{V}$$
12		f1dmex	$$⊢\left(F:J\underset{1-1}{⟶}I\wedge I\in \mathrm{V}\right)\to J\in \mathrm{V}$$
13	10 11 12	syl2anc	$$⊢\phi \to J\in \mathrm{V}$$
14	1 2	dprdf2	$$⊢\phi \to S:I⟶\mathrm{SubGrp}\left(G\right)$$
15		f1of	$$⊢F:J\underset{1-1\; onto}{⟶}I\to F:J⟶I$$
16	3 15	syl	$$⊢\phi \to F:J⟶I$$
17		fco	$$⊢\left(S:I⟶\mathrm{SubGrp}\left(G\right)\wedge F:J⟶I\right)\to \left(S\circ F\right):J⟶\mathrm{SubGrp}\left(G\right)$$
18	14 16 17	syl2anc	$$⊢\phi \to \left(S\circ F\right):J⟶\mathrm{SubGrp}\left(G\right)$$
19	1	adantr	$$⊢\left(\phi \wedge \left(x\in J\wedge y\in J\wedge x\ne y\right)\right)\to G\mathrm{dom}\mathrm{DProd}S$$
20	2	adantr	$$⊢\left(\phi \wedge \left(x\in J\wedge y\in J\wedge x\ne y\right)\right)\to \mathrm{dom}S=I$$
21	16	adantr	$$⊢\left(\phi \wedge \left(x\in J\wedge y\in J\wedge x\ne y\right)\right)\to F:J⟶I$$
22		simpr1	$$⊢\left(\phi \wedge \left(x\in J\wedge y\in J\wedge x\ne y\right)\right)\to x\in J$$
23	21 22	ffvelrnd	$$⊢\left(\phi \wedge \left(x\in J\wedge y\in J\wedge x\ne y\right)\right)\to F\left(x\right)\in I$$
24		simpr2	$$⊢\left(\phi \wedge \left(x\in J\wedge y\in J\wedge x\ne y\right)\right)\to y\in J$$
25	21 24	ffvelrnd	$$⊢\left(\phi \wedge \left(x\in J\wedge y\in J\wedge x\ne y\right)\right)\to F\left(y\right)\in I$$
26		simpr3	$$⊢\left(\phi \wedge \left(x\in J\wedge y\in J\wedge x\ne y\right)\right)\to x\ne y$$
27	10	adantr	$$⊢\left(\phi \wedge \left(x\in J\wedge y\in J\wedge x\ne y\right)\right)\to F:J\underset{1-1}{⟶}I$$
28		f1fveq	$$⊢\left(F:J\underset{1-1}{⟶}I\wedge \left(x\in J\wedge y\in J\right)\right)\to \left(F\left(x\right)=F\left(y\right)\leftrightarrow x=y\right)$$
29	27 22 24 28	syl12anc	$$⊢\left(\phi \wedge \left(x\in J\wedge y\in J\wedge x\ne y\right)\right)\to \left(F\left(x\right)=F\left(y\right)\leftrightarrow x=y\right)$$
30	29	necon3bid	$$⊢\left(\phi \wedge \left(x\in J\wedge y\in J\wedge x\ne y\right)\right)\to \left(F\left(x\right)\ne F\left(y\right)\leftrightarrow x\ne y\right)$$
31	26 30	mpbird	$$⊢\left(\phi \wedge \left(x\in J\wedge y\in J\wedge x\ne y\right)\right)\to F\left(x\right)\ne F\left(y\right)$$
32	19 20 23 25 31 4	dprdcntz	$$⊢\left(\phi \wedge \left(x\in J\wedge y\in J\wedge x\ne y\right)\right)\to S\left(F\left(x\right)\right)\subseteq \mathrm{Cntz}\left(G\right)\left(S\left(F\left(y\right)\right)\right)$$
33		fvco3	$$⊢\left(F:J⟶I\wedge x\in J\right)\to \left(S\circ F\right)\left(x\right)=S\left(F\left(x\right)\right)$$
34	21 22 33	syl2anc	$$⊢\left(\phi \wedge \left(x\in J\wedge y\in J\wedge x\ne y\right)\right)\to \left(S\circ F\right)\left(x\right)=S\left(F\left(x\right)\right)$$
35		fvco3	$$⊢\left(F:J⟶I\wedge y\in J\right)\to \left(S\circ F\right)\left(y\right)=S\left(F\left(y\right)\right)$$
36	21 24 35	syl2anc	$$⊢\left(\phi \wedge \left(x\in J\wedge y\in J\wedge x\ne y\right)\right)\to \left(S\circ F\right)\left(y\right)=S\left(F\left(y\right)\right)$$
37	36	fveq2d	$$⊢\left(\phi \wedge \left(x\in J\wedge y\in J\wedge x\ne y\right)\right)\to \mathrm{Cntz}\left(G\right)\left(\left(S\circ F\right)\left(y\right)\right)=\mathrm{Cntz}\left(G\right)\left(S\left(F\left(y\right)\right)\right)$$
38	32 34 37	3sstr4d	$$⊢\left(\phi \wedge \left(x\in J\wedge y\in J\wedge x\ne y\right)\right)\to \left(S\circ F\right)\left(x\right)\subseteq \mathrm{Cntz}\left(G\right)\left(\left(S\circ F\right)\left(y\right)\right)$$
39	16 33	sylan	$$⊢\left(\phi \wedge x\in J\right)\to \left(S\circ F\right)\left(x\right)=S\left(F\left(x\right)\right)$$
40		imaco	$$⊢\left(S\circ F\right)\left[J\setminus \left\{x\right\}\right]=S\left[F\left[J\setminus \left\{x\right\}\right]\right]$$
41	3	adantr	$$⊢\left(\phi \wedge x\in J\right)\to F:J\underset{1-1\; onto}{⟶}I$$
42		dff1o3	$$⊢F:J\underset{1-1\; onto}{⟶}I\leftrightarrow \left(F:J\underset{onto}{⟶}I\wedge \mathrm{Fun}{F}^{-1}\right)$$
43	42	simprbi	$$⊢F:J\underset{1-1\; onto}{⟶}I\to \mathrm{Fun}{F}^{-1}$$
44		imadif	$$⊢\mathrm{Fun}{F}^{-1}\to F\left[J\setminus \left\{x\right\}\right]=F\left[J\right]\setminus F\left[\left\{x\right\}\right]$$
45	41 43 44	3syl	$$⊢\left(\phi \wedge x\in J\right)\to F\left[J\setminus \left\{x\right\}\right]=F\left[J\right]\setminus F\left[\left\{x\right\}\right]$$
46		f1ofo	$$⊢F:J\underset{1-1\; onto}{⟶}I\to F:J\underset{onto}{⟶}I$$
47		foima	$$⊢F:J\underset{onto}{⟶}I\to F\left[J\right]=I$$
48	41 46 47	3syl	$$⊢\left(\phi \wedge x\in J\right)\to F\left[J\right]=I$$
49		f1ofn	$$⊢F:J\underset{1-1\; onto}{⟶}I\to FFnJ$$
50	3 49	syl	$$⊢\phi \to FFnJ$$
51		fnsnfv	$$⊢\left(FFnJ\wedge x\in J\right)\to \left\{F\left(x\right)\right\}=F\left[\left\{x\right\}\right]$$
52	50 51	sylan	$$⊢\left(\phi \wedge x\in J\right)\to \left\{F\left(x\right)\right\}=F\left[\left\{x\right\}\right]$$
53	52	eqcomd	$$⊢\left(\phi \wedge x\in J\right)\to F\left[\left\{x\right\}\right]=\left\{F\left(x\right)\right\}$$
54	48 53	difeq12d	$$⊢\left(\phi \wedge x\in J\right)\to F\left[J\right]\setminus F\left[\left\{x\right\}\right]=I\setminus \left\{F\left(x\right)\right\}$$
55	45 54	eqtrd	$$⊢\left(\phi \wedge x\in J\right)\to F\left[J\setminus \left\{x\right\}\right]=I\setminus \left\{F\left(x\right)\right\}$$
56	55	imaeq2d	$$⊢\left(\phi \wedge x\in J\right)\to S\left[F\left[J\setminus \left\{x\right\}\right]\right]=S\left[I\setminus \left\{F\left(x\right)\right\}\right]$$
57	40 56	syl5eq	$$⊢\left(\phi \wedge x\in J\right)\to \left(S\circ F\right)\left[J\setminus \left\{x\right\}\right]=S\left[I\setminus \left\{F\left(x\right)\right\}\right]$$
58	57	unieqd	$$⊢\left(\phi \wedge x\in J\right)\to \bigcup \left(S\circ F\right)\left[J\setminus \left\{x\right\}\right]=\bigcup S\left[I\setminus \left\{F\left(x\right)\right\}\right]$$
59	58	fveq2d	$$⊢\left(\phi \wedge x\in J\right)\to \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup \left(S\circ F\right)\left[J\setminus \left\{x\right\}\right]\right)=\mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{F\left(x\right)\right\}\right]\right)$$
60	39 59	ineq12d	$$⊢\left(\phi \wedge x\in J\right)\to \left(S\circ F\right)\left(x\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup \left(S\circ F\right)\left[J\setminus \left\{x\right\}\right]\right)=S\left(F\left(x\right)\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{F\left(x\right)\right\}\right]\right)$$
61	1	adantr	$$⊢\left(\phi \wedge x\in J\right)\to G\mathrm{dom}\mathrm{DProd}S$$
62	2	adantr	$$⊢\left(\phi \wedge x\in J\right)\to \mathrm{dom}S=I$$
63	16	ffvelrnda	$$⊢\left(\phi \wedge x\in J\right)\to F\left(x\right)\in I$$
64	61 62 63 5 6	dprddisj	$$⊢\left(\phi \wedge x\in J\right)\to S\left(F\left(x\right)\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{F\left(x\right)\right\}\right]\right)=\left\{0_G\right\}$$
65	60 64	eqtrd	$$⊢\left(\phi \wedge x\in J\right)\to \left(S\circ F\right)\left(x\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup \left(S\circ F\right)\left[J\setminus \left\{x\right\}\right]\right)=\left\{0_G\right\}$$
66		eqimss	$$⊢\left(S\circ F\right)\left(x\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup \left(S\circ F\right)\left[J\setminus \left\{x\right\}\right]\right)=\left\{0_G\right\}\to \left(S\circ F\right)\left(x\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup \left(S\circ F\right)\left[J\setminus \left\{x\right\}\right]\right)\subseteq \left\{0_G\right\}$$
67	65 66	syl	$$⊢\left(\phi \wedge x\in J\right)\to \left(S\circ F\right)\left(x\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup \left(S\circ F\right)\left[J\setminus \left\{x\right\}\right]\right)\subseteq \left\{0_G\right\}$$
68	4 5 6 8 13 18 38 67	dmdprdd	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}\left(S\circ F\right)$$
69		rnco2	$$⊢\mathrm{ran}\left(S\circ F\right)=S\left[\mathrm{ran}F\right]$$
70		forn	$$⊢F:J\underset{onto}{⟶}I\to \mathrm{ran}F=I$$
71	3 46 70	3syl	$$⊢\phi \to \mathrm{ran}F=I$$
72	71	imaeq2d	$$⊢\phi \to S\left[\mathrm{ran}F\right]=S\left[I\right]$$
73		ffn	$$⊢S:I⟶\mathrm{SubGrp}\left(G\right)\to SFnI$$
74		fnima	$$⊢SFnI\to S\left[I\right]=\mathrm{ran}S$$
75	14 73 74	3syl	$$⊢\phi \to S\left[I\right]=\mathrm{ran}S$$
76	72 75	eqtrd	$$⊢\phi \to S\left[\mathrm{ran}F\right]=\mathrm{ran}S$$
77	69 76	syl5eq	$$⊢\phi \to \mathrm{ran}\left(S\circ F\right)=\mathrm{ran}S$$
78	77	unieqd	$$⊢\phi \to \bigcup \mathrm{ran}\left(S\circ F\right)=\bigcup \mathrm{ran}S$$
79	78	fveq2d	$$⊢\phi \to \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup \mathrm{ran}\left(S\circ F\right)\right)=\mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup \mathrm{ran}S\right)$$
80	6	dprdspan	$$⊢G\mathrm{dom}\mathrm{DProd}\left(S\circ F\right)\to G\mathrm{DProd}\left(S\circ F\right)=\mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup \mathrm{ran}\left(S\circ F\right)\right)$$
81	68 80	syl	$$⊢\phi \to G\mathrm{DProd}\left(S\circ F\right)=\mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup \mathrm{ran}\left(S\circ F\right)\right)$$
82	6	dprdspan	$$⊢G\mathrm{dom}\mathrm{DProd}S\to G\mathrm{DProd}S=\mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup \mathrm{ran}S\right)$$
83	1 82	syl	$$⊢\phi \to G\mathrm{DProd}S=\mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup \mathrm{ran}S\right)$$
84	79 81 83	3eqtr4d	$$⊢\phi \to G\mathrm{DProd}\left(S\circ F\right)=G\mathrm{DProd}S$$
85	68 84	jca	$$⊢\phi \to \left(G\mathrm{dom}\mathrm{DProd}\left(S\circ F\right)\wedge G\mathrm{DProd}\left(S\circ F\right)=G\mathrm{DProd}S\right)$$