Step |
Hyp |
Ref |
Expression |
1 |
|
h2h.1 |
⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ |
2 |
|
h2h.2 |
⊢ 𝑈 ∈ NrmCVec |
3 |
|
eqid |
⊢ ( ·𝑠OLD ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) = ( ·𝑠OLD ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) |
4 |
3
|
smfval |
⊢ ( ·𝑠OLD ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) = ( 2nd ‘ ( 1st ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) |
5 |
|
opex |
⊢ ⟨ +ℎ , ·ℎ ⟩ ∈ V |
6 |
1 2
|
eqeltrri |
⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ NrmCVec |
7 |
|
nvex |
⊢ ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ NrmCVec → ( +ℎ ∈ V ∧ ·ℎ ∈ V ∧ normℎ ∈ V ) ) |
8 |
6 7
|
ax-mp |
⊢ ( +ℎ ∈ V ∧ ·ℎ ∈ V ∧ normℎ ∈ V ) |
9 |
8
|
simp3i |
⊢ normℎ ∈ V |
10 |
5 9
|
op1st |
⊢ ( 1st ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) = ⟨ +ℎ , ·ℎ ⟩ |
11 |
10
|
fveq2i |
⊢ ( 2nd ‘ ( 1st ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) = ( 2nd ‘ ⟨ +ℎ , ·ℎ ⟩ ) |
12 |
8
|
simp1i |
⊢ +ℎ ∈ V |
13 |
8
|
simp2i |
⊢ ·ℎ ∈ V |
14 |
12 13
|
op2nd |
⊢ ( 2nd ‘ ⟨ +ℎ , ·ℎ ⟩ ) = ·ℎ |
15 |
4 11 14
|
3eqtrri |
⊢ ·ℎ = ( ·𝑠OLD ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) |
16 |
1
|
fveq2i |
⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) |
17 |
15 16
|
eqtr4i |
⊢ ·ℎ = ( ·𝑠OLD ‘ 𝑈 ) |