This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cphclm

Description: A subcomplex pre-Hilbert space is a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Assertion cphclm ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod )

Proof

Step Hyp Ref Expression
1 cphlmod ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod )
2 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
3 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
4 2 3 cphsca ⊢ ( 𝑊 ∈ ℂPreHil → ( Scalar ‘ 𝑊 ) = ( ℂfld ↾s ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
5 2 3 cphsubrg ⊢ ( 𝑊 ∈ ℂPreHil → ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( SubRing ‘ ℂfld ) )
6 2 3 isclm ⊢ ( 𝑊 ∈ ℂMod ↔ ( 𝑊 ∈ LMod ∧ ( Scalar ‘ 𝑊 ) = ( ℂfld ↾s ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( SubRing ‘ ℂfld ) ) )
7 1 4 5 6 syl3anbrc ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod )