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 ⊢ ∗ 𝑟𝑓 = f ∈ V ⟼ x ∈ Base f ⟼ x * f

Detailed syntax breakdown

Step Hyp Ref Expression
0 cstf class ∗ 𝑟𝑓
1 vf setvar f
2 cvv class V
3 vx setvar x
4 cbs class Base
5 1 cv setvar f
6 5 4 cfv class Base f
7 cstv class ∗ 𝑟
8 5 7 cfv class * f
9 3 cv setvar x
10 9 8 cfv class x * f
11 3 6 10 cmpt class x ∈ Base f ⟼ x * f
12 1 2 11 cmpt class f ∈ V ⟼ x ∈ Base f ⟼ x * f
13 0 12 wceq wff ∗ 𝑟𝑓 = f ∈ V ⟼ x ∈ Base f ⟼ x * f