h2hva

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

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

Metamath Proof Explorer