This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) = ( √ ‘ ( 𝐴 𝑃 𝐴 ) ) )