Step |
Hyp |
Ref |
Expression |
1 |
|
imsval.3 |
⊢ 𝑀 = ( −𝑣 ‘ 𝑈 ) |
2 |
|
imsval.6 |
⊢ 𝑁 = ( normCV ‘ 𝑈 ) |
3 |
|
imsval.8 |
⊢ 𝐷 = ( IndMet ‘ 𝑈 ) |
4 |
|
fveq2 |
⊢ ( 𝑢 = 𝑈 → ( normCV ‘ 𝑢 ) = ( normCV ‘ 𝑈 ) ) |
5 |
|
fveq2 |
⊢ ( 𝑢 = 𝑈 → ( −𝑣 ‘ 𝑢 ) = ( −𝑣 ‘ 𝑈 ) ) |
6 |
4 5
|
coeq12d |
⊢ ( 𝑢 = 𝑈 → ( ( normCV ‘ 𝑢 ) ∘ ( −𝑣 ‘ 𝑢 ) ) = ( ( normCV ‘ 𝑈 ) ∘ ( −𝑣 ‘ 𝑈 ) ) ) |
7 |
|
df-ims |
⊢ IndMet = ( 𝑢 ∈ NrmCVec ↦ ( ( normCV ‘ 𝑢 ) ∘ ( −𝑣 ‘ 𝑢 ) ) ) |
8 |
|
fvex |
⊢ ( normCV ‘ 𝑈 ) ∈ V |
9 |
|
fvex |
⊢ ( −𝑣 ‘ 𝑈 ) ∈ V |
10 |
8 9
|
coex |
⊢ ( ( normCV ‘ 𝑈 ) ∘ ( −𝑣 ‘ 𝑈 ) ) ∈ V |
11 |
6 7 10
|
fvmpt |
⊢ ( 𝑈 ∈ NrmCVec → ( IndMet ‘ 𝑈 ) = ( ( normCV ‘ 𝑈 ) ∘ ( −𝑣 ‘ 𝑈 ) ) ) |
12 |
2 1
|
coeq12i |
⊢ ( 𝑁 ∘ 𝑀 ) = ( ( normCV ‘ 𝑈 ) ∘ ( −𝑣 ‘ 𝑈 ) ) |
13 |
11 3 12
|
3eqtr4g |
⊢ ( 𝑈 ∈ NrmCVec → 𝐷 = ( 𝑁 ∘ 𝑀 ) ) |