Detailed syntax breakdown of Definition df-rgmod
Step | Hyp | Ref
| Expression |
1 | | crglmod 19169 |
. 2
class
ringLMod |
2 | | vw |
. . 3
setvar 𝑤 |
3 | | cvv 3200 |
. . 3
class
V |
4 | 2 | cv 1482 |
. . . . 5
class 𝑤 |
5 | | cbs 15857 |
. . . . 5
class
Base |
6 | 4, 5 | cfv 5888 |
. . . 4
class
(Base‘𝑤) |
7 | | csra 19168 |
. . . . 5
class
subringAlg |
8 | 4, 7 | cfv 5888 |
. . . 4
class
(subringAlg ‘𝑤) |
9 | 6, 8 | cfv 5888 |
. . 3
class
((subringAlg ‘𝑤)‘(Base‘𝑤)) |
10 | 2, 3, 9 | cmpt 4729 |
. 2
class (𝑤 ∈ V ↦ ((subringAlg
‘𝑤)‘(Base‘𝑤))) |
11 | 1, 10 | wceq 1483 |
1
wff ringLMod =
(𝑤 ∈ V ↦
((subringAlg ‘𝑤)‘(Base‘𝑤))) |