Theorem cphipcl

Description: An inner product is a member of the complex numbers. (Contributed by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypotheses	nmsq.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	nmsq.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
Assertion	cphipcl	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 , 𝐵 ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		nmsq.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		nmsq.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
3		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
4		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
5	3 4	cphsubrg	⊢ ( 𝑊 ∈ ℂPreHil → ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( SubRing ‘ ℂfld ) )
6		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
7	6	subrgss	⊢ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( SubRing ‘ ℂfld ) → ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⊆ ℂ )
8	5 7	syl	⊢ ( 𝑊 ∈ ℂPreHil → ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⊆ ℂ )
9	8	3ad2ant1	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⊆ ℂ )
10		cphphl	⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil )
11	3 2 1 4	ipcl	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 , 𝐵 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
12	10 11	syl3an1	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 , 𝐵 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
13	9 12	sseldd	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 , 𝐵 ) ∈ ℂ )