Definition df-ghomOLD

Description: Obsolete version of df-ghm as of 15-Mar-2020. Define the set of group homomorphisms from g to h . (Contributed by Paul Chapman, 25-Feb-2008) (New usage is discouraged.)

	Ref	Expression
Assertion	df-ghomOLD	⊢ GrpOpHom = ( 𝑔 ∈ GrpOp , ℎ ∈ GrpOp ↦ { 𝑓 ∣ ( 𝑓 : ran 𝑔 ⟶ ran ℎ ∧ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cghomOLD	⊢ GrpOpHom
1		vg	⊢ 𝑔
2		cgr	⊢ GrpOp
3		vh	⊢ ℎ
4		vf	⊢ 𝑓
5	4	cv	⊢ 𝑓
6	1	cv	⊢ 𝑔
7	6	crn	⊢ ran 𝑔
8	3	cv	⊢ ℎ
9	8	crn	⊢ ran ℎ
10	7 9 5	wf	⊢ 𝑓 : ran 𝑔 ⟶ ran ℎ
11		vx	⊢ 𝑥
12		vy	⊢ 𝑦
13	11	cv	⊢ 𝑥
14	13 5	cfv	⊢ ( 𝑓 ‘ 𝑥 )
15	12	cv	⊢ 𝑦
16	15 5	cfv	⊢ ( 𝑓 ‘ 𝑦 )
17	14 16 8	co	⊢ ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) )
18	13 15 6	co	⊢ ( 𝑥 𝑔 𝑦 )
19	18 5	cfv	⊢ ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) )
20	17 19	wceq	⊢ ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) )
21	20 12 7	wral	⊢ ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) )
22	21 11 7	wral	⊢ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) )
23	10 22	wa	⊢ ( 𝑓 : ran 𝑔 ⟶ ran ℎ ∧ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) ) )
24	23 4	cab	⊢ { 𝑓 ∣ ( 𝑓 : ran 𝑔 ⟶ ran ℎ ∧ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) ) ) }
25	1 3 2 2 24	cmpo	⊢ ( 𝑔 ∈ GrpOp , ℎ ∈ GrpOp ↦ { 𝑓 ∣ ( 𝑓 : ran 𝑔 ⟶ ran ℎ ∧ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) ) ) } )
26	0 25	wceq	⊢ GrpOpHom = ( 𝑔 ∈ GrpOp , ℎ ∈ GrpOp ↦ { 𝑓 ∣ ( 𝑓 : ran 𝑔 ⟶ ran ℎ ∧ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) ) ) } )