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	$$⊢V={\mathrm{Base}}_W$$
	nmsq.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
Assertion	cphipcl	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge B\in V\right)\to A\underset{\dot{}}{,}B\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		nmsq.v	$$⊢V={\mathrm{Base}}_W$$
2		nmsq.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
3		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
4		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
5	3 4	cphsubrg	$$⊢W\in \mathrm{CPreHil}\to {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
6		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
7	6	subrgss	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\subseteq ℂ$$
8	5 7	syl	$$⊢W\in \mathrm{CPreHil}\to {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\subseteq ℂ$$
9	8	3ad2ant1	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge B\in V\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\subseteq ℂ$$
10		cphphl	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{PreHil}$$
11	3 2 1 4	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to A\underset{\dot{}}{,}B\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
12	10 11	syl3an1	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge B\in V\right)\to A\underset{\dot{}}{,}B\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
13	9 12	sseldd	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge B\in V\right)\to A\underset{\dot{}}{,}B\in ℂ$$