Definition df-staf 18845

Description: Define the functionalization of the involution in a star ring. This is not strictly necessary but by having *r as an actual function we can state the principal properties of an involution much more cleanly. (Contributed by Mario Carneiro, 6-Oct-2015.)

Assertion

Ref	Expression
df-staf	|- *rf = ( f e. _V |-> ( x e. ( Base ` f ) |-> ( ( *r ` f ) ` x ) ) )

Distinct variable group:   x, f

Detailed syntax breakdown of Definition df-staf

Step	Hyp	Ref	Expression
1		cstf 18843	. 2 class *rf
2		vf	. . 3 setvar f
3		cvv 3200	. . 3 class _V
4		vx	. . . 4 setvar x
5	2	cv 1482	. . . . 5 class f
6		cbs 15857	. . . . 5 class Base
7	5, 6	cfv 5888	. . . 4 class ( Base ` f )
8	4	cv 1482	. . . . 5 class x
9		cstv 15943	. . . . . 6 class *r
10	5, 9	cfv 5888	. . . . 5 class ( *r ` f )
11	8, 10	cfv 5888	. . . 4 class ( ( *r ` f ) ` x )
12	4, 7, 11	cmpt 4729	. . 3 class ( x e. ( Base ` f ) |-> ( ( *r ` f ) ` x ) )
13	2, 3, 12	cmpt 4729	. 2 class ( f e. _V |-> ( x e. ( Base ` f ) |-> ( ( *r ` f ) ` x ) ) )
14	1, 13	wceq 1483	1 wff *rf = ( f e. _V |-> ( x e. ( Base ` f ) |-> ( ( *r ` f ) ` x ) ) )

This definition is referenced by:  staffval  18847