Theorem pj1ghm2

Description: The left projection function is a group homomorphism. (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	pj1eu.a	⊢ + = ( +g ‘ 𝐺 )
	pj1eu.s	⊢ ⊕ = ( LSSum ‘ 𝐺 )
	pj1eu.o	⊢ 0 = ( 0g ‘ 𝐺 )
	pj1eu.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
	pj1eu.2	⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
	pj1eu.3	⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
	pj1eu.4	⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) = { 0 } )
	pj1eu.5	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )
	pj1f.p	⊢ 𝑃 = ( proj1 ‘ 𝐺 )
Assertion	pj1ghm2	⊢ ( 𝜑 → ( 𝑇 𝑃 𝑈 ) ∈ ( ( 𝐺 ↾s ( 𝑇 ⊕ 𝑈 ) ) GrpHom ( 𝐺 ↾s 𝑇 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pj1eu.a	⊢ + = ( +g ‘ 𝐺 )
2		pj1eu.s	⊢ ⊕ = ( LSSum ‘ 𝐺 )
3		pj1eu.o	⊢ 0 = ( 0g ‘ 𝐺 )
4		pj1eu.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
5		pj1eu.2	⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
6		pj1eu.3	⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
7		pj1eu.4	⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) = { 0 } )
8		pj1eu.5	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )
9		pj1f.p	⊢ 𝑃 = ( proj1 ‘ 𝐺 )
10	1 2 3 4 5 6 7 8 9	pj1ghm	⊢ ( 𝜑 → ( 𝑇 𝑃 𝑈 ) ∈ ( ( 𝐺 ↾s ( 𝑇 ⊕ 𝑈 ) ) GrpHom 𝐺 ) )
11	1 2 3 4 5 6 7 8 9	pj1f	⊢ ( 𝜑 → ( 𝑇 𝑃 𝑈 ) : ( 𝑇 ⊕ 𝑈 ) ⟶ 𝑇 )
12	11	frnd	⊢ ( 𝜑 → ran ( 𝑇 𝑃 𝑈 ) ⊆ 𝑇 )
13		eqid	⊢ ( 𝐺 ↾s 𝑇 ) = ( 𝐺 ↾s 𝑇 )
14	13	resghm2b	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ ran ( 𝑇 𝑃 𝑈 ) ⊆ 𝑇 ) → ( ( 𝑇 𝑃 𝑈 ) ∈ ( ( 𝐺 ↾s ( 𝑇 ⊕ 𝑈 ) ) GrpHom 𝐺 ) ↔ ( 𝑇 𝑃 𝑈 ) ∈ ( ( 𝐺 ↾s ( 𝑇 ⊕ 𝑈 ) ) GrpHom ( 𝐺 ↾s 𝑇 ) ) ) )
15	5 12 14	syl2anc	⊢ ( 𝜑 → ( ( 𝑇 𝑃 𝑈 ) ∈ ( ( 𝐺 ↾s ( 𝑇 ⊕ 𝑈 ) ) GrpHom 𝐺 ) ↔ ( 𝑇 𝑃 𝑈 ) ∈ ( ( 𝐺 ↾s ( 𝑇 ⊕ 𝑈 ) ) GrpHom ( 𝐺 ↾s 𝑇 ) ) ) )
16	10 15	mpbid	⊢ ( 𝜑 → ( 𝑇 𝑃 𝑈 ) ∈ ( ( 𝐺 ↾s ( 𝑇 ⊕ 𝑈 ) ) GrpHom ( 𝐺 ↾s 𝑇 ) ) )