Step |
Hyp |
Ref |
Expression |
1 |
|
h2h.1 |
⊢ 𝑈 = 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 |
2 |
|
h2h.2 |
⊢ 𝑈 ∈ NrmCVec |
3 |
1
|
fveq2i |
⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) |
4 |
|
eqid |
⊢ ( normCV ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) = ( normCV ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) |
5 |
4
|
nmcvfval |
⊢ ( normCV ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) = ( 2nd ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) |
6 |
|
opex |
⊢ 〈 +ℎ , ·ℎ 〉 ∈ V |
7 |
1 2
|
eqeltrri |
⊢ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ∈ NrmCVec |
8 |
|
nvex |
⊢ ( 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ∈ NrmCVec → ( +ℎ ∈ V ∧ ·ℎ ∈ V ∧ normℎ ∈ V ) ) |
9 |
7 8
|
ax-mp |
⊢ ( +ℎ ∈ V ∧ ·ℎ ∈ V ∧ normℎ ∈ V ) |
10 |
9
|
simp3i |
⊢ normℎ ∈ V |
11 |
6 10
|
op2nd |
⊢ ( 2nd ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) = normℎ |
12 |
3 5 11
|
3eqtrri |
⊢ normℎ = ( normCV ‘ 𝑈 ) |