Step |
Hyp |
Ref |
Expression |
1 |
|
nvs.1 |
⊢ 𝑋 = ( BaseSet ‘ 𝑈 ) |
2 |
|
nvs.4 |
⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 ) |
3 |
|
nvs.6 |
⊢ 𝑁 = ( normCV ‘ 𝑈 ) |
4 |
|
recn |
⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ ) |
5 |
4
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ℂ ) |
6 |
1 2 3
|
nvs |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝑆 𝐵 ) ) = ( ( abs ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) ) |
7 |
5 6
|
syl3an2 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝑆 𝐵 ) ) = ( ( abs ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) ) |
8 |
|
absid |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( abs ‘ 𝐴 ) = 𝐴 ) |
9 |
8
|
3ad2ant2 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ 𝑋 ) → ( abs ‘ 𝐴 ) = 𝐴 ) |
10 |
9
|
oveq1d |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ 𝑋 ) → ( ( abs ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) = ( 𝐴 · ( 𝑁 ‘ 𝐵 ) ) ) |
11 |
7 10
|
eqtrd |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝑆 𝐵 ) ) = ( 𝐴 · ( 𝑁 ‘ 𝐵 ) ) ) |