Metamath Proof Explorer

Theorem vcdir

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 vcdir 
|- ( ( W e. CVecOLD /\ ( A e. CC /\ B e. CC /\ C e. X ) ) -> ( ( A + B ) S C ) = ( ( A S C ) G ( 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 simpl 
 |-  ( ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) -> ( ( y + z ) S x ) = ( ( y S x ) G ( 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 + z ) S x ) = ( ( y S x ) G ( 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 + z ) S x ) = ( ( y S x ) G ( 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 + z ) S x ) = ( ( y S x ) G ( 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 + z ) S x ) = ( ( y S x ) G ( 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 + z ) S x ) = ( ( y S x ) G ( 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 + z ) S x ) = ( ( y S x ) G ( z S x ) ) )
12 4 11 syl 
 |-  ( W e. CVecOLD -> A. x e. X A. y e. CC A. z e. CC ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) )
13 oveq2 
 |-  ( x = C -> ( ( y + z ) S x ) = ( ( y + z ) S C ) )
14 oveq2 
 |-  ( x = C -> ( y S x ) = ( y S C ) )
15 oveq2 
 |-  ( x = C -> ( z S x ) = ( z S C ) )
16 14 15 oveq12d 
 |-  ( x = C -> ( ( y S x ) G ( z S x ) ) = ( ( y S C ) G ( z S C ) ) )
17 13 16 eqeq12d 
 |-  ( x = C -> ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) <-> ( ( y + z ) S C ) = ( ( y S C ) G ( z S C ) ) ) )
18 oveq1 
 |-  ( y = A -> ( y + z ) = ( A + z ) )
19 18 oveq1d 
 |-  ( y = A -> ( ( y + z ) S C ) = ( ( A + z ) S C ) )
20 oveq1 
 |-  ( y = A -> ( y S C ) = ( A S C ) )
21 20 oveq1d 
 |-  ( y = A -> ( ( y S C ) G ( z S C ) ) = ( ( A S C ) G ( z S C ) ) )
22 19 21 eqeq12d 
 |-  ( y = A -> ( ( ( y + z ) S C ) = ( ( y S C ) G ( z S C ) ) <-> ( ( A + z ) S C ) = ( ( A S C ) G ( z S C ) ) ) )
23 oveq2 
 |-  ( z = B -> ( A + z ) = ( A + B ) )
24 23 oveq1d 
 |-  ( z = B -> ( ( A + z ) S C ) = ( ( A + B ) S C ) )
25 oveq1 
 |-  ( z = B -> ( z S C ) = ( B S C ) )
26 25 oveq2d 
 |-  ( z = B -> ( ( A S C ) G ( z S C ) ) = ( ( A S C ) G ( B S C ) ) )
27 24 26 eqeq12d 
 |-  ( z = B -> ( ( ( A + z ) S C ) = ( ( A S C ) G ( z S C ) ) <-> ( ( A + B ) S C ) = ( ( A S C ) G ( B S C ) ) ) )
28 17 22 27 rspc3v 
 |-  ( ( C e. X /\ A e. CC /\ B e. CC ) -> ( A. x e. X A. y e. CC A. z e. CC ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) -> ( ( A + B ) S C ) = ( ( A S C ) G ( B S C ) ) ) )
29 12 28 syl5 
 |-  ( ( C e. X /\ A e. CC /\ B e. CC ) -> ( W e. CVecOLD -> ( ( A + B ) S C ) = ( ( A S C ) G ( B S C ) ) ) )
30 29 3coml 
 |-  ( ( A e. CC /\ B e. CC /\ C e. X ) -> ( W e. CVecOLD -> ( ( A + B ) S C ) = ( ( A S C ) G ( B S C ) ) ) )
31 30 impcom 
 |-  ( ( W e. CVecOLD /\ ( A e. CC /\ B e. CC /\ C e. X ) ) -> ( ( A + B ) S C ) = ( ( A S C ) G ( B S C ) ) )