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

Metamath Proof Explorer

Theorem imsdval2

Description: Value of the distance function of the induced metric of a normed complex vector space. Equation 1 of Kreyszig p. 59. (Contributed by NM, 28-Nov-2006) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	imsdval2.1	\|- X = ( BaseSet ` U )
		imsdval2.2	\|- G = ( +v ` U )
		imsdval2.4	\|- S = ( .sOLD ` U )
		imsdval2.6	\|- N = ( normCV ` U )
		imsdval2.8	\|- D = ( IndMet ` U )
	Assertion	imsdval2	\|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A D B ) = ( N ` ( A G ( -u 1 S B ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		imsdval2.1	\|- X = ( BaseSet ` U )
2		imsdval2.2	\|- G = ( +v ` U )
3		imsdval2.4	\|- S = ( .sOLD ` U )
4		imsdval2.6	\|- N = ( normCV ` U )
5		imsdval2.8	\|- D = ( IndMet ` U )
6		eqid	\|- ( -v ` U ) = ( -v ` U )
7	1 6 4 5	imsdval	\|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A D B ) = ( N ` ( A ( -v ` U ) B ) ) )
8	1 2 3 6	nvmval	\|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A ( -v ` U ) B ) = ( A G ( -u 1 S B ) ) )
9	8	fveq2d	\|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A ( -v ` U ) B ) ) = ( N ` ( A G ( -u 1 S B ) ) ) )
10	7 9	eqtrd	\|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A D B ) = ( N ` ( A G ( -u 1 S B ) ) ) )