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 = ( f e. _V |-> ( x e. ( Base ` f ) |-> ( ( *r ` f ) ` x ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cstf | |- *rf |
|
| 1 | vf | |- f |
|
| 2 | cvv | |- _V |
|
| 3 | vx | |- x |
|
| 4 | cbs | |- Base |
|
| 5 | 1 | cv | |- f |
| 6 | 5 4 | cfv | |- ( Base ` f ) |
| 7 | cstv | |- *r |
|
| 8 | 5 7 | cfv | |- ( *r ` f ) |
| 9 | 3 | cv | |- x |
| 10 | 9 8 | cfv | |- ( ( *r ` f ) ` x ) |
| 11 | 3 6 10 | cmpt | |- ( x e. ( Base ` f ) |-> ( ( *r ` f ) ` x ) ) |
| 12 | 1 2 11 | cmpt | |- ( f e. _V |-> ( x e. ( Base ` f ) |-> ( ( *r ` f ) ` x ) ) ) |
| 13 | 0 12 | wceq | |- *rf = ( f e. _V |-> ( x e. ( Base ` f ) |-> ( ( *r ` f ) ` x ) ) ) |