This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dpjghm2

Description: The direct product is the binary subgroup product ("sum") of the direct products of the partition. (Contributed by Mario Carneiro, 26-Apr-2016)

Ref Expression
Hypotheses dpjfval.1 ⊢ φ → G dom ⁡ DProd S
dpjfval.2 ⊢ φ → dom ⁡ S = I
dpjfval.p ⊢ P = G dProj S
dpjlid.3 ⊢ φ → X ∈ I
Assertion dpjghm2 ⊢ φ → P ⁡ X ∈ G ↾ 𝑠 G DProd S GrpHom G ↾ 𝑠 S ⁡ X

Proof

Step Hyp Ref Expression
1 dpjfval.1 ⊢ φ → G dom ⁡ DProd S
2 dpjfval.2 ⊢ φ → dom ⁡ S = I
3 dpjfval.p ⊢ P = G dProj S
4 dpjlid.3 ⊢ φ → X ∈ I
5 1 2 3 4 dpjghm ⊢ φ → P ⁡ X ∈ G ↾ 𝑠 G DProd S GrpHom G
6 1 2 dprdf2 ⊢ φ → S : I ⟶ SubGrp ⁡ G
7 6 4 ffvelcdmd ⊢ φ → S ⁡ X ∈ SubGrp ⁡ G
8 1 2 3 4 dpjf ⊢ φ → P ⁡ X : G DProd S ⟶ S ⁡ X
9 8 frnd ⊢ φ → ran ⁡ P ⁡ X ⊆ S ⁡ X
10 eqid ⊢ G ↾ 𝑠 S ⁡ X = G ↾ 𝑠 S ⁡ X
11 10 resghm2b ⊢ S ⁡ X ∈ SubGrp ⁡ G ∧ ran ⁡ P ⁡ X ⊆ S ⁡ X → P ⁡ X ∈ G ↾ 𝑠 G DProd S GrpHom G ↔ P ⁡ X ∈ G ↾ 𝑠 G DProd S GrpHom G ↾ 𝑠 S ⁡ X
12 7 9 11 syl2anc ⊢ φ → P ⁡ X ∈ G ↾ 𝑠 G DProd S GrpHom G ↔ P ⁡ X ∈ G ↾ 𝑠 G DProd S GrpHom G ↾ 𝑠 S ⁡ X
13 5 12 mpbid ⊢ φ → P ⁡ X ∈ G ↾ 𝑠 G DProd S GrpHom G ↾ 𝑠 S ⁡ X