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 ffvelcdmd ⊢ φ → 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