# Metamath Proof Explorer

## 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
phllmhm.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
ip0l.z ${⊢}{Z}={0}_{{F}}$
ip0l.o
Assertion ip0r

### Proof

Step Hyp Ref Expression
1 phlsrng.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
2 phllmhm.h
3 phllmhm.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
4 ip0l.z ${⊢}{Z}={0}_{{F}}$
5 ip0l.o
6 1 2 3 4 5 ip0l
7 6 fveq2d
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
11 9 10 syl
12 eqid ${⊢}{*}_{{F}}={*}_{{F}}$
13 1 2 3 12 ipcj
14 13 3expa
15 14 an32s
16 11 15 mpdan
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}}^{{*}_{{F}}}={Z}$
20 18 19 syl ${⊢}\left({W}\in \mathrm{PreHil}\wedge {A}\in {V}\right)\to {{Z}}^{{*}_{{F}}}={Z}$
21 7 16 20 3eqtr3d