Theorem cphip0l

Description: Inner product with a zero first argument. Part of proof of Theorem 6.44 of Ponnusamy p. 361. Complex version of ip0l . (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	cphipcj.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	cphipcj.v	$$⊢V={\mathrm{Base}}_W$$
	cphip0l.z	$$⊢\underset{\dot{}}{0}=0_W$$
Assertion	cphip0l	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to \underset{\dot{}}{0}\underset{\dot{}}{,}A=0$$

Proof

Step	Hyp	Ref	Expression
1		cphipcj.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
2		cphipcj.v	$$⊢V={\mathrm{Base}}_W$$
3		cphip0l.z	$$⊢\underset{\dot{}}{0}=0_W$$
4		cphphl	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{PreHil}$$
5		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
6		eqid	$$⊢0_{\mathrm{Scalar}\left(W\right)}=0_{\mathrm{Scalar}\left(W\right)}$$
7	5 1 2 6 3	ip0l	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to \underset{\dot{}}{0}\underset{\dot{}}{,}A=0_{\mathrm{Scalar}\left(W\right)}$$
8	4 7	sylan	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to \underset{\dot{}}{0}\underset{\dot{}}{,}A=0_{\mathrm{Scalar}\left(W\right)}$$
9		cphclm	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{CMod}$$
10	5	clm0	$$⊢W\in \mathrm{CMod}\to 0=0_{\mathrm{Scalar}\left(W\right)}$$
11	9 10	syl	$$⊢W\in \mathrm{CPreHil}\to 0=0_{\mathrm{Scalar}\left(W\right)}$$
12	11	adantr	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to 0=0_{\mathrm{Scalar}\left(W\right)}$$
13	8 12	eqtr4d	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to \underset{\dot{}}{0}\underset{\dot{}}{,}A=0$$