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 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
dprdf1.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
dprdf1.3 ⊢ ( 𝜑 → 𝐹 : 𝐽 –1-1→ 𝐼 )
Assertion dprdf1 ( 𝜑 → ( 𝐺 dom DProd ( 𝑆 ∘ 𝐹 ) ∧ ( 𝐺 DProd ( 𝑆 ∘ 𝐹 ) ) ⊆ ( 𝐺 DProd 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 dprdf1.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2 dprdf1.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3 dprdf1.3 ⊢ ( 𝜑 → 𝐹 : 𝐽 –1-1→ 𝐼 )
4 f1f ⊢ ( 𝐹 : 𝐽 –1-1→ 𝐼 → 𝐹 : 𝐽 ⟶ 𝐼 )
5 frn ⊢ ( 𝐹 : 𝐽 ⟶ 𝐼 → ran 𝐹 ⊆ 𝐼 )
6 3 4 5 3syl ⊢ ( 𝜑 → ran 𝐹 ⊆ 𝐼 )
7 1 2 6 dprdres ⊢ ( 𝜑 → ( 𝐺 dom DProd ( 𝑆 ↾ ran 𝐹 ) ∧ ( 𝐺 DProd ( 𝑆 ↾ ran 𝐹 ) ) ⊆ ( 𝐺 DProd 𝑆 ) ) )
8 7 simpld ⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑆 ↾ ran 𝐹 ) )
9 1 2 dprdf2 ⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
10 9 6 fssresd ⊢ ( 𝜑 → ( 𝑆 ↾ ran 𝐹 ) : ran 𝐹 ⟶ ( SubGrp ‘ 𝐺 ) )
11 10 fdmd ⊢ ( 𝜑 → dom ( 𝑆 ↾ ran 𝐹 ) = ran 𝐹 )
12 f1f1orn ⊢ ( 𝐹 : 𝐽 –1-1→ 𝐼 → 𝐹 : 𝐽 –1-1-onto→ ran 𝐹 )
13 3 12 syl ⊢ ( 𝜑 → 𝐹 : 𝐽 –1-1-onto→ ran 𝐹 )
14 8 11 13 dprdf1o ⊢ ( 𝜑 → ( 𝐺 dom DProd ( ( 𝑆 ↾ ran 𝐹 ) ∘ 𝐹 ) ∧ ( 𝐺 DProd ( ( 𝑆 ↾ ran 𝐹 ) ∘ 𝐹 ) ) = ( 𝐺 DProd ( 𝑆 ↾ ran 𝐹 ) ) ) )
15 14 simpld ⊢ ( 𝜑 → 𝐺 dom DProd ( ( 𝑆 ↾ ran 𝐹 ) ∘ 𝐹 ) )
16 ssid ⊢ ran 𝐹 ⊆ ran 𝐹
17 cores ⊢ ( ran 𝐹 ⊆ ran 𝐹 → ( ( 𝑆 ↾ ran 𝐹 ) ∘ 𝐹 ) = ( 𝑆 ∘ 𝐹 ) )
18 16 17 ax-mp ⊢ ( ( 𝑆 ↾ ran 𝐹 ) ∘ 𝐹 ) = ( 𝑆 ∘ 𝐹 )
19 15 18 breqtrdi ⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑆 ∘ 𝐹 ) )
20 18 oveq2i ⊢ ( 𝐺 DProd ( ( 𝑆 ↾ ran 𝐹 ) ∘ 𝐹 ) ) = ( 𝐺 DProd ( 𝑆 ∘ 𝐹 ) )
21 14 simprd ⊢ ( 𝜑 → ( 𝐺 DProd ( ( 𝑆 ↾ ran 𝐹 ) ∘ 𝐹 ) ) = ( 𝐺 DProd ( 𝑆 ↾ ran 𝐹 ) ) )
22 20 21 eqtr3id ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ∘ 𝐹 ) ) = ( 𝐺 DProd ( 𝑆 ↾ ran 𝐹 ) ) )
23 7 simprd ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ ran 𝐹 ) ) ⊆ ( 𝐺 DProd 𝑆 ) )
24 22 23 eqsstrd ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ∘ 𝐹 ) ) ⊆ ( 𝐺 DProd 𝑆 ) )
25 19 24 jca ⊢ ( 𝜑 → ( 𝐺 dom DProd ( 𝑆 ∘ 𝐹 ) ∧ ( 𝐺 DProd ( 𝑆 ∘ 𝐹 ) ) ⊆ ( 𝐺 DProd 𝑆 ) ) )