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 ${⊢}{\ast }_{\mathrm{𝑟𝑓}}=\left({f}\in \mathrm{V}⟼\left({x}\in {\mathrm{Base}}_{{f}}⟼{{x}}^{{*}_{{f}}}\right)\right)$

Detailed syntax breakdown

Step Hyp Ref Expression
0 cstf ${class}{\ast }_{\mathrm{𝑟𝑓}}$
1 vf ${setvar}{f}$
2 cvv ${class}\mathrm{V}$
3 vx ${setvar}{x}$
4 cbs ${class}\mathrm{Base}$
5 1 cv ${setvar}{f}$
6 5 4 cfv ${class}{\mathrm{Base}}_{{f}}$
7 cstv ${class}{\ast }_{𝑟}$
8 5 7 cfv ${class}{*}_{{f}}$
9 3 cv ${setvar}{x}$
10 9 8 cfv ${class}{{x}}^{{*}_{{f}}}$
11 3 6 10 cmpt ${class}\left({x}\in {\mathrm{Base}}_{{f}}⟼{{x}}^{{*}_{{f}}}\right)$
12 1 2 11 cmpt ${class}\left({f}\in \mathrm{V}⟼\left({x}\in {\mathrm{Base}}_{{f}}⟼{{x}}^{{*}_{{f}}}\right)\right)$
13 0 12 wceq ${wff}{\ast }_{\mathrm{𝑟𝑓}}=\left({f}\in \mathrm{V}⟼\left({x}\in {\mathrm{Base}}_{{f}}⟼{{x}}^{{*}_{{f}}}\right)\right)$