Theorem ghomf

Description: Mapping property of a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009)

	Ref	Expression
Hypotheses	ghomf.1	⊢ 𝑋 = ran 𝐺
	ghomf.2	⊢ 𝑊 = ran 𝐻
Assertion	ghomf	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → 𝐹 : 𝑋 ⟶ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		ghomf.1	⊢ 𝑋 = ran 𝐺
2		ghomf.2	⊢ 𝑊 = ran 𝐻
3	1 2	elghomOLD	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ) → ( 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑊 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) )
4	3	simprbda	⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ) ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → 𝐹 : 𝑋 ⟶ 𝑊 )
5	4	3impa	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → 𝐹 : 𝑋 ⟶ 𝑊 )