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 ( 𝑆 ‘ 𝑋 ) ) ) )