Theorem hlcom

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

	Ref	Expression
Hypotheses	hladdf.1	|- X = ( BaseSet ` U )
	hladdf.2	|- G = ( +v ` U )
Assertion	hlcom	|- ( ( U e. CHilOLD /\ A e. X /\ B e. X ) -> ( A G B ) = ( B G A ) )

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	nvcom	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G B ) = ( B G A ) )
5	3 4	syl3an1	|- ( ( U e. CHilOLD /\ A e. X /\ B e. X ) -> ( A G B ) = ( B G A ) )