# Metamath Proof Explorer

## Theorem norm-iii

Description: Theorem 3.3(iii) of Beran p. 97. (Contributed by NM, 25-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion norm-iii $⊢ A ∈ ℂ ∧ B ∈ ℋ → norm ℎ ⁡ A ⋅ ℎ B = A ⁢ norm ℎ ⁡ B$

### Proof

Step Hyp Ref Expression
1 fvoveq1 $⊢ A = if A ∈ ℂ A 0 → norm ℎ ⁡ A ⋅ ℎ B = norm ℎ ⁡ if A ∈ ℂ A 0 ⋅ ℎ B$
2 fveq2 $⊢ A = if A ∈ ℂ A 0 → A = if A ∈ ℂ A 0$
3 2 oveq1d $⊢ A = if A ∈ ℂ A 0 → A ⁢ norm ℎ ⁡ B = if A ∈ ℂ A 0 ⁢ norm ℎ ⁡ B$
4 1 3 eqeq12d $⊢ A = if A ∈ ℂ A 0 → norm ℎ ⁡ A ⋅ ℎ B = A ⁢ norm ℎ ⁡ B ↔ norm ℎ ⁡ if A ∈ ℂ A 0 ⋅ ℎ B = if A ∈ ℂ A 0 ⁢ norm ℎ ⁡ B$
5 oveq2 $⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℂ A 0 ⋅ ℎ B = if A ∈ ℂ A 0 ⋅ ℎ if B ∈ ℋ B 0 ℎ$
6 5 fveq2d $⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℂ A 0 ⋅ ℎ B = norm ℎ ⁡ if A ∈ ℂ A 0 ⋅ ℎ if B ∈ ℋ B 0 ℎ$
7 fveq2 $⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ B = norm ℎ ⁡ if B ∈ ℋ B 0 ℎ$
8 7 oveq2d $⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℂ A 0 ⁢ norm ℎ ⁡ B = if A ∈ ℂ A 0 ⁢ norm ℎ ⁡ if B ∈ ℋ B 0 ℎ$
9 6 8 eqeq12d $⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℂ A 0 ⋅ ℎ B = if A ∈ ℂ A 0 ⁢ norm ℎ ⁡ B ↔ norm ℎ ⁡ if A ∈ ℂ A 0 ⋅ ℎ if B ∈ ℋ B 0 ℎ = if A ∈ ℂ A 0 ⁢ norm ℎ ⁡ if B ∈ ℋ B 0 ℎ$
10 0cn $⊢ 0 ∈ ℂ$
11 10 elimel $⊢ if A ∈ ℂ A 0 ∈ ℂ$
12 ifhvhv0 $⊢ if B ∈ ℋ B 0 ℎ ∈ ℋ$
13 11 12 norm-iii-i $⊢ norm ℎ ⁡ if A ∈ ℂ A 0 ⋅ ℎ if B ∈ ℋ B 0 ℎ = if A ∈ ℂ A 0 ⁢ norm ℎ ⁡ if B ∈ ℋ B 0 ℎ$
14 4 9 13 dedth2h $⊢ A ∈ ℂ ∧ B ∈ ℋ → norm ℎ ⁡ A ⋅ ℎ B = A ⁢ norm ℎ ⁡ B$