Definition df-staf 20114

Description: Define the functionalization of the involution in a star ring. This is not strictly necessary but by having *_𝑟 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 = (𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑓) ↦ ((*𝑟‘𝑓)‘𝑥)))

Distinct variable group:   𝑥,𝑓

Detailed syntax breakdown of Definition df-staf

Step	Hyp	Ref	Expression
1		cstf 20112	. 2 class *rf
2		vf	. . 3 setvar 𝑓
3		cvv 3433	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5	2	cv 1538	. . . . 5 class 𝑓
6		cbs 16921	. . . . 5 class Base
7	5, 6	cfv 6437	. . . 4 class (Base‘𝑓)
8	4	cv 1538	. . . . 5 class 𝑥
9		cstv 16973	. . . . . 6 class *𝑟
10	5, 9	cfv 6437	. . . . 5 class (*𝑟‘𝑓)
11	8, 10	cfv 6437	. . . 4 class ((*𝑟‘𝑓)‘𝑥)
12	4, 7, 11	cmpt 5158	. . 3 class (𝑥 ∈ (Base‘𝑓) ↦ ((*𝑟‘𝑓)‘𝑥))
13	2, 3, 12	cmpt 5158	. 2 class (𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑓) ↦ ((*𝑟‘𝑓)‘𝑥)))
14	1, 13	wceq 1539	1 wff *rf = (𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑓) ↦ ((*𝑟‘𝑓)‘𝑥)))

This definition is referenced by:  staffval  20116