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 ⊢ W ∈ CPreHil → W ∈ CMod

Proof

Step Hyp Ref Expression
1 cphlmod ⊢ W ∈ CPreHil → W ∈ LMod
2 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
3 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
4 2 3 cphsca ⊢ W ∈ CPreHil → Scalar ⁡ W = ℂ fld ↾ 𝑠 Base Scalar ⁡ W
5 2 3 cphsubrg ⊢ W ∈ CPreHil → Base Scalar ⁡ W ∈ SubRing ⁡ ℂ fld
6 2 3 isclm ⊢ W ∈ CMod ↔ W ∈ LMod ∧ Scalar ⁡ W = ℂ fld ↾ 𝑠 Base Scalar ⁡ W ∧ Base Scalar ⁡ W ∈ SubRing ⁡ ℂ fld
7 1 4 5 6 syl3anbrc ⊢ W ∈ CPreHil → W ∈ CMod