Step |
Hyp |
Ref |
Expression |
1 |
|
fveq2 |
⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( normℎ ‘ 𝐴 ) = ( normℎ ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ) |
2 |
1
|
oveq1d |
⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( normℎ ‘ 𝐴 ) ↑ 2 ) = ( ( normℎ ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ↑ 2 ) ) |
3 |
|
id |
⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) |
4 |
3 3
|
oveq12d |
⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( 𝐴 ·ih 𝐴 ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ) |
5 |
2 4
|
eqeq12d |
⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( ( normℎ ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 ·ih 𝐴 ) ↔ ( ( normℎ ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ↑ 2 ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ) ) |
6 |
|
ifhvhv0 |
⊢ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ∈ ℋ |
7 |
6
|
normsqi |
⊢ ( ( normℎ ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ↑ 2 ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) |
8 |
5 7
|
dedth |
⊢ ( 𝐴 ∈ ℋ → ( ( normℎ ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 ·ih 𝐴 ) ) |