Theorem ncvspds

Description: Value of the distance function in terms of the norm of a normed subcomplex vector space. Equation 1 of Kreyszig p. 59. (Contributed by NM, 28-Nov-2006) (Revised by AV, 13-Oct-2021)

	Ref	Expression
Hypotheses	ncvspds.n	|- N = ( norm ` G )
	ncvspds.x	|- X = ( Base ` G )
	ncvspds.p	|- .+ = ( +g ` G )
	ncvspds.d	|- D = ( dist ` G )
	ncvspds.s	|- .x. = ( .s ` G )
Assertion	ncvspds	|- ( ( G e. ( NrmVec i^i CVec ) /\ A e. X /\ B e. X ) -> ( A D B ) = ( N ` ( A .+ ( -u 1 .x. B ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ncvspds.n	|- N = ( norm ` G )
2		ncvspds.x	|- X = ( Base ` G )
3		ncvspds.p	|- .+ = ( +g ` G )
4		ncvspds.d	|- D = ( dist ` G )
5		ncvspds.s	|- .x. = ( .s ` G )
6		elin	|- ( G e. ( NrmVec i^i CVec ) <-> ( G e. NrmVec /\ G e. CVec ) )
7		nvcnlm	|- ( G e. NrmVec -> G e. NrmMod )
8		nlmngp	|- ( G e. NrmMod -> G e. NrmGrp )
9	7 8	syl	|- ( G e. NrmVec -> G e. NrmGrp )
10	9	adantr	|- ( ( G e. NrmVec /\ G e. CVec ) -> G e. NrmGrp )
11	6 10	sylbi	|- ( G e. ( NrmVec i^i CVec ) -> G e. NrmGrp )
12		eqid	|- ( -g ` G ) = ( -g ` G )
13	1 2 12 4	ngpds	|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A D B ) = ( N ` ( A ( -g ` G ) B ) ) )
14	11 13	syl3an1	|- ( ( G e. ( NrmVec i^i CVec ) /\ A e. X /\ B e. X ) -> ( A D B ) = ( N ` ( A ( -g ` G ) B ) ) )
15		id	|- ( G e. CVec -> G e. CVec )
16	15	cvsclm	|- ( G e. CVec -> G e. CMod )
17	6 16	simplbiim	|- ( G e. ( NrmVec i^i CVec ) -> G e. CMod )
18		eqid	|- ( Scalar ` G ) = ( Scalar ` G )
19	2 3 12 18 5	clmvsubval	|- ( ( G e. CMod /\ A e. X /\ B e. X ) -> ( A ( -g ` G ) B ) = ( A .+ ( -u 1 .x. B ) ) )
20	17 19	syl3an1	|- ( ( G e. ( NrmVec i^i CVec ) /\ A e. X /\ B e. X ) -> ( A ( -g ` G ) B ) = ( A .+ ( -u 1 .x. B ) ) )
21	20	fveq2d	|- ( ( G e. ( NrmVec i^i CVec ) /\ A e. X /\ B e. X ) -> ( N ` ( A ( -g ` G ) B ) ) = ( N ` ( A .+ ( -u 1 .x. B ) ) ) )
22	14 21	eqtrd	|- ( ( G e. ( NrmVec i^i CVec ) /\ A e. X /\ B e. X ) -> ( A D B ) = ( N ` ( A .+ ( -u 1 .x. B ) ) ) )