This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 dpjfval.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2 dpjfval.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3 dpjfval.p ⊢ 𝑃 = ( 𝐺 dProj 𝑆 )
4 dpjlid.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
5 1 2 3 4 dpjghm ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑋 ) ∈ ( ( 𝐺 ↾s ( 𝐺 DProd 𝑆 ) ) GrpHom 𝐺 ) )
6 1 2 dprdf2 ⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
7 6 4 ffvelcdmd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ∈ ( SubGrp ‘ 𝐺 ) )
8 1 2 3 4 dpjf ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑋 ) : ( 𝐺 DProd 𝑆 ) ⟶ ( 𝑆 ‘ 𝑋 ) )
9 8 frnd ⊢ ( 𝜑 → ran ( 𝑃 ‘ 𝑋 ) ⊆ ( 𝑆 ‘ 𝑋 ) )
10 eqid ⊢ ( 𝐺 ↾s ( 𝑆 ‘ 𝑋 ) ) = ( 𝐺 ↾s ( 𝑆 ‘ 𝑋 ) )
11 10 resghm2b ⊢ ( ( ( 𝑆 ‘ 𝑋 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ran ( 𝑃 ‘ 𝑋 ) ⊆ ( 𝑆 ‘ 𝑋 ) ) → ( ( 𝑃 ‘ 𝑋 ) ∈ ( ( 𝐺 ↾s ( 𝐺 DProd 𝑆 ) ) GrpHom 𝐺 ) ↔ ( 𝑃 ‘ 𝑋 ) ∈ ( ( 𝐺 ↾s ( 𝐺 DProd 𝑆 ) ) GrpHom ( 𝐺 ↾s ( 𝑆 ‘ 𝑋 ) ) ) ) )
12 7 9 11 syl2anc ⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝑋 ) ∈ ( ( 𝐺 ↾s ( 𝐺 DProd 𝑆 ) ) GrpHom 𝐺 ) ↔ ( 𝑃 ‘ 𝑋 ) ∈ ( ( 𝐺 ↾s ( 𝐺 DProd 𝑆 ) ) GrpHom ( 𝐺 ↾s ( 𝑆 ‘ 𝑋 ) ) ) ) )
13 5 12 mpbid ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑋 ) ∈ ( ( 𝐺 ↾s ( 𝐺 DProd 𝑆 ) ) GrpHom ( 𝐺 ↾s ( 𝑆 ‘ 𝑋 ) ) ) )