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

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 1 2 3 4 dpjghm φ P X G 𝑠 G DProd S GrpHom G
6 1 2 dprdf2 φ S : I SubGrp G
7 6 4 ffvelrnd φ S X SubGrp G
8 1 2 3 4 dpjf φ P X : G DProd S S X
9 8 frnd φ ran P X S X
10 eqid G 𝑠 S X = G 𝑠 S X
11 10 resghm2b S X SubGrp G ran P X S X P X G 𝑠 G DProd S GrpHom G P X G 𝑠 G DProd S GrpHom G 𝑠 S X
12 7 9 11 syl2anc φ P X G 𝑠 G DProd S GrpHom G P X G 𝑠 G DProd S GrpHom G 𝑠 S X
13 5 12 mpbid φ P X G 𝑠 G DProd S GrpHom G 𝑠 S X