Metamath Proof Explorer


Theorem hladdf

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

Ref Expression
Hypotheses hladdf.1 X=BaseSetU
hladdf.2 G=+vU
Assertion hladdf UCHilOLDG:X×XX

Proof

Step Hyp Ref Expression
1 hladdf.1 X=BaseSetU
2 hladdf.2 G=+vU
3 hlnv UCHilOLDUNrmCVec
4 1 2 nvgf UNrmCVecG:X×XX
5 3 4 syl UCHilOLDG:X×XX