Theorem hvpncan3

Description: Subtraction and addition of equal Hilbert space vectors. (Contributed by NM, 27-Aug-2004) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		hvaddsubass	|- ( ( A e. ~H /\ B e. ~H /\ A e. ~H ) -> ( ( A +h B ) -h A ) = ( A +h ( B -h A ) ) )
2	1	3anidm13	|- ( ( A e. ~H /\ B e. ~H ) -> ( ( A +h B ) -h A ) = ( A +h ( B -h A ) ) )
3		hvpncan2	|- ( ( A e. ~H /\ B e. ~H ) -> ( ( A +h B ) -h A ) = B )
4	2 3	eqtr3d	|- ( ( A e. ~H /\ B e. ~H ) -> ( A +h ( B -h A ) ) = B )