This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC TOPOLOGY Metric subcomplex vector spaces Subcomplex modules clmsca
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 ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
isclm.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion
clmsca ⊢ ( 𝑊 ∈ ℂMod → 𝐹 = ( ℂfld ↾s 𝐾 ) )
Proof
Step
Hyp
Ref
Expression
1
isclm.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2
isclm.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
3
1 2
isclm ⊢ ( 𝑊 ∈ ℂMod ↔ ( 𝑊 ∈ LMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) )
4
3
simp2bi ⊢ ( 𝑊 ∈ ℂMod → 𝐹 = ( ℂfld ↾s 𝐾 ) )