Metamath Proof Explorer

Theorem nvscom

Description: Commutative law for the scalar product of a normed complex vector space. (Contributed by NM, 14-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses nvscl.1 
|- X = ( BaseSet ` U )
nvscl.4 
|- S = ( .sOLD ` U )
Assertion nvscom 
|- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. CC /\ C e. X ) ) -> ( A S ( B S C ) ) = ( B S ( A S C ) ) )

Proof

Step Hyp Ref Expression
1 nvscl.1 
 |-  X = ( BaseSet ` U )
2 nvscl.4 
 |-  S = ( .sOLD ` U )
3 mulcom 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
4 3 oveq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) S C ) = ( ( B x. A ) S C ) )
5 4 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. X ) -> ( ( A x. B ) S C ) = ( ( B x. A ) S C ) )
6 5 adantl 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ B e. CC /\ C e. X ) ) -> ( ( A x. B ) S C ) = ( ( B x. A ) S C ) )
7 1 2 nvsass 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ B e. CC /\ C e. X ) ) -> ( ( A x. B ) S C ) = ( A S ( B S C ) ) )
8 3ancoma 
 |-  ( ( A e. CC /\ B e. CC /\ C e. X ) <-> ( B e. CC /\ A e. CC /\ C e. X ) )
9 1 2 nvsass 
 |-  ( ( U e. NrmCVec /\ ( B e. CC /\ A e. CC /\ C e. X ) ) -> ( ( B x. A ) S C ) = ( B S ( A S C ) ) )
10 8 9 sylan2b 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ B e. CC /\ C e. X ) ) -> ( ( B x. A ) S C ) = ( B S ( A S C ) ) )
11 6 7 10 3eqtr3d 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ B e. CC /\ C e. X ) ) -> ( A S ( B S C ) ) = ( B S ( A S C ) ) )