Metamath Proof Explorer


Theorem h2hva

Description: The group (addition) operation of Hilbert space. (Contributed by NM, 31-May-2008) (New usage is discouraged.)

Ref Expression
Hypotheses h2h.1 𝑈 = ⟨ ⟨ + , · ⟩ , norm
h2h.2 𝑈 ∈ NrmCVec
Assertion h2hva + = ( +𝑣𝑈 )

Proof

Step Hyp Ref Expression
1 h2h.1 𝑈 = ⟨ ⟨ + , · ⟩ , norm
2 h2h.2 𝑈 ∈ NrmCVec
3 eqid ( +𝑣 ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ ) = ( +𝑣 ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ )
4 3 vafval ( +𝑣 ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ ) = ( 1st ‘ ( 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 ( 1st ‘ ( 1st ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ ) ) = ( 1st ‘ ⟨ + , · ⟩ )
12 8 simp1i + ∈ V
13 8 simp2i · ∈ V
14 12 13 op1st ( 1st ‘ ⟨ + , · ⟩ ) = +
15 4 11 14 3eqtrri + = ( +𝑣 ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ )
16 1 fveq2i ( +𝑣𝑈 ) = ( +𝑣 ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ )
17 15 16 eqtr4i + = ( +𝑣𝑈 )