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	|- ( ph -> G dom DProd S )
	dpjfval.2	|- ( ph -> dom S = I )
	dpjfval.p	|- P = ( G dProj S )
	dpjlid.3	|- ( ph -> X e. I )
Assertion	dpjghm2	|- ( ph -> ( P ` X ) e. ( ( G |`s ( G DProd S ) ) GrpHom ( G |`s ( S ` X ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dpjfval.1	|- ( ph -> G dom DProd S )
2		dpjfval.2	|- ( ph -> dom S = I )
3		dpjfval.p	|- P = ( G dProj S )
4		dpjlid.3	|- ( ph -> X e. I )
5	1 2 3 4	dpjghm	|- ( ph -> ( P ` X ) e. ( ( G |`s ( G DProd S ) ) GrpHom G ) )
6	1 2	dprdf2	|- ( ph -> S : I --> ( SubGrp ` G ) )
7	6 4	ffvelrnd	|- ( ph -> ( S ` X ) e. ( SubGrp ` G ) )
8	1 2 3 4	dpjf	|- ( ph -> ( P ` X ) : ( G DProd S ) --> ( S ` X ) )
9	8	frnd	|- ( ph -> ran ( P ` X ) C_ ( S ` X ) )
10		eqid	|- ( G |`s ( S ` X ) ) = ( G |`s ( S ` X ) )
11	10	resghm2b	|- ( ( ( S ` X ) e. ( SubGrp ` G ) /\ ran ( P ` X ) C_ ( S ` X ) ) -> ( ( P ` X ) e. ( ( G |`s ( G DProd S ) ) GrpHom G ) <-> ( P ` X ) e. ( ( G |`s ( G DProd S ) ) GrpHom ( G |`s ( S ` X ) ) ) ) )
12	7 9 11	syl2anc	|- ( ph -> ( ( P ` X ) e. ( ( G |`s ( G DProd S ) ) GrpHom G ) <-> ( P ` X ) e. ( ( G |`s ( G DProd S ) ) GrpHom ( G |`s ( S ` X ) ) ) ) )
13	5 12	mpbid	|- ( ph -> ( P ` X ) e. ( ( G |`s ( G DProd S ) ) GrpHom ( G |`s ( S ` X ) ) ) )