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 clmsubrg
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 ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
isclm.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion
clmsubrg ⊢ ( 𝑊 ∈ ℂMod → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
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
simp3bi ⊢ ( 𝑊 ∈ ℂMod → 𝐾 ∈ ( SubRing ‘ ℂfld ) )