Description: The base set of the ring of scalars of a subcomplex module is the base set of a subring of the field of complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | isclm.f | |- F = ( Scalar ` W ) |
|
| isclm.k | |- K = ( Base ` F ) |
||
| Assertion | clmsubrg | |- ( W e. CMod -> K e. ( SubRing ` CCfld ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | isclm.f | |- F = ( Scalar ` W ) |
|
| 2 | isclm.k | |- K = ( Base ` F ) |
|
| 3 | 1 2 | isclm | |- ( W e. CMod <-> ( W e. LMod /\ F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) |
| 4 | 3 | simp3bi | |- ( W e. CMod -> K e. ( SubRing ` CCfld ) ) |