Step |
Hyp |
Ref |
Expression |
1 |
|
hhsssh2.1 |
⊢ 𝑊 = 〈 〈 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 〉 , ( normℎ ↾ 𝐻 ) 〉 |
2 |
|
hhssims.2 |
⊢ 𝐻 ∈ Sℋ |
3 |
|
hhssims.3 |
⊢ 𝐷 = ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) ) |
4 |
1 2
|
hhssnv |
⊢ 𝑊 ∈ NrmCVec |
5 |
1 2
|
hhssvs |
⊢ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) = ( −𝑣 ‘ 𝑊 ) |
6 |
1
|
hhssnm |
⊢ ( normℎ ↾ 𝐻 ) = ( normCV ‘ 𝑊 ) |
7 |
|
eqid |
⊢ ( IndMet ‘ 𝑊 ) = ( IndMet ‘ 𝑊 ) |
8 |
5 6 7
|
imsval |
⊢ ( 𝑊 ∈ NrmCVec → ( IndMet ‘ 𝑊 ) = ( ( normℎ ↾ 𝐻 ) ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ) ) |
9 |
4 8
|
ax-mp |
⊢ ( IndMet ‘ 𝑊 ) = ( ( normℎ ↾ 𝐻 ) ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ) |
10 |
|
resco |
⊢ ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) ) = ( normℎ ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ) |
11 |
1 2
|
hhssvsf |
⊢ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) : ( 𝐻 × 𝐻 ) ⟶ 𝐻 |
12 |
|
frn |
⊢ ( ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) : ( 𝐻 × 𝐻 ) ⟶ 𝐻 → ran ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ) |
13 |
11 12
|
ax-mp |
⊢ ran ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 |
14 |
|
cores |
⊢ ( ran ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 → ( ( normℎ ↾ 𝐻 ) ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ) = ( normℎ ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ) ) |
15 |
13 14
|
ax-mp |
⊢ ( ( normℎ ↾ 𝐻 ) ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ) = ( normℎ ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ) |
16 |
10 15
|
eqtr4i |
⊢ ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) ) = ( ( normℎ ↾ 𝐻 ) ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ) |
17 |
9 16
|
eqtr4i |
⊢ ( IndMet ‘ 𝑊 ) = ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) ) |
18 |
3 17
|
eqtr4i |
⊢ 𝐷 = ( IndMet ‘ 𝑊 ) |