Theorem hvpncan2

Description: Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	hvpncan2	|- ( ( A e. ~H /\ B e. ~H ) -> ( ( A +h B ) -h A ) = B )

Proof

Step	Hyp	Ref	Expression
1		ax-hvcom	|- ( ( B e. ~H /\ A e. ~H ) -> ( B +h A ) = ( A +h B ) )
2	1	oveq1d	|- ( ( B e. ~H /\ A e. ~H ) -> ( ( B +h A ) -h A ) = ( ( A +h B ) -h A ) )
3		hvpncan	|- ( ( B e. ~H /\ A e. ~H ) -> ( ( B +h A ) -h A ) = B )
4	2 3	eqtr3d	|- ( ( B e. ~H /\ A e. ~H ) -> ( ( A +h B ) -h A ) = B )
5	4	ancoms	|- ( ( A e. ~H /\ B e. ~H ) -> ( ( A +h B ) -h A ) = B )