Step |
Hyp |
Ref |
Expression |
1 |
|
isnvi.5 |
⊢ 𝑋 = ran 𝐺 |
2 |
|
isnvi.6 |
⊢ 𝑍 = ( GId ‘ 𝐺 ) |
3 |
|
isnvi.7 |
⊢ 〈 𝐺 , 𝑆 〉 ∈ CVecOLD |
4 |
|
isnvi.8 |
⊢ 𝑁 : 𝑋 ⟶ ℝ |
5 |
|
isnvi.9 |
⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑥 ) = 0 ) → 𝑥 = 𝑍 ) |
6 |
|
isnvi.10 |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ) |
7 |
|
isnvi.11 |
⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) |
8 |
|
isnvi.12 |
⊢ 𝑈 = 〈 〈 𝐺 , 𝑆 〉 , 𝑁 〉 |
9 |
5
|
ex |
⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ) |
10 |
6
|
ancoms |
⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) → ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ) |
11 |
10
|
ralrimiva |
⊢ ( 𝑥 ∈ 𝑋 → ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ) |
12 |
7
|
ralrimiva |
⊢ ( 𝑥 ∈ 𝑋 → ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) |
13 |
9 11 12
|
3jca |
⊢ ( 𝑥 ∈ 𝑋 → ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) |
14 |
13
|
rgen |
⊢ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) |
15 |
1 2
|
isnv |
⊢ ( 〈 〈 𝐺 , 𝑆 〉 , 𝑁 〉 ∈ NrmCVec ↔ ( 〈 𝐺 , 𝑆 〉 ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) |
16 |
3 4 14 15
|
mpbir3an |
⊢ 〈 〈 𝐺 , 𝑆 〉 , 𝑁 〉 ∈ NrmCVec |
17 |
8 16
|
eqeltri |
⊢ 𝑈 ∈ NrmCVec |