Theorem isghm3

Description: Property of a group homomorphism, similar to ismhm . (Contributed by Mario Carneiro, 7-Mar-2015)

	Ref	Expression
Hypotheses	isghm.w	⊢ 𝑋 = ( Base ‘ 𝑆 )
	isghm.x	⊢ 𝑌 = ( Base ‘ 𝑇 )
	isghm.a	⊢ + = ( +g ‘ 𝑆 )
	isghm.b	⊢ ⨣ = ( +g ‘ 𝑇 )
Assertion	isghm3	⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isghm.w	⊢ 𝑋 = ( Base ‘ 𝑆 )
2		isghm.x	⊢ 𝑌 = ( Base ‘ 𝑇 )
3		isghm.a	⊢ + = ( +g ‘ 𝑆 )
4		isghm.b	⊢ ⨣ = ( +g ‘ 𝑇 )
5	1 2 3 4	isghm	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) ) )
6	5	baib	⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) ) )