ipnm

Description: Norm expressed in terms of inner product. (Contributed by NM, 11-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ipid.1	$⊢ X = BaseSet (U)$
	ipid.6	$⊢ N = {norm}_{CV} (U)$
	ipid.7	$⊢ P = \cdot_{𝑖OLD} (U)$
Assertion	ipnm	$⊢ (U \in NrmCVec \land A \in X) \to N (A) = \sqrt{A P A}$

Step	Hyp	Ref	Expression
1		ipid.1	$⊢ X = BaseSet (U)$
2		ipid.6	$⊢ N = {norm}_{CV} (U)$
3		ipid.7	$⊢ P = \cdot_{𝑖OLD} (U)$
4	1 2 3	ipidsq	$⊢ (U \in NrmCVec \land A \in X) \to A P A = {N (A)}^{2}$
5	4	fveq2d	$⊢ (U \in NrmCVec \land A \in X) \to \sqrt{A P A} = \sqrt{{N (A)}^{2}}$
6	1 2	nvcl	$⊢ (U \in NrmCVec \land A \in X) \to N (A) \in ℝ$
7	1 2	nvge0	$⊢ (U \in NrmCVec \land A \in X) \to 0 \leq N (A)$
8	6 7	sqrtsqd	$⊢ (U \in NrmCVec \land A \in X) \to \sqrt{{N (A)}^{2}} = N (A)$
9	5 8	eqtr2d	$⊢ (U \in NrmCVec \land A \in X) \to N (A) = \sqrt{A P A}$

Metamath Proof Explorer