Theorem elghomOLD

Description: Obsolete version of isghm as of 15-Mar-2020. Membership in the set of group homomorphisms from G to H . (Contributed by Paul Chapman, 3-Mar-2008) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	elghomOLD.1	⊢ 𝑋 = ran 𝐺
	elghomOLD.2	⊢ 𝑊 = ran 𝐻
Assertion	elghomOLD	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ) → ( 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑊 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elghomOLD.1	⊢ 𝑋 = ran 𝐺
2		elghomOLD.2	⊢ 𝑊 = ran 𝐻
3		eqid	⊢ { 𝑓 ∣ ( 𝑓 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑓 ‘ 𝑥 ) 𝐻 ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) ) } = { 𝑓 ∣ ( 𝑓 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑓 ‘ 𝑥 ) 𝐻 ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) ) }
4	3	elghomlem2OLD	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ) → ( 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ↔ ( 𝐹 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) )
5	1 2	feq23i	⊢ ( 𝐹 : 𝑋 ⟶ 𝑊 ↔ 𝐹 : ran 𝐺 ⟶ ran 𝐻 )
6	1	raleqi	⊢ ( ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ↔ ∀ 𝑦 ∈ ran 𝐺 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) )
7	1 6	raleqbii	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ↔ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) )
8	5 7	anbi12i	⊢ ( ( 𝐹 : 𝑋 ⟶ 𝑊 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ↔ ( 𝐹 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
9	4 8	bitr4di	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ) → ( 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑊 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) )