Metamath Proof Explorer


Theorem reipcl

Description: An inner product of an element with itself is real. (Contributed by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses reipcl.v V = Base W
reipcl.h , ˙ = 𝑖 W
Assertion reipcl W CPreHil A V A , ˙ A

Proof

Step Hyp Ref Expression
1 reipcl.v V = Base W
2 reipcl.h , ˙ = 𝑖 W
3 eqid norm W = norm W
4 1 2 3 nmsq W CPreHil A V norm W A 2 = A , ˙ A
5 cphngp W CPreHil W NrmGrp
6 1 3 nmcl W NrmGrp A V norm W A
7 5 6 sylan W CPreHil A V norm W A
8 7 resqcld W CPreHil A V norm W A 2
9 4 8 eqeltrrd W CPreHil A V A , ˙ A