Metamath Proof Explorer


Theorem ipnm

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

Ref Expression
Hypotheses ipid.1 𝑋 = ( BaseSet ‘ 𝑈 )
ipid.6 𝑁 = ( normCV𝑈 )
ipid.7 𝑃 = ( ·𝑖OLD𝑈 )
Assertion ipnm ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( 𝑁𝐴 ) = ( √ ‘ ( 𝐴 𝑃 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 ipid.1 𝑋 = ( BaseSet ‘ 𝑈 )
2 ipid.6 𝑁 = ( normCV𝑈 )
3 ipid.7 𝑃 = ( ·𝑖OLD𝑈 )
4 1 2 3 ipidsq ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( 𝐴 𝑃 𝐴 ) = ( ( 𝑁𝐴 ) ↑ 2 ) )
5 4 fveq2d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( √ ‘ ( 𝐴 𝑃 𝐴 ) ) = ( √ ‘ ( ( 𝑁𝐴 ) ↑ 2 ) ) )
6 1 2 nvcl ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( 𝑁𝐴 ) ∈ ℝ )
7 1 2 nvge0 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → 0 ≤ ( 𝑁𝐴 ) )
8 6 7 sqrtsqd ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( √ ‘ ( ( 𝑁𝐴 ) ↑ 2 ) ) = ( 𝑁𝐴 ) )
9 5 8 eqtr2d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( 𝑁𝐴 ) = ( √ ‘ ( 𝐴 𝑃 𝐴 ) ) )