Definition df-staf

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)

	Ref	Expression
Assertion	df-staf	⊢ *rf = ( 𝑓 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑓 ) ↦ ( ( *𝑟 ‘ 𝑓 ) ‘ 𝑥 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cstf	⊢ *rf
1		vf	⊢ 𝑓
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5	1	cv	⊢ 𝑓
6	5 4	cfv	⊢ ( Base ‘ 𝑓 )
7		cstv	⊢ *𝑟
8	5 7	cfv	⊢ ( *𝑟 ‘ 𝑓 )
9	3	cv	⊢ 𝑥
10	9 8	cfv	⊢ ( ( *𝑟 ‘ 𝑓 ) ‘ 𝑥 )
11	3 6 10	cmpt	⊢ ( 𝑥 ∈ ( Base ‘ 𝑓 ) ↦ ( ( *𝑟 ‘ 𝑓 ) ‘ 𝑥 ) )
12	1 2 11	cmpt	⊢ ( 𝑓 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑓 ) ↦ ( ( *𝑟 ‘ 𝑓 ) ‘ 𝑥 ) ) )
13	0 12	wceq	⊢ *rf = ( 𝑓 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑓 ) ↦ ( ( *𝑟 ‘ 𝑓 ) ‘ 𝑥 ) ) )