Metamath Proof Explorer

Theorem vcass

Description: Associative law for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses vciOLD.1 
|- G = ( 1st ` W )
vciOLD.2 
|- S = ( 2nd ` W )
vciOLD.3 
|- X = ran G
Assertion vcass 
|- ( ( W e. CVecOLD /\ ( A e. CC /\ B e. CC /\ C e. X ) ) -> ( ( A x. B ) S C ) = ( A S ( B S C ) ) )

Proof

Step Hyp Ref Expression
1 vciOLD.1 
 |-  G = ( 1st ` W )
2 vciOLD.2 
 |-  S = ( 2nd ` W )
3 vciOLD.3 
 |-  X = ran G
4 1 2 3 vciOLD 
 |-  ( W e. CVecOLD -> ( G e. AbelOp /\ S : ( CC X. X ) --> X /\ A. x e. X ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) ) )
5 simpr 
 |-  ( ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) -> ( ( y x. z ) S x ) = ( y S ( z S x ) ) )
6 5 ralimi 
 |-  ( A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) -> A. z e. CC ( ( y x. z ) S x ) = ( y S ( z S x ) ) )
7 6 adantl 
 |-  ( ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) -> A. z e. CC ( ( y x. z ) S x ) = ( y S ( z S x ) ) )
8 7 ralimi 
 |-  ( A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) -> A. y e. CC A. z e. CC ( ( y x. z ) S x ) = ( y S ( z S x ) ) )
9 8 adantl 
 |-  ( ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) -> A. y e. CC A. z e. CC ( ( y x. z ) S x ) = ( y S ( z S x ) ) )
10 9 ralimi 
 |-  ( A. x e. X ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) -> A. x e. X A. y e. CC A. z e. CC ( ( y x. z ) S x ) = ( y S ( z S x ) ) )
11 10 3ad2ant3 
 |-  ( ( G e. AbelOp /\ S : ( CC X. X ) --> X /\ A. x e. X ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) ) -> A. x e. X A. y e. CC A. z e. CC ( ( y x. z ) S x ) = ( y S ( z S x ) ) )
12 4 11 syl 
 |-  ( W e. CVecOLD -> A. x e. X A. y e. CC A. z e. CC ( ( y x. z ) S x ) = ( y S ( z S x ) ) )
13 oveq2 
 |-  ( x = C -> ( ( y x. z ) S x ) = ( ( y x. z ) S C ) )
14 oveq2 
 |-  ( x = C -> ( z S x ) = ( z S C ) )
15 14 oveq2d 
 |-  ( x = C -> ( y S ( z S x ) ) = ( y S ( z S C ) ) )
16 13 15 eqeq12d 
 |-  ( x = C -> ( ( ( y x. z ) S x ) = ( y S ( z S x ) ) <-> ( ( y x. z ) S C ) = ( y S ( z S C ) ) ) )
17 oveq1 
 |-  ( y = A -> ( y x. z ) = ( A x. z ) )
18 17 oveq1d 
 |-  ( y = A -> ( ( y x. z ) S C ) = ( ( A x. z ) S C ) )
19 oveq1 
 |-  ( y = A -> ( y S ( z S C ) ) = ( A S ( z S C ) ) )
20 18 19 eqeq12d 
 |-  ( y = A -> ( ( ( y x. z ) S C ) = ( y S ( z S C ) ) <-> ( ( A x. z ) S C ) = ( A S ( z S C ) ) ) )
21 oveq2 
 |-  ( z = B -> ( A x. z ) = ( A x. B ) )
22 21 oveq1d 
 |-  ( z = B -> ( ( A x. z ) S C ) = ( ( A x. B ) S C ) )
23 oveq1 
 |-  ( z = B -> ( z S C ) = ( B S C ) )
24 23 oveq2d 
 |-  ( z = B -> ( A S ( z S C ) ) = ( A S ( B S C ) ) )
25 22 24 eqeq12d 
 |-  ( z = B -> ( ( ( A x. z ) S C ) = ( A S ( z S C ) ) <-> ( ( A x. B ) S C ) = ( A S ( B S C ) ) ) )
26 16 20 25 rspc3v 
 |-  ( ( C e. X /\ A e. CC /\ B e. CC ) -> ( A. x e. X A. y e. CC A. z e. CC ( ( y x. z ) S x ) = ( y S ( z S x ) ) -> ( ( A x. B ) S C ) = ( A S ( B S C ) ) ) )
27 12 26 syl5 
 |-  ( ( C e. X /\ A e. CC /\ B e. CC ) -> ( W e. CVecOLD -> ( ( A x. B ) S C ) = ( A S ( B S C ) ) ) )
28 27 3coml 
 |-  ( ( A e. CC /\ B e. CC /\ C e. X ) -> ( W e. CVecOLD -> ( ( A x. B ) S C ) = ( A S ( B S C ) ) ) )
29 28 impcom 
 |-  ( ( W e. CVecOLD /\ ( A e. CC /\ B e. CC /\ C e. X ) ) -> ( ( A x. B ) S C ) = ( A S ( B S C ) ) )