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 
|- ( 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 ffvelcdmd 
 |-  ( 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 ) ) ) )