Theorem nvdir

Description: Distributive law for the scalar product of a complex vector space. (Contributed by NM, 4-Dec-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvdi.1	|- X = ( BaseSet ` U )
	nvdi.2	|- G = ( +v ` U )
	nvdi.4	|- S = ( .sOLD ` U )
Assertion	nvdir	|- ( ( U e. NrmCVec /\ ( 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		nvdi.1	|- X = ( BaseSet ` U )
2		nvdi.2	|- G = ( +v ` U )
3		nvdi.4	|- S = ( .sOLD ` U )
4		eqid	|- ( 1st ` U ) = ( 1st ` U )
5	4	nvvc	|- ( U e. NrmCVec -> ( 1st ` U ) e. CVecOLD )
6	2	vafval	|- G = ( 1st ` ( 1st ` U ) )
7	3	smfval	|- S = ( 2nd ` ( 1st ` U ) )
8	1 2	bafval	|- X = ran G
9	6 7 8	vcdir	|- ( ( ( 1st ` U ) e. CVecOLD /\ ( A e. CC /\ B e. CC /\ C e. X ) ) -> ( ( A + B ) S C ) = ( ( A S C ) G ( B S C ) ) )
10	5 9	sylan	|- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. CC /\ C e. X ) ) -> ( ( A + B ) S C ) = ( ( A S C ) G ( B S C ) ) )