Step |
Hyp |
Ref |
Expression |
1 |
|
hhss.1 |
⊢ 𝑊 = 〈 〈 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 〉 , ( normℎ ↾ 𝐻 ) 〉 |
2 |
|
eqid |
⊢ ( normCV ‘ 𝑊 ) = ( normCV ‘ 𝑊 ) |
3 |
2
|
nmcvfval |
⊢ ( normCV ‘ 𝑊 ) = ( 2nd ‘ 𝑊 ) |
4 |
1
|
fveq2i |
⊢ ( 2nd ‘ 𝑊 ) = ( 2nd ‘ 〈 〈 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 〉 , ( normℎ ↾ 𝐻 ) 〉 ) |
5 |
|
opex |
⊢ 〈 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 〉 ∈ V |
6 |
|
normf |
⊢ normℎ : ℋ ⟶ ℝ |
7 |
|
ax-hilex |
⊢ ℋ ∈ V |
8 |
|
fex |
⊢ ( ( normℎ : ℋ ⟶ ℝ ∧ ℋ ∈ V ) → normℎ ∈ V ) |
9 |
6 7 8
|
mp2an |
⊢ normℎ ∈ V |
10 |
9
|
resex |
⊢ ( normℎ ↾ 𝐻 ) ∈ V |
11 |
5 10
|
op2nd |
⊢ ( 2nd ‘ 〈 〈 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 〉 , ( normℎ ↾ 𝐻 ) 〉 ) = ( normℎ ↾ 𝐻 ) |
12 |
3 4 11
|
3eqtrri |
⊢ ( normℎ ↾ 𝐻 ) = ( normCV ‘ 𝑊 ) |