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	$⊢ φ \to G dom DProd S$
		dpjfval.2	$⊢ φ \to dom S = I$
		dpjfval.p	$⊢ P = G dProj S$
		dpjlid.3	$⊢ φ \to X \in I$
	Assertion	dpjghm2	$⊢ φ \to P (X) \in ((G ↾_{𝑠} (G DProd S)) GrpHom (G ↾_{𝑠} S (X)))$

Proof

Step	Hyp	Ref	Expression
1		dpjfval.1	$⊢ φ \to G dom DProd S$
2		dpjfval.2	$⊢ φ \to dom S = I$
3		dpjfval.p	$⊢ P = G dProj S$
4		dpjlid.3	$⊢ φ \to X \in I$
5	1 2 3 4	dpjghm	$⊢ φ \to P (X) \in ((G ↾_{𝑠} (G DProd S)) GrpHom G)$
6	1 2	dprdf2	$⊢ φ \to S : I ⟶ SubGrp (G)$
7	6 4	ffvelcdmd	$⊢ φ \to S (X) \in SubGrp (G)$
8	1 2 3 4	dpjf	$⊢ φ \to P (X) : G DProd S ⟶ S (X)$
9	8	frnd	$⊢ φ \to ran P (X) \subseteq S (X)$
10		eqid	$⊢ G ↾_{𝑠} S (X) = G ↾_{𝑠} S (X)$
11	10	resghm2b	$⊢ (S (X) \in SubGrp (G) \land ran P (X) \subseteq S (X)) \to (P (X) \in ((G ↾_{𝑠} (G DProd S)) GrpHom G) \leftrightarrow P (X) \in ((G ↾_{𝑠} (G DProd S)) GrpHom (G ↾_{𝑠} S (X))))$
12	7 9 11	syl2anc	$⊢ φ \to (P (X) \in ((G ↾_{𝑠} (G DProd S)) GrpHom G) \leftrightarrow P (X) \in ((G ↾_{𝑠} (G DProd S)) GrpHom (G ↾_{𝑠} S (X))))$
13	5 12	mpbid	$⊢ φ \to P (X) \in ((G ↾_{𝑠} (G DProd S)) GrpHom (G ↾_{𝑠} S (X)))$