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	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
Assertion	reipcl	$⊢ (W \in CPreHil \land A \in V) \to A \underset{˙}{,} A \in ℝ$

Step	Hyp	Ref	Expression
1		reipcl.v	$⊢ V = {Base}_{W}$
2		reipcl.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
3		eqid	$⊢ norm (W) = norm (W)$
4	1 2 3	nmsq	$⊢ (W \in CPreHil \land A \in V) \to {norm (W) (A)}^{2} = A \underset{˙}{,} A$
5		cphngp	$⊢ W \in CPreHil \to W \in NrmGrp$
6	1 3	nmcl	$⊢ (W \in NrmGrp \land A \in V) \to norm (W) (A) \in ℝ$
7	5 6	sylan	$⊢ (W \in CPreHil \land A \in V) \to norm (W) (A) \in ℝ$
8	7	resqcld	$⊢ (W \in CPreHil \land A \in V) \to {norm (W) (A)}^{2} \in ℝ$
9	4 8	eqeltrrd	$⊢ (W \in CPreHil \land A \in V) \to A \underset{˙}{,} A \in ℝ$

Metamath Proof Explorer