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 = ( BaseSet ` U )
	hladdf.2	|- G = ( +v ` U )
Assertion	hladdf	|- ( U e. CHilOLD -> G : ( X X. X ) --> X )

Proof

Step	Hyp	Ref	Expression
1		hladdf.1	|- X = ( BaseSet ` U )
2		hladdf.2	|- G = ( +v ` U )
3		hlnv	|- ( U e. CHilOLD -> U e. NrmCVec )
4	1 2	nvgf	|- ( U e. NrmCVec -> G : ( X X. X ) --> X )
5	3 4	syl	|- ( U e. CHilOLD -> G : ( X X. X ) --> X )