This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )