Metamath Proof Explorer


Theorem ovolfsval

Description: The value of the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Hypothesis ovolfs.1 G=absF
Assertion ovolfsval F:2NGN=2ndFN1stFN

Proof

Step Hyp Ref Expression
1 ovolfs.1 G=absF
2 1 fveq1i GN=absFN
3 fvco3 F:2NabsFN=absFN
4 2 3 eqtrid F:2NGN=absFN
5 ffvelrn F:2NFN2
6 5 elin2d F:2NFN2
7 1st2nd2 FN2FN=1stFN2ndFN
8 6 7 syl F:2NFN=1stFN2ndFN
9 8 fveq2d F:2NabsFN=abs1stFN2ndFN
10 df-ov 1stFNabs2ndFN=abs1stFN2ndFN
11 9 10 eqtr4di F:2NabsFN=1stFNabs2ndFN
12 ovolfcl F:2N1stFN2ndFN1stFN2ndFN
13 12 simp1d F:2N1stFN
14 13 recnd F:2N1stFN
15 12 simp2d F:2N2ndFN
16 15 recnd F:2N2ndFN
17 eqid abs=abs
18 17 cnmetdval 1stFN2ndFN1stFNabs2ndFN=1stFN2ndFN
19 14 16 18 syl2anc F:2N1stFNabs2ndFN=1stFN2ndFN
20 abssuble0 1stFN2ndFN1stFN2ndFN1stFN2ndFN=2ndFN1stFN
21 12 20 syl F:2N1stFN2ndFN=2ndFN1stFN
22 19 21 eqtrd F:2N1stFNabs2ndFN=2ndFN1stFN
23 11 22 eqtrd F:2NabsFN=2ndFN1stFN
24 4 23 eqtrd F:2NGN=2ndFN1stFN