Metamath Proof Explorer


Theorem cphip0r

Description: Inner product with a zero second argument. Complex version of ip0r . (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses cphipcj.h , ˙ = 𝑖 W
cphipcj.v V = Base W
cphip0l.z 0 ˙ = 0 W
Assertion cphip0r W CPreHil A V A , ˙ 0 ˙ = 0

Proof

Step Hyp Ref Expression
1 cphipcj.h , ˙ = 𝑖 W
2 cphipcj.v V = Base W
3 cphip0l.z 0 ˙ = 0 W
4 cphphl W CPreHil W PreHil
5 eqid Scalar W = Scalar W
6 eqid 0 Scalar W = 0 Scalar W
7 5 1 2 6 3 ip0r W PreHil A V A , ˙ 0 ˙ = 0 Scalar W
8 4 7 sylan W CPreHil A V A , ˙ 0 ˙ = 0 Scalar W
9 cphclm W CPreHil W CMod
10 5 clm0 W CMod 0 = 0 Scalar W
11 9 10 syl W CPreHil 0 = 0 Scalar W
12 11 adantr W CPreHil A V 0 = 0 Scalar W
13 8 12 eqtr4d W CPreHil A V A , ˙ 0 ˙ = 0