Detailed syntax breakdown of Definition df-clm
| Step | Hyp | Ref
| Expression |
| 1 | | cclm 25095 |
. 2
class
ℂMod |
| 2 | | vf |
. . . . . . . 8
setvar 𝑓 |
| 3 | 2 | cv 1539 |
. . . . . . 7
class 𝑓 |
| 4 | | ccnfld 21364 |
. . . . . . . 8
class
ℂfld |
| 5 | | vk |
. . . . . . . . 9
setvar 𝑘 |
| 6 | 5 | cv 1539 |
. . . . . . . 8
class 𝑘 |
| 7 | | cress 17274 |
. . . . . . . 8
class
↾s |
| 8 | 4, 6, 7 | co 7431 |
. . . . . . 7
class
(ℂfld ↾s 𝑘) |
| 9 | 3, 8 | wceq 1540 |
. . . . . 6
wff 𝑓 = (ℂfld
↾s 𝑘) |
| 10 | | csubrg 20569 |
. . . . . . . 8
class
SubRing |
| 11 | 4, 10 | cfv 6561 |
. . . . . . 7
class
(SubRing‘ℂfld) |
| 12 | 6, 11 | wcel 2108 |
. . . . . 6
wff 𝑘 ∈
(SubRing‘ℂfld) |
| 13 | 9, 12 | wa 395 |
. . . . 5
wff (𝑓 = (ℂfld
↾s 𝑘)
∧ 𝑘 ∈
(SubRing‘ℂfld)) |
| 14 | | cbs 17247 |
. . . . . 6
class
Base |
| 15 | 3, 14 | cfv 6561 |
. . . . 5
class
(Base‘𝑓) |
| 16 | 13, 5, 15 | wsbc 3788 |
. . . 4
wff
[(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s
𝑘) ∧ 𝑘 ∈
(SubRing‘ℂfld)) |
| 17 | | vw |
. . . . . 6
setvar 𝑤 |
| 18 | 17 | cv 1539 |
. . . . 5
class 𝑤 |
| 19 | | csca 17300 |
. . . . 5
class
Scalar |
| 20 | 18, 19 | cfv 6561 |
. . . 4
class
(Scalar‘𝑤) |
| 21 | 16, 2, 20 | wsbc 3788 |
. . 3
wff
[(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s
𝑘) ∧ 𝑘 ∈
(SubRing‘ℂfld)) |
| 22 | | clmod 20858 |
. . 3
class
LMod |
| 23 | 21, 17, 22 | crab 3436 |
. 2
class {𝑤 ∈ LMod ∣
[(Scalar‘𝑤) /
𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s
𝑘) ∧ 𝑘 ∈
(SubRing‘ℂfld))} |
| 24 | 1, 23 | wceq 1540 |
1
wff ℂMod
= {𝑤 ∈ LMod ∣
[(Scalar‘𝑤) /
𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s
𝑘) ∧ 𝑘 ∈
(SubRing‘ℂfld))} |