Theorem ip0l

Description: Inner product with a zero first argument. Part of proof of Theorem 6.44 of Ponnusamy p. 361. (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	ip0l	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to \underset{\dot{}}{0}\underset{\dot{}}{,}A=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		phllmod	$$⊢W\in \mathrm{PreHil}\to W\in \mathrm{LMod}$$
7		lmodgrp	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Grp}$$
8	3 5	grpidcl	$$⊢W\in \mathrm{Grp}\to \underset{\dot{}}{0}\in V$$
9	6 7 8	3syl	$$⊢W\in \mathrm{PreHil}\to \underset{\dot{}}{0}\in V$$
10	9	adantr	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to \underset{\dot{}}{0}\in V$$
11		oveq1	$$⊢x=\underset{\dot{}}{0}\to x\underset{\dot{}}{,}A=\underset{\dot{}}{0}\underset{\dot{}}{,}A$$
12		eqid	$$⊢\left(x\in V⟼x\underset{\dot{}}{,}A\right)=\left(x\in V⟼x\underset{\dot{}}{,}A\right)$$
13		ovex	$$⊢\underset{\dot{}}{0}\underset{\dot{}}{,}A\in \mathrm{V}$$
14	11 12 13	fvmpt	$$⊢\underset{\dot{}}{0}\in V\to \left(x\in V⟼x\underset{\dot{}}{,}A\right)\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}\underset{\dot{}}{,}A$$
15	10 14	syl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to \left(x\in V⟼x\underset{\dot{}}{,}A\right)\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}\underset{\dot{}}{,}A$$
16	1 2 3 12	phllmhm	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to \left(x\in V⟼x\underset{\dot{}}{,}A\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)$$
17		lmghm	$$⊢\left(x\in V⟼x\underset{\dot{}}{,}A\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)\to \left(x\in V⟼x\underset{\dot{}}{,}A\right)\in \left(W\mathrm{GrpHom}\mathrm{ringLMod}\left(F\right)\right)$$
18		rlm0	$$⊢0_F=0_{\mathrm{ringLMod}\left(F\right)}$$
19	4 18	eqtri	$$⊢Z=0_{\mathrm{ringLMod}\left(F\right)}$$
20	5 19	ghmid	$$⊢\left(x\in V⟼x\underset{\dot{}}{,}A\right)\in \left(W\mathrm{GrpHom}\mathrm{ringLMod}\left(F\right)\right)\to \left(x\in V⟼x\underset{\dot{}}{,}A\right)\left(\underset{\dot{}}{0}\right)=Z$$
21	16 17 20	3syl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to \left(x\in V⟼x\underset{\dot{}}{,}A\right)\left(\underset{\dot{}}{0}\right)=Z$$
22	15 21	eqtr3d	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to \underset{\dot{}}{0}\underset{\dot{}}{,}A=Z$$