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 φ G dom DProd S
dpjfval.2 φ dom S = I
dpjfval.p P = G dProj S
dpjlid.3 φ X I
Assertion dpjghm φ P X G 𝑠 G DProd S GrpHom G

Proof

Step Hyp Ref Expression
1 dpjfval.1 φ G dom DProd S
2 dpjfval.2 φ dom S = I
3 dpjfval.p P = G dProj S
4 dpjlid.3 φ X I
5 eqid + G = + G
6 eqid LSSum G = LSSum G
7 eqid 0 G = 0 G
8 eqid Cntz G = Cntz G
9 1 2 dprdf2 φ S : I SubGrp G
10 9 4 ffvelrnd φ S X SubGrp G
11 difssd φ I X I
12 1 2 11 dprdres φ G dom DProd S I X G DProd S I X G DProd S
13 12 simpld φ G dom DProd S I X
14 dprdsubg G dom DProd S I X G DProd S I X SubGrp G
15 13 14 syl φ G DProd S I X SubGrp G
16 1 2 4 7 dpjdisj φ S X G DProd S I X = 0 G
17 1 2 4 8 dpjcntz φ S X Cntz G G DProd S I X
18 eqid proj 1 G = proj 1 G
19 5 6 7 8 10 15 16 17 18 pj1ghm φ S X proj 1 G G DProd S I X G 𝑠 S X LSSum G G DProd S I X GrpHom G
20 1 2 3 18 4 dpjval φ P X = S X proj 1 G G DProd S I X
21 1 2 4 6 dpjlsm φ G DProd S = S X LSSum G G DProd S I X
22 21 oveq2d φ G 𝑠 G DProd S = G 𝑠 S X LSSum G G DProd S I X
23 22 oveq1d φ G 𝑠 G DProd S GrpHom G = G 𝑠 S X LSSum G G DProd S I X GrpHom G
24 19 20 23 3eltr4d φ P X G 𝑠 G DProd S GrpHom G