Step |
Hyp |
Ref |
Expression |
1 |
|
nvf.1 |
⊢ 𝑋 = ( BaseSet ‘ 𝑈 ) |
2 |
|
nvf.6 |
⊢ 𝑁 = ( normCV ‘ 𝑈 ) |
3 |
|
eqid |
⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 ) |
4 |
|
eqid |
⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 ) |
5 |
|
eqid |
⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 ) |
6 |
1 3 4 5 2
|
nvi |
⊢ ( 𝑈 ∈ NrmCVec → ( 〈 ( +𝑣 ‘ 𝑈 ) , ( ·𝑠OLD ‘ 𝑈 ) 〉 ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = ( 0vec ‘ 𝑈 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) |
7 |
6
|
simp2d |
⊢ ( 𝑈 ∈ NrmCVec → 𝑁 : 𝑋 ⟶ ℝ ) |