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 𝐺 ) )