Metamath Proof Explorer

Theorem vcdi

Description: Distributive 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 vcdi 
|- ( ( W e. CVecOLD /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( A S ( B G C ) ) = ( ( A S B ) G ( A 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 simpl 
 |-  ( ( 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. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) )
6 5 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. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) )
7 6 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. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) )
8 7 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. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) )
9 8 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. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) )
10 4 9 syl 
 |-  ( W e. CVecOLD -> A. x e. X A. y e. CC A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) )
11 oveq1 
 |-  ( x = B -> ( x G z ) = ( B G z ) )
12 11 oveq2d 
 |-  ( x = B -> ( y S ( x G z ) ) = ( y S ( B G z ) ) )
13 oveq2 
 |-  ( x = B -> ( y S x ) = ( y S B ) )
14 13 oveq1d 
 |-  ( x = B -> ( ( y S x ) G ( y S z ) ) = ( ( y S B ) G ( y S z ) ) )
15 12 14 eqeq12d 
 |-  ( x = B -> ( ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) <-> ( y S ( B G z ) ) = ( ( y S B ) G ( y S z ) ) ) )
16 oveq1 
 |-  ( y = A -> ( y S ( B G z ) ) = ( A S ( B G z ) ) )
17 oveq1 
 |-  ( y = A -> ( y S B ) = ( A S B ) )
18 oveq1 
 |-  ( y = A -> ( y S z ) = ( A S z ) )
19 17 18 oveq12d 
 |-  ( y = A -> ( ( y S B ) G ( y S z ) ) = ( ( A S B ) G ( A S z ) ) )
20 16 19 eqeq12d 
 |-  ( y = A -> ( ( y S ( B G z ) ) = ( ( y S B ) G ( y S z ) ) <-> ( A S ( B G z ) ) = ( ( A S B ) G ( A S z ) ) ) )
21 oveq2 
 |-  ( z = C -> ( B G z ) = ( B G C ) )
22 21 oveq2d 
 |-  ( z = C -> ( A S ( B G z ) ) = ( A S ( B G C ) ) )
23 oveq2 
 |-  ( z = C -> ( A S z ) = ( A S C ) )
24 23 oveq2d 
 |-  ( z = C -> ( ( A S B ) G ( A S z ) ) = ( ( A S B ) G ( A S C ) ) )
25 22 24 eqeq12d 
 |-  ( z = C -> ( ( A S ( B G z ) ) = ( ( A S B ) G ( A S z ) ) <-> ( A S ( B G C ) ) = ( ( A S B ) G ( A S C ) ) ) )
26 15 20 25 rspc3v 
 |-  ( ( B e. X /\ A e. CC /\ C e. X ) -> ( A. x e. X A. y e. CC A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) -> ( A S ( B G C ) ) = ( ( A S B ) G ( A S C ) ) ) )
27 10 26 syl5 
 |-  ( ( B e. X /\ A e. CC /\ C e. X ) -> ( W e. CVecOLD -> ( A S ( B G C ) ) = ( ( A S B ) G ( A S C ) ) ) )
28 27 3com12 
 |-  ( ( A e. CC /\ B e. X /\ C e. X ) -> ( W e. CVecOLD -> ( A S ( B G C ) ) = ( ( A S B ) G ( A S C ) ) ) )
29 28 impcom 
 |-  ( ( W e. CVecOLD /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( A S ( B G C ) ) = ( ( A S B ) G ( A S C ) ) )