Theorem cphclm

Description: A subcomplex pre-Hilbert space is a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Assertion	cphclm	⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod )

Proof

Step	Hyp	Ref	Expression
1		cphlmod	⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod )
2		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
3		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
4	2 3	cphsca	⊢ ( 𝑊 ∈ ℂPreHil → ( Scalar ‘ 𝑊 ) = ( ℂfld ↾s ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
5	2 3	cphsubrg	⊢ ( 𝑊 ∈ ℂPreHil → ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( SubRing ‘ ℂfld ) )
6	2 3	isclm	⊢ ( 𝑊 ∈ ℂMod ↔ ( 𝑊 ∈ LMod ∧ ( Scalar ‘ 𝑊 ) = ( ℂfld ↾s ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( SubRing ‘ ℂfld ) ) )
7	1 4 5 6	syl3anbrc	⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod )