Metamath Proof Explorer

Theorem phclm

Description: A pre-Hilbert space whose field of scalars is a restriction of the field of complex numbers is a subcomplex module. TODO: redundant hypotheses. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses tcphval.n ⊢ G = toCPreHil ⁡ W
tcphcph.v ⊢ V = Base W
tcphcph.f ⊢ F = Scalar ⁡ W
tcphcph.1 ⊢ φ → W ∈ PreHil
tcphcph.2 ⊢ φ → F = ℂ fld ↾ 𝑠 K
Assertion phclm ⊢ φ → W ∈ CMod

Proof

Step Hyp Ref Expression
1 tcphval.n ⊢ G = toCPreHil ⁡ W
2 tcphcph.v ⊢ V = Base W
3 tcphcph.f ⊢ F = Scalar ⁡ W
4 tcphcph.1 ⊢ φ → W ∈ PreHil
5 tcphcph.2 ⊢ φ → F = ℂ fld ↾ 𝑠 K
6 phllmod ⊢ W ∈ PreHil → W ∈ LMod
7 4 6 syl ⊢ φ → W ∈ LMod
8 eqid ⊢ Base F = Base F
9 phllvec ⊢ W ∈ PreHil → W ∈ LVec
10 4 9 syl ⊢ φ → W ∈ LVec
11 3 lvecdrng ⊢ W ∈ LVec → F ∈ DivRing
12 10 11 syl ⊢ φ → F ∈ DivRing
13 8 5 12 cphsubrglem ⊢ φ → F = ℂ fld ↾ 𝑠 Base F ∧ Base F = K ∩ ℂ ∧ Base F ∈ SubRing ⁡ ℂ fld
14 13 simp1d ⊢ φ → F = ℂ fld ↾ 𝑠 Base F
15 13 simp3d ⊢ φ → Base F ∈ SubRing ⁡ ℂ fld
16 3 8 isclm ⊢ W ∈ CMod ↔ W ∈ LMod ∧ F = ℂ fld ↾ 𝑠 Base F ∧ Base F ∈ SubRing ⁡ ℂ fld
17 7 14 15 16 syl3anbrc ⊢ φ → W ∈ CMod