Step |
Hyp |
Ref |
Expression |
1 |
|
imsdfn.1 |
⊢ 𝑋 = ( BaseSet ‘ 𝑈 ) |
2 |
|
imsdfn.8 |
⊢ 𝐷 = ( IndMet ‘ 𝑈 ) |
3 |
|
eqid |
⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 ) |
4 |
1 3
|
nvf |
⊢ ( 𝑈 ∈ NrmCVec → ( normCV ‘ 𝑈 ) : 𝑋 ⟶ ℝ ) |
5 |
|
eqid |
⊢ ( −𝑣 ‘ 𝑈 ) = ( −𝑣 ‘ 𝑈 ) |
6 |
1 5
|
nvmf |
⊢ ( 𝑈 ∈ NrmCVec → ( −𝑣 ‘ 𝑈 ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) |
7 |
|
fco |
⊢ ( ( ( normCV ‘ 𝑈 ) : 𝑋 ⟶ ℝ ∧ ( −𝑣 ‘ 𝑈 ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) → ( ( normCV ‘ 𝑈 ) ∘ ( −𝑣 ‘ 𝑈 ) ) : ( 𝑋 × 𝑋 ) ⟶ ℝ ) |
8 |
4 6 7
|
syl2anc |
⊢ ( 𝑈 ∈ NrmCVec → ( ( normCV ‘ 𝑈 ) ∘ ( −𝑣 ‘ 𝑈 ) ) : ( 𝑋 × 𝑋 ) ⟶ ℝ ) |
9 |
5 3 2
|
imsval |
⊢ ( 𝑈 ∈ NrmCVec → 𝐷 = ( ( normCV ‘ 𝑈 ) ∘ ( −𝑣 ‘ 𝑈 ) ) ) |
10 |
9
|
feq1d |
⊢ ( 𝑈 ∈ NrmCVec → ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ↔ ( ( normCV ‘ 𝑈 ) ∘ ( −𝑣 ‘ 𝑈 ) ) : ( 𝑋 × 𝑋 ) ⟶ ℝ ) ) |
11 |
8 10
|
mpbird |
⊢ ( 𝑈 ∈ NrmCVec → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) |