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

Metamath Proof Explorer

Theorem normsq

Description: The square of a norm. (Contributed by NM, 12-May-2005) (New usage is discouraged.)

Ref Expression
Assertion normsq ⊢ A ∈ ℋ → norm ℎ ⁡ A 2 = A ⋅ ih A

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ
2 1 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2
3 id ⊢ A = if A ∈ ℋ A 0 ℎ → A = if A ∈ ℋ A 0 ℎ
4 3 3 oveq12d ⊢ A = if A ∈ ℋ A 0 ℎ → A ⋅ ih A = if A ∈ ℋ A 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ
5 2 4 eqeq12d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A 2 = A ⋅ ih A ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2 = if A ∈ ℋ A 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ
6 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
7 6 normsqi ⊢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2 = if A ∈ ℋ A 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ
8 5 7 dedth ⊢ A ∈ ℋ → norm ℎ ⁡ A 2 = A ⋅ ih A