Description: The ring of scalars F of a subcomplex module is the restriction of the field of complex numbers to the base set of F . (Contributed by Mario Carneiro, 16-Oct-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | isclm.f | |- F = ( Scalar ` W ) |
|
| isclm.k | |- K = ( Base ` F ) |
||
| Assertion | clmsca | |- ( W e. CMod -> F = ( CCfld |`s K ) ) |
| 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 | simp2bi | |- ( W e. CMod -> F = ( CCfld |`s K ) ) |