Detailed syntax breakdown of Definition df-invr
| Step | Hyp | Ref
| Expression |
| 1 | | cinvr 20387 |
. 2
class
invr |
| 2 | | vr |
. . 3
setvar 𝑟 |
| 3 | | cvv 3480 |
. . 3
class
V |
| 4 | 2 | cv 1539 |
. . . . . 6
class 𝑟 |
| 5 | | cmgp 20137 |
. . . . . 6
class
mulGrp |
| 6 | 4, 5 | cfv 6561 |
. . . . 5
class
(mulGrp‘𝑟) |
| 7 | | cui 20355 |
. . . . . 6
class
Unit |
| 8 | 4, 7 | cfv 6561 |
. . . . 5
class
(Unit‘𝑟) |
| 9 | | cress 17274 |
. . . . 5
class
↾s |
| 10 | 6, 8, 9 | co 7431 |
. . . 4
class
((mulGrp‘𝑟)
↾s (Unit‘𝑟)) |
| 11 | | cminusg 18952 |
. . . 4
class
invg |
| 12 | 10, 11 | cfv 6561 |
. . 3
class
(invg‘((mulGrp‘𝑟) ↾s (Unit‘𝑟))) |
| 13 | 2, 3, 12 | cmpt 5225 |
. 2
class (𝑟 ∈ V ↦
(invg‘((mulGrp‘𝑟) ↾s (Unit‘𝑟)))) |
| 14 | 1, 13 | wceq 1540 |
1
wff
invr = (𝑟
∈ V ↦ (invg‘((mulGrp‘𝑟) ↾s (Unit‘𝑟)))) |