Theorem ip0r

Description: Inner product with a zero second argument. (Contributed by NM, 5-Feb-2007) (Revised by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	phlsrng.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	phllmhm.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	phllmhm.v	$$⊢V={\mathrm{Base}}_W$$
	ip0l.z	$$⊢Z=0_F$$
	ip0l.o	$$⊢\underset{\dot{}}{0}=0_W$$
Assertion	ip0r	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to A\underset{\dot{}}{,}\underset{\dot{}}{0}=Z$$

Proof

Step	Hyp	Ref	Expression
1		phlsrng.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		phllmhm.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
3		phllmhm.v	$$⊢V={\mathrm{Base}}_W$$
4		ip0l.z	$$⊢Z=0_F$$
5		ip0l.o	$$⊢\underset{\dot{}}{0}=0_W$$
6	1 2 3 4 5	ip0l	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to \underset{\dot{}}{0}\underset{\dot{}}{,}A=Z$$
7	6	fveq2d	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to {\left(\underset{\dot{}}{0}\underset{\dot{}}{,}A\right)}^{{\mathrm{*}}_F}=Z^{{\mathrm{*}}_F}$$
8		phllmod	$$⊢W\in \mathrm{PreHil}\to W\in \mathrm{LMod}$$
9	8	adantr	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to W\in \mathrm{LMod}$$
10	3 5	lmod0vcl	$$⊢W\in \mathrm{LMod}\to \underset{\dot{}}{0}\in V$$
11	9 10	syl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to \underset{\dot{}}{0}\in V$$
12		eqid	$$⊢{\mathrm{*}}_F={\mathrm{*}}_F$$
13	1 2 3 12	ipcj	$$⊢\left(W\in \mathrm{PreHil}\wedge \underset{\dot{}}{0}\in V\wedge A\in V\right)\to {\left(\underset{\dot{}}{0}\underset{\dot{}}{,}A\right)}^{{\mathrm{*}}_F}=A\underset{\dot{}}{,}\underset{\dot{}}{0}$$
14	13	3expa	$$⊢\left(\left(W\in \mathrm{PreHil}\wedge \underset{\dot{}}{0}\in V\right)\wedge A\in V\right)\to {\left(\underset{\dot{}}{0}\underset{\dot{}}{,}A\right)}^{{\mathrm{*}}_F}=A\underset{\dot{}}{,}\underset{\dot{}}{0}$$
15	14	an32s	$$⊢\left(\left(W\in \mathrm{PreHil}\wedge A\in V\right)\wedge \underset{\dot{}}{0}\in V\right)\to {\left(\underset{\dot{}}{0}\underset{\dot{}}{,}A\right)}^{{\mathrm{*}}_F}=A\underset{\dot{}}{,}\underset{\dot{}}{0}$$
16	11 15	mpdan	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to {\left(\underset{\dot{}}{0}\underset{\dot{}}{,}A\right)}^{{\mathrm{*}}_F}=A\underset{\dot{}}{,}\underset{\dot{}}{0}$$
17	1	phlsrng	$$⊢W\in \mathrm{PreHil}\to F\in \mathrm{*-Ring}$$
18	17	adantr	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to F\in \mathrm{*-Ring}$$
19	12 4	srng0	$$⊢F\in \mathrm{*-Ring}\to Z^{{\mathrm{*}}_F}=Z$$
20	18 19	syl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to Z^{{\mathrm{*}}_F}=Z$$
21	7 16 20	3eqtr3d	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to A\underset{\dot{}}{,}\underset{\dot{}}{0}=Z$$