nmfval

Description: The value of the norm function as the distance to zero. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	nmfval.n	\|- N = ( norm ` W )
	nmfval.x	\|- X = ( Base ` W )
	nmfval.z	\|- .0. = ( 0g ` W )
	nmfval.d	\|- D = ( dist ` W )
Assertion	nmfval	\|- N = ( x e. X \|-> ( x D .0. ) )

Proof

Step	Hyp	Ref	Expression
1		nmfval.n	\|- N = ( norm ` W )
2		nmfval.x	\|- X = ( Base ` W )
3		nmfval.z	\|- .0. = ( 0g ` W )
4		nmfval.d	\|- D = ( dist ` W )
5		fveq2	\|- ( w = W -> ( Base ` w ) = ( Base ` W ) )
6	5 2	eqtr4di	\|- ( w = W -> ( Base ` w ) = X )
7		fveq2	\|- ( w = W -> ( dist ` w ) = ( dist ` W ) )
8	7 4	eqtr4di	\|- ( w = W -> ( dist ` w ) = D )
9		eqidd	\|- ( w = W -> x = x )
10		fveq2	\|- ( w = W -> ( 0g ` w ) = ( 0g ` W ) )
11	10 3	eqtr4di	\|- ( w = W -> ( 0g ` w ) = .0. )
12	8 9 11	oveq123d	\|- ( w = W -> ( x ( dist ` w ) ( 0g ` w ) ) = ( x D .0. ) )
13	6 12	mpteq12dv	\|- ( w = W -> ( x e. ( Base ` w ) \|-> ( x ( dist ` w ) ( 0g ` w ) ) ) = ( x e. X \|-> ( x D .0. ) ) )
14		df-nm	\|- norm = ( w e. _V \|-> ( x e. ( Base ` w ) \|-> ( x ( dist ` w ) ( 0g ` w ) ) ) )
15		eqid	\|- ( x e. X \|-> ( x D .0. ) ) = ( x e. X \|-> ( x D .0. ) )
16		df-ov	\|- ( x D .0. ) = ( D ` <. x , .0. >. )
17		fvrn0	\|- ( D ` <. x , .0. >. ) e. ( ran D u. { (/) } )
18	16 17	eqeltri	\|- ( x D .0. ) e. ( ran D u. { (/) } )
19	18	a1i	\|- ( x e. X -> ( x D .0. ) e. ( ran D u. { (/) } ) )
20	15 19	fmpti	\|- ( x e. X \|-> ( x D .0. ) ) : X --> ( ran D u. { (/) } )
21	2	fvexi	\|- X e. _V
22	4	fvexi	\|- D e. _V
23	22	rnex	\|- ran D e. _V
24		p0ex	\|- { (/) } e. _V
25	23 24	unex	\|- ( ran D u. { (/) } ) e. _V
26		fex2	\|- ( ( ( x e. X \|-> ( x D .0. ) ) : X --> ( ran D u. { (/) } ) /\ X e. _V /\ ( ran D u. { (/) } ) e. _V ) -> ( x e. X \|-> ( x D .0. ) ) e. _V )
27	20 21 25 26	mp3an	\|- ( x e. X \|-> ( x D .0. ) ) e. _V
28	13 14 27	fvmpt	\|- ( W e. _V -> ( norm ` W ) = ( x e. X \|-> ( x D .0. ) ) )
29		fvprc	\|- ( -. W e. _V -> ( norm ` W ) = (/) )
30		mpt0	\|- ( x e. (/) \|-> ( x D .0. ) ) = (/)
31	29 30	eqtr4di	\|- ( -. W e. _V -> ( norm ` W ) = ( x e. (/) \|-> ( x D .0. ) ) )
32		fvprc	\|- ( -. W e. _V -> ( Base ` W ) = (/) )
33	2 32	eqtrid	\|- ( -. W e. _V -> X = (/) )
34	33	mpteq1d	\|- ( -. W e. _V -> ( x e. X \|-> ( x D .0. ) ) = ( x e. (/) \|-> ( x D .0. ) ) )
35	31 34	eqtr4d	\|- ( -. W e. _V -> ( norm ` W ) = ( x e. X \|-> ( x D .0. ) ) )
36	28 35	pm2.61i	\|- ( norm ` W ) = ( x e. X \|-> ( x D .0. ) )
37	1 36	eqtri	\|- N = ( x e. X \|-> ( x D .0. ) )

Metamath Proof Explorer

Theorem nmfval

Proof