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 )