Metamath Proof Explorer

Theorem dpjghm

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 dpjghm 
|- ( ph -> ( P ` X ) e. ( ( G |`s ( G DProd S ) ) GrpHom G ) )

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 eqid 
 |-  ( +g ` G ) = ( +g ` G )
6 eqid 
 |-  ( LSSum ` G ) = ( LSSum ` G )
7 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
8 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
9 1 2 dprdf2 
 |-  ( ph -> S : I --> ( SubGrp ` G ) )
10 9 4 ffvelrnd 
 |-  ( ph -> ( S ` X ) e. ( SubGrp ` G ) )
11 difssd 
 |-  ( ph -> ( I \ { X } ) C_ I )
12 1 2 11 dprdres 
 |-  ( ph -> ( G dom DProd ( S |` ( I \ { X } ) ) /\ ( G DProd ( S |` ( I \ { X } ) ) ) C_ ( G DProd S ) ) )
13 12 simpld 
 |-  ( ph -> G dom DProd ( S |` ( I \ { X } ) ) )
14 dprdsubg 
 |-  ( G dom DProd ( S |` ( I \ { X } ) ) -> ( G DProd ( S |` ( I \ { X } ) ) ) e. ( SubGrp ` G ) )
15 13 14 syl 
 |-  ( ph -> ( G DProd ( S |` ( I \ { X } ) ) ) e. ( SubGrp ` G ) )
16 1 2 4 7 dpjdisj 
 |-  ( ph -> ( ( S ` X ) i^i ( G DProd ( S |` ( I \ { X } ) ) ) ) = { ( 0g ` G ) } )
17 1 2 4 8 dpjcntz 
 |-  ( ph -> ( S ` X ) C_ ( ( Cntz ` G ) ` ( G DProd ( S |` ( I \ { X } ) ) ) ) )
18 eqid 
 |-  ( proj1 ` G ) = ( proj1 ` G )
19 5 6 7 8 10 15 16 17 18 pj1ghm 
 |-  ( ph -> ( ( S ` X ) ( proj1 ` G ) ( G DProd ( S |` ( I \ { X } ) ) ) ) e. ( ( G |`s ( ( S ` X ) ( LSSum ` G ) ( G DProd ( S |` ( I \ { X } ) ) ) ) ) GrpHom G ) )
20 1 2 3 18 4 dpjval 
 |-  ( ph -> ( P ` X ) = ( ( S ` X ) ( proj1 ` G ) ( G DProd ( S |` ( I \ { X } ) ) ) ) )
21 1 2 4 6 dpjlsm 
 |-  ( ph -> ( G DProd S ) = ( ( S ` X ) ( LSSum ` G ) ( G DProd ( S |` ( I \ { X } ) ) ) ) )
22 21 oveq2d 
 |-  ( ph -> ( G |`s ( G DProd S ) ) = ( G |`s ( ( S ` X ) ( LSSum ` G ) ( G DProd ( S |` ( I \ { X } ) ) ) ) ) )
23 22 oveq1d 
 |-  ( ph -> ( ( G |`s ( G DProd S ) ) GrpHom G ) = ( ( G |`s ( ( S ` X ) ( LSSum ` G ) ( G DProd ( S |` ( I \ { X } ) ) ) ) ) GrpHom G ) )
24 19 20 23 3eltr4d 
 |-  ( ph -> ( P ` X ) e. ( ( G |`s ( G DProd S ) ) GrpHom G ) )