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 
|- G = ( toCPreHil ` W )
tcphcph.v 
|- V = ( Base ` W )
tcphcph.f 
|- F = ( Scalar ` W )
tcphcph.1 
|- ( ph -> W e. PreHil )
tcphcph.2 
|- ( ph -> F = ( CCfld |`s K ) )
Assertion phclm 
|- ( ph -> W e. 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 
 |-  ( ph -> W e. PreHil )
5 tcphcph.2 
 |-  ( ph -> F = ( CCfld |`s K ) )
6 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
7 4 6 syl 
 |-  ( ph -> W e. LMod )
8 eqid 
 |-  ( Base ` F ) = ( Base ` F )
9 phllvec 
 |-  ( W e. PreHil -> W e. LVec )
10 4 9 syl 
 |-  ( ph -> W e. LVec )
11 3 lvecdrng 
 |-  ( W e. LVec -> F e. DivRing )
12 10 11 syl 
 |-  ( ph -> F e. DivRing )
13 8 5 12 cphsubrglem 
 |-  ( ph -> ( F = ( CCfld |`s ( Base ` F ) ) /\ ( Base ` F ) = ( K i^i CC ) /\ ( Base ` F ) e. ( SubRing ` CCfld ) ) )
14 13 simp1d 
 |-  ( ph -> F = ( CCfld |`s ( Base ` F ) ) )
15 13 simp3d 
 |-  ( ph -> ( Base ` F ) e. ( SubRing ` CCfld ) )
16 3 8 isclm 
 |-  ( W e. CMod <-> ( W e. LMod /\ F = ( CCfld |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` CCfld ) ) )
17 7 14 15 16 syl3anbrc 
 |-  ( ph -> W e. CMod )