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 = 1 st W
vciOLD.2 S = 2 nd W
vciOLD.3 X = ran G
Assertion vcdir W CVec OLD A B C X A + B S C = A S C G B S C

Proof

Step Hyp Ref Expression
1 vciOLD.1 G = 1 st W
2 vciOLD.2 S = 2 nd W
3 vciOLD.3 X = ran G
4 1 2 3 vciOLD W CVec OLD G AbelOp S : × X X x X 1 S x = x y z X y S x G z = y S x G y S z z y + z S x = y S x G z S x y z S x = y S z S x
5 simpl y + z S x = y S x G z S x y z S x = y S z S x y + z S x = y S x G z S x
6 5 ralimi z y + z S x = y S x G z S x y z S x = y S z S x z y + z S x = y S x G z S x
7 6 adantl z X y S x G z = y S x G y S z z y + z S x = y S x G z S x y z S x = y S z S x z y + z S x = y S x G z S x
8 7 ralimi y z X y S x G z = y S x G y S z z y + z S x = y S x G z S x y z S x = y S z S x y z y + z S x = y S x G z S x
9 8 adantl 1 S x = x y z X y S x G z = y S x G y S z z y + z S x = y S x G z S x y z S x = y S z S x y z y + z S x = y S x G z S x
10 9 ralimi x X 1 S x = x y z X y S x G z = y S x G y S z z y + z S x = y S x G z S x y z S x = y S z S x x X y z y + z S x = y S x G z S x
11 10 3ad2ant3 G AbelOp S : × X X x X 1 S x = x y z X y S x G z = y S x G y S z z y + z S x = y S x G z S x y z S x = y S z S x x X y z y + z S x = y S x G z S x
12 4 11 syl W CVec OLD x X y z 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 X A B x X y z 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 X A B W CVec OLD A + B S C = A S C G B S C
30 29 3coml A B C X W CVec OLD A + B S C = A S C G B S C
31 30 impcom W CVec OLD A B C X A + B S C = A S C G B S C