Theorem rrndsxmet

Description: D is an extended metric for the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	rrndsxmet.1	|- ( ph -> X e. Fin )
	rrndsxmet.2	|- D = ( f e. ( RR ^m X ) , g e. ( RR ^m X ) |-> ( sqrt ` sum_ k e. X ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) )
Assertion	rrndsxmet	|- ( ph -> D e. ( *Met ` ( RR ^m X ) ) )

Proof

Step	Hyp	Ref	Expression
1		rrndsxmet.1	|- ( ph -> X e. Fin )
2		rrndsxmet.2	|- D = ( f e. ( RR ^m X ) , g e. ( RR ^m X ) |-> ( sqrt ` sum_ k e. X ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) )
3	1 2	rrndsmet	|- ( ph -> D e. ( Met ` ( RR ^m X ) ) )
4		metxmet	|- ( D e. ( Met ` ( RR ^m X ) ) -> D e. ( *Met ` ( RR ^m X ) ) )
5	3 4	syl	|- ( ph -> D e. ( *Met ` ( RR ^m X ) ) )