Theorem nvnpcan

Description: Cancellation law for a normed complex vector space. (Contributed by NM, 24-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvpncan2.1	|- X = ( BaseSet ` U )
	nvpncan2.2	|- G = ( +v ` U )
	nvpncan2.3	|- M = ( -v ` U )
Assertion	nvnpcan	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A M B ) G B ) = A )

Proof

Step	Hyp	Ref	Expression
1		nvpncan2.1	|- X = ( BaseSet ` U )
2		nvpncan2.2	|- G = ( +v ` U )
3		nvpncan2.3	|- M = ( -v ` U )
4		simprl	|- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> A e. X )
5		simprr	|- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> B e. X )
6	4 5 5	3jca	|- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> ( A e. X /\ B e. X /\ B e. X ) )
7	1 2 3	nvaddsub	|- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X /\ B e. X ) ) -> ( ( A G B ) M B ) = ( ( A M B ) G B ) )
8	6 7	syldan	|- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> ( ( A G B ) M B ) = ( ( A M B ) G B ) )
9	8	3impb	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A G B ) M B ) = ( ( A M B ) G B ) )
10	1 2 3	nvpncan	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A G B ) M B ) = A )
11	9 10	eqtr3d	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A M B ) G B ) = A )