Step |
Hyp |
Ref |
Expression |
1 |
|
ovolfs.1 |
|- G = ( ( abs o. - ) o. F ) |
2 |
1
|
fveq1i |
|- ( G ` N ) = ( ( ( abs o. - ) o. F ) ` N ) |
3 |
|
fvco3 |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( ( ( abs o. - ) o. F ) ` N ) = ( ( abs o. - ) ` ( F ` N ) ) ) |
4 |
2 3
|
eqtrid |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( G ` N ) = ( ( abs o. - ) ` ( F ` N ) ) ) |
5 |
|
ffvelrn |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( F ` N ) e. ( <_ i^i ( RR X. RR ) ) ) |
6 |
5
|
elin2d |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( F ` N ) e. ( RR X. RR ) ) |
7 |
|
1st2nd2 |
|- ( ( F ` N ) e. ( RR X. RR ) -> ( F ` N ) = <. ( 1st ` ( F ` N ) ) , ( 2nd ` ( F ` N ) ) >. ) |
8 |
6 7
|
syl |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( F ` N ) = <. ( 1st ` ( F ` N ) ) , ( 2nd ` ( F ` N ) ) >. ) |
9 |
8
|
fveq2d |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( ( abs o. - ) ` ( F ` N ) ) = ( ( abs o. - ) ` <. ( 1st ` ( F ` N ) ) , ( 2nd ` ( F ` N ) ) >. ) ) |
10 |
|
df-ov |
|- ( ( 1st ` ( F ` N ) ) ( abs o. - ) ( 2nd ` ( F ` N ) ) ) = ( ( abs o. - ) ` <. ( 1st ` ( F ` N ) ) , ( 2nd ` ( F ` N ) ) >. ) |
11 |
9 10
|
eqtr4di |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( ( abs o. - ) ` ( F ` N ) ) = ( ( 1st ` ( F ` N ) ) ( abs o. - ) ( 2nd ` ( F ` N ) ) ) ) |
12 |
|
ovolfcl |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( ( 1st ` ( F ` N ) ) e. RR /\ ( 2nd ` ( F ` N ) ) e. RR /\ ( 1st ` ( F ` N ) ) <_ ( 2nd ` ( F ` N ) ) ) ) |
13 |
12
|
simp1d |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( 1st ` ( F ` N ) ) e. RR ) |
14 |
13
|
recnd |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( 1st ` ( F ` N ) ) e. CC ) |
15 |
12
|
simp2d |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( 2nd ` ( F ` N ) ) e. RR ) |
16 |
15
|
recnd |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( 2nd ` ( F ` N ) ) e. CC ) |
17 |
|
eqid |
|- ( abs o. - ) = ( abs o. - ) |
18 |
17
|
cnmetdval |
|- ( ( ( 1st ` ( F ` N ) ) e. CC /\ ( 2nd ` ( F ` N ) ) e. CC ) -> ( ( 1st ` ( F ` N ) ) ( abs o. - ) ( 2nd ` ( F ` N ) ) ) = ( abs ` ( ( 1st ` ( F ` N ) ) - ( 2nd ` ( F ` N ) ) ) ) ) |
19 |
14 16 18
|
syl2anc |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( ( 1st ` ( F ` N ) ) ( abs o. - ) ( 2nd ` ( F ` N ) ) ) = ( abs ` ( ( 1st ` ( F ` N ) ) - ( 2nd ` ( F ` N ) ) ) ) ) |
20 |
|
abssuble0 |
|- ( ( ( 1st ` ( F ` N ) ) e. RR /\ ( 2nd ` ( F ` N ) ) e. RR /\ ( 1st ` ( F ` N ) ) <_ ( 2nd ` ( F ` N ) ) ) -> ( abs ` ( ( 1st ` ( F ` N ) ) - ( 2nd ` ( F ` N ) ) ) ) = ( ( 2nd ` ( F ` N ) ) - ( 1st ` ( F ` N ) ) ) ) |
21 |
12 20
|
syl |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( abs ` ( ( 1st ` ( F ` N ) ) - ( 2nd ` ( F ` N ) ) ) ) = ( ( 2nd ` ( F ` N ) ) - ( 1st ` ( F ` N ) ) ) ) |
22 |
19 21
|
eqtrd |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( ( 1st ` ( F ` N ) ) ( abs o. - ) ( 2nd ` ( F ` N ) ) ) = ( ( 2nd ` ( F ` N ) ) - ( 1st ` ( F ` N ) ) ) ) |
23 |
11 22
|
eqtrd |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( ( abs o. - ) ` ( F ` N ) ) = ( ( 2nd ` ( F ` N ) ) - ( 1st ` ( F ` N ) ) ) ) |
24 |
4 23
|
eqtrd |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( G ` N ) = ( ( 2nd ` ( F ` N ) ) - ( 1st ` ( F ` N ) ) ) ) |