dprdf1

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

	Ref	Expression
Hypotheses	dprdf1.1	\|- ( ph -> G dom DProd S )
	dprdf1.2	\|- ( ph -> dom S = I )
	dprdf1.3	\|- ( ph -> F : J -1-1-> I )
Assertion	dprdf1	\|- ( ph -> ( G dom DProd ( S o. F ) /\ ( G DProd ( S o. F ) ) C_ ( G DProd S ) ) )

Step	Hyp	Ref	Expression
1		dprdf1.1	\|- ( ph -> G dom DProd S )
2		dprdf1.2	\|- ( ph -> dom S = I )
3		dprdf1.3	\|- ( ph -> F : J -1-1-> I )
4		f1f	\|- ( F : J -1-1-> I -> F : J --> I )
5		frn	\|- ( F : J --> I -> ran F C_ I )
6	3 4 5	3syl	\|- ( ph -> ran F C_ I )
7	1 2 6	dprdres	\|- ( ph -> ( G dom DProd ( S \|` ran F ) /\ ( G DProd ( S \|` ran F ) ) C_ ( G DProd S ) ) )
8	7	simpld	\|- ( ph -> G dom DProd ( S \|` ran F ) )
9	1 2	dprdf2	\|- ( ph -> S : I --> ( SubGrp ` G ) )
10	9 6	fssresd	\|- ( ph -> ( S \|` ran F ) : ran F --> ( SubGrp ` G ) )
11	10	fdmd	\|- ( ph -> dom ( S \|` ran F ) = ran F )
12		f1f1orn	\|- ( F : J -1-1-> I -> F : J -1-1-onto-> ran F )
13	3 12	syl	\|- ( ph -> F : J -1-1-onto-> ran F )
14	8 11 13	dprdf1o	\|- ( ph -> ( G dom DProd ( ( S \|` ran F ) o. F ) /\ ( G DProd ( ( S \|` ran F ) o. F ) ) = ( G DProd ( S \|` ran F ) ) ) )
15	14	simpld	\|- ( ph -> G dom DProd ( ( S \|` ran F ) o. F ) )
16		ssid	\|- ran F C_ ran F
17		cores	\|- ( ran F C_ ran F -> ( ( S \|` ran F ) o. F ) = ( S o. F ) )
18	16 17	ax-mp	\|- ( ( S \|` ran F ) o. F ) = ( S o. F )
19	15 18	breqtrdi	\|- ( ph -> G dom DProd ( S o. F ) )
20	18	oveq2i	\|- ( G DProd ( ( S \|` ran F ) o. F ) ) = ( G DProd ( S o. F ) )
21	14	simprd	\|- ( ph -> ( G DProd ( ( S \|` ran F ) o. F ) ) = ( G DProd ( S \|` ran F ) ) )
22	20 21	eqtr3id	\|- ( ph -> ( G DProd ( S o. F ) ) = ( G DProd ( S \|` ran F ) ) )
23	7	simprd	\|- ( ph -> ( G DProd ( S \|` ran F ) ) C_ ( G DProd S ) )
24	22 23	eqsstrd	\|- ( ph -> ( G DProd ( S o. F ) ) C_ ( G DProd S ) )
25	19 24	jca	\|- ( ph -> ( G dom DProd ( S o. F ) /\ ( G DProd ( S o. F ) ) C_ ( G DProd S ) ) )

Metamath Proof Explorer