MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-staf Structured version   Visualization version   GIF version

Definition df-staf 18614
Description: Define the functionalization of the involution in a star ring. This is not strictly necessary but by having *𝑟 as an actual function we can state the principal properties of an involution much more cleanly. (Contributed by Mario Carneiro, 6-Oct-2015.)
Assertion
Ref Expression
df-staf *rf = (𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑓) ↦ ((*𝑟𝑓)‘𝑥)))
Distinct variable group:   𝑥,𝑓

Detailed syntax breakdown of Definition df-staf
StepHypRef Expression
1 cstf 18612 . 2 class *rf
2 vf . . 3 setvar 𝑓
3 cvv 3172 . . 3 class V
4 vx . . . 4 setvar 𝑥
52cv 1473 . . . . 5 class 𝑓
6 cbs 15641 . . . . 5 class Base
75, 6cfv 5790 . . . 4 class (Base‘𝑓)
84cv 1473 . . . . 5 class 𝑥
9 cstv 15716 . . . . . 6 class *𝑟
105, 9cfv 5790 . . . . 5 class (*𝑟𝑓)
118, 10cfv 5790 . . . 4 class ((*𝑟𝑓)‘𝑥)
124, 7, 11cmpt 4637 . . 3 class (𝑥 ∈ (Base‘𝑓) ↦ ((*𝑟𝑓)‘𝑥))
132, 3, 12cmpt 4637 . 2 class (𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑓) ↦ ((*𝑟𝑓)‘𝑥)))
141, 13wceq 1474 1 wff *rf = (𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑓) ↦ ((*𝑟𝑓)‘𝑥)))
Colors of variables: wff setvar class
This definition is referenced by:  staffval  18616
  Copyright terms: Public domain W3C validator