Metamath Proof Explorer


Theorem dprdf1

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

Ref Expression
Hypotheses dprdf1.1 φ G dom DProd S
dprdf1.2 φ dom S = I
dprdf1.3 φ F : J 1-1 I
Assertion dprdf1 φ G dom DProd S F G DProd S F G DProd S

Proof

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