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 = 1 st W
vciOLD.2 S = 2 nd W
vciOLD.3 X = ran G
Assertion vcdi W CVec OLD A B X C X A S B G C = A S B G A 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 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 X y S x G z = y S x G y S z
6 5 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 X y S x G z = y S x G y S z
7 6 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 X y S x G z = y S x G y S z
8 7 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 X y S x G z = y S x G y S z
9 8 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 X y S x G z = y S x G y S z
10 4 9 syl W CVec OLD x X y z 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 X A C X x X y z 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 X A C X W CVec OLD A S B G C = A S B G A S C
28 27 3com12 A B X C X W CVec OLD A S B G C = A S B G A S C
29 28 impcom W CVec OLD A B X C X A S B G C = A S B G A S C