Theorem hvadd4i

Description: Hilbert vector space addition law. (Contributed by NM, 3-Sep-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hvass.1	|- A e. ~H
	hvass.2	|- B e. ~H
	hvass.3	|- C e. ~H
	hvadd4.4	|- D e. ~H
Assertion	hvadd4i	|- ( ( A +h B ) +h ( C +h D ) ) = ( ( A +h C ) +h ( B +h D ) )

Proof

Step	Hyp	Ref	Expression
1		hvass.1	|- A e. ~H
2		hvass.2	|- B e. ~H
3		hvass.3	|- C e. ~H
4		hvadd4.4	|- D e. ~H
5		hvadd4	|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A +h B ) +h ( C +h D ) ) = ( ( A +h C ) +h ( B +h D ) ) )
6	1 2 3 4 5	mp4an	|- ( ( A +h B ) +h ( C +h D ) ) = ( ( A +h C ) +h ( B +h D ) )