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

Metamath Proof Explorer

Theorem normsqi

Description: The square of a norm. (Contributed by NM, 21-Aug-1999) (New usage is discouraged.)

Ref Expression
Hypothesis normcl.1 ⊢ A ∈ ℋ
Assertion normsqi ⊢ norm ℎ ⁡ A 2 = A ⋅ ih A

Proof

Step Hyp Ref Expression
1 normcl.1 ⊢ A ∈ ℋ
2 normval ⊢ A ∈ ℋ → norm ℎ ⁡ A = A ⋅ ih A
3 1 2 ax-mp ⊢ norm ℎ ⁡ A = A ⋅ ih A
4 3 oveq1i ⊢ norm ℎ ⁡ A 2 = A ⋅ ih A 2
5 hiidge0 ⊢ A ∈ ℋ → 0 ≤ A ⋅ ih A
6 1 5 ax-mp ⊢ 0 ≤ A ⋅ ih A
7 hiidrcl ⊢ A ∈ ℋ → A ⋅ ih A ∈ ℝ
8 1 7 ax-mp ⊢ A ⋅ ih A ∈ ℝ
9 8 sqsqrti ⊢ 0 ≤ A ⋅ ih A → A ⋅ ih A 2 = A ⋅ ih A
10 6 9 ax-mp ⊢ A ⋅ ih A 2 = A ⋅ ih A
11 4 10 eqtri ⊢ norm ℎ ⁡ A 2 = A ⋅ ih A