Step |
Hyp |
Ref |
Expression |
1 |
|
cnnv.6 |
⊢ 𝑈 = 〈 〈 + , · 〉 , abs 〉 |
2 |
|
cnaddabloOLD |
⊢ + ∈ AbelOp |
3 |
|
ablogrpo |
⊢ ( + ∈ AbelOp → + ∈ GrpOp ) |
4 |
2 3
|
ax-mp |
⊢ + ∈ GrpOp |
5 |
|
ax-addf |
⊢ + : ( ℂ × ℂ ) ⟶ ℂ |
6 |
5
|
fdmi |
⊢ dom + = ( ℂ × ℂ ) |
7 |
4 6
|
grporn |
⊢ ℂ = ran + |
8 |
|
cnidOLD |
⊢ 0 = ( GId ‘ + ) |
9 |
|
cncvcOLD |
⊢ 〈 + , · 〉 ∈ CVecOLD |
10 |
|
absf |
⊢ abs : ℂ ⟶ ℝ |
11 |
|
abs00 |
⊢ ( 𝑥 ∈ ℂ → ( ( abs ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ) |
12 |
11
|
biimpa |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( abs ‘ 𝑥 ) = 0 ) → 𝑥 = 0 ) |
13 |
|
absmul |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( abs ‘ ( 𝑦 · 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( abs ‘ 𝑥 ) ) ) |
14 |
|
abstri |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( abs ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( abs ‘ 𝑥 ) + ( abs ‘ 𝑦 ) ) ) |
15 |
7 8 9 10 12 13 14 1
|
isnvi |
⊢ 𝑈 ∈ NrmCVec |