Theorem ipge0

Description: The inner product in a subcomplex pre-Hilbert space is positive definite. (Contributed by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	reipcl.v	$$⊢V={\mathrm{Base}}_W$$
	reipcl.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
Assertion	ipge0	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to 0\le A\underset{\dot{}}{,}A$$

Proof

Step	Hyp	Ref	Expression
1		reipcl.v	$$⊢V={\mathrm{Base}}_W$$
2		reipcl.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
3		cphngp	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{NrmGrp}$$
4		eqid	$$⊢\mathrm{norm}\left(W\right)=\mathrm{norm}\left(W\right)$$
5	1 4	nmcl	$$⊢\left(W\in \mathrm{NrmGrp}\wedge A\in V\right)\to \mathrm{norm}\left(W\right)\left(A\right)\in ℝ$$
6	3 5	sylan	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to \mathrm{norm}\left(W\right)\left(A\right)\in ℝ$$
7	6	sqge0d	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to 0\le {\mathrm{norm}\left(W\right)\left(A\right)}^2$$
8	1 2 4	nmsq	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to {\mathrm{norm}\left(W\right)\left(A\right)}^2=A\underset{\dot{}}{,}A$$
9	7 8	breqtrd	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to 0\le A\underset{\dot{}}{,}A$$