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

Definition df-staf 18668
 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 18666 . 2 class *rf
2 vf . . 3 setvar 𝑓
3 cvv 3173 . . 3 class V
4 vx . . . 4 setvar 𝑥
52cv 1474 . . . . 5 class 𝑓
6 cbs 15695 . . . . 5 class Base
75, 6cfv 5804 . . . 4 class (Base‘𝑓)
84cv 1474 . . . . 5 class 𝑥
9 cstv 15770 . . . . . 6 class *𝑟
105, 9cfv 5804 . . . . 5 class (*𝑟𝑓)
118, 10cfv 5804 . . . 4 class ((*𝑟𝑓)‘𝑥)
124, 7, 11cmpt 4643 . . 3 class (𝑥 ∈ (Base‘𝑓) ↦ ((*𝑟𝑓)‘𝑥))
132, 3, 12cmpt 4643 . 2 class (𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑓) ↦ ((*𝑟𝑓)‘𝑥)))
141, 13wceq 1475 1 wff *rf = (𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑓) ↦ ((*𝑟𝑓)‘𝑥)))
 Colors of variables: wff setvar class This definition is referenced by:  staffval  18670
 Copyright terms: Public domain W3C validator