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 ⊢ 𝐴 ∈ ℋ
Assertion normsqi ( ( normℎ ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 ·ih 𝐴 )

Proof

Step Hyp Ref Expression
1 normcl.1 ⊢ 𝐴 ∈ ℋ
2 normval ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ 𝐴 ) = ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) )
3 1 2 ax-mp ⊢ ( normℎ ‘ 𝐴 ) = ( √ ‘ ( 𝐴 ·ih 𝐴 ) )
4 3 oveq1i ⊢ ( ( normℎ ‘ 𝐴 ) ↑ 2 ) = ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ↑ 2 )
5 hiidge0 ⊢ ( 𝐴 ∈ ℋ → 0 ≤ ( 𝐴 ·ih 𝐴 ) )
6 1 5 ax-mp ⊢ 0 ≤ ( 𝐴 ·ih 𝐴 )
7 hiidrcl ⊢ ( 𝐴 ∈ ℋ → ( 𝐴 ·ih 𝐴 ) ∈ ℝ )
8 1 7 ax-mp ⊢ ( 𝐴 ·ih 𝐴 ) ∈ ℝ
9 8 sqsqrti ⊢ ( 0 ≤ ( 𝐴 ·ih 𝐴 ) → ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ↑ 2 ) = ( 𝐴 ·ih 𝐴 ) )
10 6 9 ax-mp ⊢ ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ↑ 2 ) = ( 𝐴 ·ih 𝐴 )
11 4 10 eqtri ⊢ ( ( normℎ ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 ·ih 𝐴 )