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

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 ⊢ 𝐺 = ( toℂPreHil ‘ 𝑊 )
tcphcph.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
tcphcph.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
tcphcph.1 ⊢ ( 𝜑 → 𝑊 ∈ PreHil )
tcphcph.2 ⊢ ( 𝜑 → 𝐹 = ( ℂfld ↾s 𝐾 ) )
Assertion phclm ( 𝜑 → 𝑊 ∈ ℂMod )

Proof

Step Hyp Ref Expression
1 tcphval.n ⊢ 𝐺 = ( toℂPreHil ‘ 𝑊 )
2 tcphcph.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
3 tcphcph.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4 tcphcph.1 ⊢ ( 𝜑 → 𝑊 ∈ PreHil )
5 tcphcph.2 ⊢ ( 𝜑 → 𝐹 = ( ℂfld ↾s 𝐾 ) )
6 phllmod ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
7 4 6 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
8 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
9 phllvec ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LVec )
10 4 9 syl ⊢ ( 𝜑 → 𝑊 ∈ LVec )
11 3 lvecdrng ⊢ ( 𝑊 ∈ LVec → 𝐹 ∈ DivRing )
12 10 11 syl ⊢ ( 𝜑 → 𝐹 ∈ DivRing )
13 8 5 12 cphsubrglem ⊢ ( 𝜑 → ( 𝐹 = ( ℂfld ↾s ( Base ‘ 𝐹 ) ) ∧ ( Base ‘ 𝐹 ) = ( 𝐾 ∩ ℂ ) ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ ℂfld ) ) )
14 13 simp1d ⊢ ( 𝜑 → 𝐹 = ( ℂfld ↾s ( Base ‘ 𝐹 ) ) )
15 13 simp3d ⊢ ( 𝜑 → ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ ℂfld ) )
16 3 8 isclm ⊢ ( 𝑊 ∈ ℂMod ↔ ( 𝑊 ∈ LMod ∧ 𝐹 = ( ℂfld ↾s ( Base ‘ 𝐹 ) ) ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ ℂfld ) ) )
17 7 14 15 16 syl3anbrc ⊢ ( 𝜑 → 𝑊 ∈ ℂMod )