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 = (g \in GrpOp, h \in GrpOp ⟼ \{f \| (f : ran g ⟶ ran h \land \forall x \in ran g \forall y \in ran g f (x) h f (y) = f (x g y))\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cghomOLD	$class GrpOpHom$
1		vg	$setvar g$
2		cgr	$class GrpOp$
3		vh	$setvar h$
4		vf	$setvar f$
5	4	cv	$setvar f$
6	1	cv	$setvar g$
7	6	crn	$class ran g$
8	3	cv	$setvar h$
9	8	crn	$class ran h$
10	7 9 5	wf	$wff f : ran g ⟶ ran h$
11		vx	$setvar x$
12		vy	$setvar y$
13	11	cv	$setvar x$
14	13 5	cfv	$class f (x)$
15	12	cv	$setvar y$
16	15 5	cfv	$class f (y)$
17	14 16 8	co	$class (f (x) h f (y))$
18	13 15 6	co	$class (x g y)$
19	18 5	cfv	$class f (x g y)$
20	17 19	wceq	$wff f (x) h f (y) = f (x g y)$
21	20 12 7	wral	$wff \forall y \in ran g f (x) h f (y) = f (x g y)$
22	21 11 7	wral	$wff \forall x \in ran g \forall y \in ran g f (x) h f (y) = f (x g y)$
23	10 22	wa	$wff (f : ran g ⟶ ran h \land \forall x \in ran g \forall y \in ran g f (x) h f (y) = f (x g y))$
24	23 4	cab	$class \{f \| (f : ran g ⟶ ran h \land \forall x \in ran g \forall y \in ran g f (x) h f (y) = f (x g y))\}$
25	1 3 2 2 24	cmpo	$class (g \in GrpOp, h \in GrpOp ⟼ \{f \| (f : ran g ⟶ ran h \land \forall x \in ran g \forall y \in ran g f (x) h f (y) = f (x g y))\})$
26	0 25	wceq	$wff GrpOpHom = (g \in GrpOp, h \in GrpOp ⟼ \{f \| (f : ran g ⟶ ran h \land \forall x \in ran g \forall y \in ran g f (x) h f (y) = f (x g y))\})$

Metamath Proof Explorer

Definition df-ghomOLD

Detailed syntax breakdown