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