This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑓 ) ↦ ( ( *𝑟 ‘ 𝑓 ) ‘ 𝑥 ) ) )