This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hladdid

Description: Hilbert space addition with the zero vector. (Contributed by NM, 7-Sep-2007) (New usage is discouraged.)

Ref Expression
Hypotheses hladdid.1 ⊢ X = BaseSet ⁡ U
hladdid.2 ⊢ G = + v ⁡ U
hladdid.5 ⊢ Z = 0 vec ⁡ U
Assertion hladdid ⊢ U ∈ CHil OLD ∧ A ∈ X → A G Z = A

Proof

Step Hyp Ref Expression
1 hladdid.1 ⊢ X = BaseSet ⁡ U
2 hladdid.2 ⊢ G = + v ⁡ U
3 hladdid.5 ⊢ Z = 0 vec ⁡ U
4 hlnv ⊢ U ∈ CHil OLD → U ∈ NrmCVec
5 1 2 3 nv0rid ⊢ U ∈ NrmCVec ∧ A ∈ X → A G Z = A
6 4 5 sylan ⊢ U ∈ CHil OLD ∧ A ∈ X → A G Z = A