This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nvsass

Description: Associative law for the scalar product of a normed complex vector space. (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	nvscl.1	\|- X = ( BaseSet ` U )
		nvscl.4	\|- S = ( .sOLD ` U )
	Assertion	nvsass	\|- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. CC /\ C e. X ) ) -> ( ( A x. B ) S C ) = ( A S ( B S C ) ) )

Proof

Step	Hyp	Ref	Expression
1		nvscl.1	\|- X = ( BaseSet ` U )
2		nvscl.4	\|- S = ( .sOLD ` U )
3		eqid	\|- ( 1st ` U ) = ( 1st ` U )
4	3	nvvc	\|- ( U e. NrmCVec -> ( 1st ` U ) e. CVecOLD )
5		eqid	\|- ( +v ` U ) = ( +v ` U )
6	5	vafval	\|- ( +v ` U ) = ( 1st ` ( 1st ` U ) )
7	2	smfval	\|- S = ( 2nd ` ( 1st ` U ) )
8	1 5	bafval	\|- X = ran ( +v ` U )
9	6 7 8	vcass	\|- ( ( ( 1st ` U ) e. CVecOLD /\ ( A e. CC /\ B e. CC /\ C e. X ) ) -> ( ( A x. B ) S C ) = ( A S ( B S C ) ) )
10	4 9	sylan	\|- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. CC /\ C e. X ) ) -> ( ( A x. B ) S C ) = ( A S ( B S C ) ) )