Theorem dprdf1

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

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

Proof

Step	Hyp	Ref	Expression
1		dprdf1.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
2		dprdf1.2	$$⊢\phi \to \mathrm{dom}S=I$$
3		dprdf1.3	$$⊢\phi \to F:J\underset{1-1}{⟶}I$$
4		f1f	$$⊢F:J\underset{1-1}{⟶}I\to F:J⟶I$$
5		frn	$$⊢F:J⟶I\to \mathrm{ran}F\subseteq I$$
6	3 4 5	3syl	$$⊢\phi \to \mathrm{ran}F\subseteq I$$
7	1 2 6	dprdres	$$⊢\phi \to \left(G\mathrm{dom}\mathrm{DProd}\left({S\upharpoonright }_{\mathrm{ran}F}\right)\wedge G\mathrm{DProd}\left({S\upharpoonright }_{\mathrm{ran}F}\right)\subseteq G\mathrm{DProd}S\right)$$
8	7	simpld	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}\left({S\upharpoonright }_{\mathrm{ran}F}\right)$$
9	1 2	dprdf2	$$⊢\phi \to S:I⟶\mathrm{SubGrp}\left(G\right)$$
10	9 6	fssresd	$$⊢\phi \to \left({S\upharpoonright }_{\mathrm{ran}F}\right):\mathrm{ran}F⟶\mathrm{SubGrp}\left(G\right)$$
11	10	fdmd	$$⊢\phi \to \mathrm{dom}\left({S\upharpoonright }_{\mathrm{ran}F}\right)=\mathrm{ran}F$$
12		f1f1orn	$$⊢F:J\underset{1-1}{⟶}I\to F:J\underset{1-1\; onto}{⟶}\mathrm{ran}F$$
13	3 12	syl	$$⊢\phi \to F:J\underset{1-1\; onto}{⟶}\mathrm{ran}F$$
14	8 11 13	dprdf1o	$$⊢\phi \to \left(G\mathrm{dom}\mathrm{DProd}\left(\left({S\upharpoonright }_{\mathrm{ran}F}\right)\circ F\right)\wedge G\mathrm{DProd}\left(\left({S\upharpoonright }_{\mathrm{ran}F}\right)\circ F\right)=G\mathrm{DProd}\left({S\upharpoonright }_{\mathrm{ran}F}\right)\right)$$
15	14	simpld	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}\left(\left({S\upharpoonright }_{\mathrm{ran}F}\right)\circ F\right)$$
16		ssid	$$⊢\mathrm{ran}F\subseteq \mathrm{ran}F$$
17		cores	$$⊢\mathrm{ran}F\subseteq \mathrm{ran}F\to \left({S\upharpoonright }_{\mathrm{ran}F}\right)\circ F=S\circ F$$
18	16 17	ax-mp	$$⊢\left({S\upharpoonright }_{\mathrm{ran}F}\right)\circ F=S\circ F$$
19	15 18	breqtrdi	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}\left(S\circ F\right)$$
20	18	oveq2i	$$⊢G\mathrm{DProd}\left(\left({S\upharpoonright }_{\mathrm{ran}F}\right)\circ F\right)=G\mathrm{DProd}\left(S\circ F\right)$$
21	14	simprd	$$⊢\phi \to G\mathrm{DProd}\left(\left({S\upharpoonright }_{\mathrm{ran}F}\right)\circ F\right)=G\mathrm{DProd}\left({S\upharpoonright }_{\mathrm{ran}F}\right)$$
22	20 21	syl5eqr	$$⊢\phi \to G\mathrm{DProd}\left(S\circ F\right)=G\mathrm{DProd}\left({S\upharpoonright }_{\mathrm{ran}F}\right)$$
23	7	simprd	$$⊢\phi \to G\mathrm{DProd}\left({S\upharpoonright }_{\mathrm{ran}F}\right)\subseteq G\mathrm{DProd}S$$
24	22 23	eqsstrd	$$⊢\phi \to G\mathrm{DProd}\left(S\circ F\right)\subseteq G\mathrm{DProd}S$$
25	19 24	jca	$$⊢\phi \to \left(G\mathrm{dom}\mathrm{DProd}\left(S\circ F\right)\wedge G\mathrm{DProd}\left(S\circ F\right)\subseteq G\mathrm{DProd}S\right)$$