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 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
dpjfval.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
dpjfval.p ⊢ 𝑃 = ( 𝐺 dProj 𝑆 )
dpjlid.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
Assertion dpjghm ( 𝜑 → ( 𝑃 ‘ 𝑋 ) ∈ ( ( 𝐺 ↾s ( 𝐺 DProd 𝑆 ) ) GrpHom 𝐺 ) )

Proof

Step Hyp Ref Expression
1 dpjfval.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2 dpjfval.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3 dpjfval.p ⊢ 𝑃 = ( 𝐺 dProj 𝑆 )
4 dpjlid.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
5 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
6 eqid ⊢ ( LSSum ‘ 𝐺 ) = ( LSSum ‘ 𝐺 )
7 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
8 eqid ⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
9 1 2 dprdf2 ⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
10 9 4 ffvelrnd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ∈ ( SubGrp ‘ 𝐺 ) )
11 difssd ⊢ ( 𝜑 → ( 𝐼 ∖ { 𝑋 } ) ⊆ 𝐼 )
12 1 2 11 dprdres ⊢ ( 𝜑 → ( 𝐺 dom DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ⊆ ( 𝐺 DProd 𝑆 ) ) )
13 12 simpld ⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) )
14 dprdsubg ⊢ ( 𝐺 dom DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) → ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
15 13 14 syl ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
16 1 2 4 7 dpjdisj ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) ∩ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } )
17 1 2 4 8 dpjcntz ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) )
18 eqid ⊢ ( proj1 ‘ 𝐺 ) = ( proj1 ‘ 𝐺 )
19 5 6 7 8 10 15 16 17 18 pj1ghm ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) ( proj1 ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ∈ ( ( 𝐺 ↾s ( ( 𝑆 ‘ 𝑋 ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ) GrpHom 𝐺 ) )
20 1 2 3 18 4 dpjval ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑋 ) = ( ( 𝑆 ‘ 𝑋 ) ( proj1 ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) )
21 1 2 4 6 dpjlsm ⊢ ( 𝜑 → ( 𝐺 DProd 𝑆 ) = ( ( 𝑆 ‘ 𝑋 ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) )
22 21 oveq2d ⊢ ( 𝜑 → ( 𝐺 ↾s ( 𝐺 DProd 𝑆 ) ) = ( 𝐺 ↾s ( ( 𝑆 ‘ 𝑋 ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ) )
23 22 oveq1d ⊢ ( 𝜑 → ( ( 𝐺 ↾s ( 𝐺 DProd 𝑆 ) ) GrpHom 𝐺 ) = ( ( 𝐺 ↾s ( ( 𝑆 ‘ 𝑋 ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ) GrpHom 𝐺 ) )
24 19 20 23 3eltr4d ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑋 ) ∈ ( ( 𝐺 ↾s ( 𝐺 DProd 𝑆 ) ) GrpHom 𝐺 ) )