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 )