Detailed syntax breakdown of Definition df-rgmod
Step | Hyp | Ref
| Expression |
1 | | crglmod 18990 |
. 2
class
ringLMod |
2 | | vw |
. . 3
setvar 𝑤 |
3 | | cvv 3173 |
. . 3
class
V |
4 | 2 | cv 1474 |
. . . . 5
class 𝑤 |
5 | | cbs 15695 |
. . . . 5
class
Base |
6 | 4, 5 | cfv 5804 |
. . . 4
class
(Base‘𝑤) |
7 | | csra 18989 |
. . . . 5
class
subringAlg |
8 | 4, 7 | cfv 5804 |
. . . 4
class
(subringAlg ‘𝑤) |
9 | 6, 8 | cfv 5804 |
. . 3
class
((subringAlg ‘𝑤)‘(Base‘𝑤)) |
10 | 2, 3, 9 | cmpt 4643 |
. 2
class (𝑤 ∈ V ↦ ((subringAlg
‘𝑤)‘(Base‘𝑤))) |
11 | 1, 10 | wceq 1475 |
1
wff ringLMod =
(𝑤 ∈ V ↦
((subringAlg ‘𝑤)‘(Base‘𝑤))) |