Step |
Hyp |
Ref |
Expression |
1 |
|
dv11cn.x |
|- X = ( A ( ball ` ( abs o. - ) ) R ) |
2 |
|
dv11cn.a |
|- ( ph -> A e. CC ) |
3 |
|
dv11cn.r |
|- ( ph -> R e. RR* ) |
4 |
|
dv11cn.f |
|- ( ph -> F : X --> CC ) |
5 |
|
dv11cn.g |
|- ( ph -> G : X --> CC ) |
6 |
|
dv11cn.d |
|- ( ph -> dom ( CC _D F ) = X ) |
7 |
|
dv11cn.e |
|- ( ph -> ( CC _D F ) = ( CC _D G ) ) |
8 |
|
dv11cn.c |
|- ( ph -> C e. X ) |
9 |
|
dv11cn.p |
|- ( ph -> ( F ` C ) = ( G ` C ) ) |
10 |
4
|
ffnd |
|- ( ph -> F Fn X ) |
11 |
5
|
ffnd |
|- ( ph -> G Fn X ) |
12 |
1
|
ovexi |
|- X e. _V |
13 |
12
|
a1i |
|- ( ph -> X e. _V ) |
14 |
|
inidm |
|- ( X i^i X ) = X |
15 |
10 11 13 13 14
|
offn |
|- ( ph -> ( F oF - G ) Fn X ) |
16 |
|
0cn |
|- 0 e. CC |
17 |
|
fnconstg |
|- ( 0 e. CC -> ( X X. { 0 } ) Fn X ) |
18 |
16 17
|
mp1i |
|- ( ph -> ( X X. { 0 } ) Fn X ) |
19 |
|
subcl |
|- ( ( x e. CC /\ y e. CC ) -> ( x - y ) e. CC ) |
20 |
19
|
adantl |
|- ( ( ph /\ ( x e. CC /\ y e. CC ) ) -> ( x - y ) e. CC ) |
21 |
20 4 5 13 13 14
|
off |
|- ( ph -> ( F oF - G ) : X --> CC ) |
22 |
21
|
ffvelrnda |
|- ( ( ph /\ x e. X ) -> ( ( F oF - G ) ` x ) e. CC ) |
23 |
8
|
anim1ci |
|- ( ( ph /\ x e. X ) -> ( x e. X /\ C e. X ) ) |
24 |
|
cnxmet |
|- ( abs o. - ) e. ( *Met ` CC ) |
25 |
|
blssm |
|- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ A e. CC /\ R e. RR* ) -> ( A ( ball ` ( abs o. - ) ) R ) C_ CC ) |
26 |
24 2 3 25
|
mp3an2i |
|- ( ph -> ( A ( ball ` ( abs o. - ) ) R ) C_ CC ) |
27 |
1 26
|
eqsstrid |
|- ( ph -> X C_ CC ) |
28 |
4
|
ffvelrnda |
|- ( ( ph /\ x e. X ) -> ( F ` x ) e. CC ) |
29 |
5
|
ffvelrnda |
|- ( ( ph /\ x e. X ) -> ( G ` x ) e. CC ) |
30 |
4
|
feqmptd |
|- ( ph -> F = ( x e. X |-> ( F ` x ) ) ) |
31 |
5
|
feqmptd |
|- ( ph -> G = ( x e. X |-> ( G ` x ) ) ) |
32 |
13 28 29 30 31
|
offval2 |
|- ( ph -> ( F oF - G ) = ( x e. X |-> ( ( F ` x ) - ( G ` x ) ) ) ) |
33 |
32
|
oveq2d |
|- ( ph -> ( CC _D ( F oF - G ) ) = ( CC _D ( x e. X |-> ( ( F ` x ) - ( G ` x ) ) ) ) ) |
34 |
|
cnelprrecn |
|- CC e. { RR , CC } |
35 |
34
|
a1i |
|- ( ph -> CC e. { RR , CC } ) |
36 |
|
fvexd |
|- ( ( ph /\ x e. X ) -> ( ( CC _D F ) ` x ) e. _V ) |
37 |
30
|
oveq2d |
|- ( ph -> ( CC _D F ) = ( CC _D ( x e. X |-> ( F ` x ) ) ) ) |
38 |
|
dvfcn |
|- ( CC _D F ) : dom ( CC _D F ) --> CC |
39 |
6
|
feq2d |
|- ( ph -> ( ( CC _D F ) : dom ( CC _D F ) --> CC <-> ( CC _D F ) : X --> CC ) ) |
40 |
38 39
|
mpbii |
|- ( ph -> ( CC _D F ) : X --> CC ) |
41 |
40
|
feqmptd |
|- ( ph -> ( CC _D F ) = ( x e. X |-> ( ( CC _D F ) ` x ) ) ) |
42 |
37 41
|
eqtr3d |
|- ( ph -> ( CC _D ( x e. X |-> ( F ` x ) ) ) = ( x e. X |-> ( ( CC _D F ) ` x ) ) ) |
43 |
31
|
oveq2d |
|- ( ph -> ( CC _D G ) = ( CC _D ( x e. X |-> ( G ` x ) ) ) ) |
44 |
7 41 43
|
3eqtr3rd |
|- ( ph -> ( CC _D ( x e. X |-> ( G ` x ) ) ) = ( x e. X |-> ( ( CC _D F ) ` x ) ) ) |
45 |
35 28 36 42 29 36 44
|
dvmptsub |
|- ( ph -> ( CC _D ( x e. X |-> ( ( F ` x ) - ( G ` x ) ) ) ) = ( x e. X |-> ( ( ( CC _D F ) ` x ) - ( ( CC _D F ) ` x ) ) ) ) |
46 |
40
|
ffvelrnda |
|- ( ( ph /\ x e. X ) -> ( ( CC _D F ) ` x ) e. CC ) |
47 |
46
|
subidd |
|- ( ( ph /\ x e. X ) -> ( ( ( CC _D F ) ` x ) - ( ( CC _D F ) ` x ) ) = 0 ) |
48 |
47
|
mpteq2dva |
|- ( ph -> ( x e. X |-> ( ( ( CC _D F ) ` x ) - ( ( CC _D F ) ` x ) ) ) = ( x e. X |-> 0 ) ) |
49 |
|
fconstmpt |
|- ( X X. { 0 } ) = ( x e. X |-> 0 ) |
50 |
48 49
|
eqtr4di |
|- ( ph -> ( x e. X |-> ( ( ( CC _D F ) ` x ) - ( ( CC _D F ) ` x ) ) ) = ( X X. { 0 } ) ) |
51 |
33 45 50
|
3eqtrd |
|- ( ph -> ( CC _D ( F oF - G ) ) = ( X X. { 0 } ) ) |
52 |
51
|
dmeqd |
|- ( ph -> dom ( CC _D ( F oF - G ) ) = dom ( X X. { 0 } ) ) |
53 |
|
snnzg |
|- ( 0 e. CC -> { 0 } =/= (/) ) |
54 |
|
dmxp |
|- ( { 0 } =/= (/) -> dom ( X X. { 0 } ) = X ) |
55 |
16 53 54
|
mp2b |
|- dom ( X X. { 0 } ) = X |
56 |
52 55
|
eqtrdi |
|- ( ph -> dom ( CC _D ( F oF - G ) ) = X ) |
57 |
|
eqimss2 |
|- ( dom ( CC _D ( F oF - G ) ) = X -> X C_ dom ( CC _D ( F oF - G ) ) ) |
58 |
56 57
|
syl |
|- ( ph -> X C_ dom ( CC _D ( F oF - G ) ) ) |
59 |
|
0red |
|- ( ph -> 0 e. RR ) |
60 |
51
|
fveq1d |
|- ( ph -> ( ( CC _D ( F oF - G ) ) ` x ) = ( ( X X. { 0 } ) ` x ) ) |
61 |
|
c0ex |
|- 0 e. _V |
62 |
61
|
fvconst2 |
|- ( x e. X -> ( ( X X. { 0 } ) ` x ) = 0 ) |
63 |
60 62
|
sylan9eq |
|- ( ( ph /\ x e. X ) -> ( ( CC _D ( F oF - G ) ) ` x ) = 0 ) |
64 |
63
|
abs00bd |
|- ( ( ph /\ x e. X ) -> ( abs ` ( ( CC _D ( F oF - G ) ) ` x ) ) = 0 ) |
65 |
|
0le0 |
|- 0 <_ 0 |
66 |
64 65
|
eqbrtrdi |
|- ( ( ph /\ x e. X ) -> ( abs ` ( ( CC _D ( F oF - G ) ) ` x ) ) <_ 0 ) |
67 |
27 21 2 3 1 58 59 66
|
dvlipcn |
|- ( ( ph /\ ( x e. X /\ C e. X ) ) -> ( abs ` ( ( ( F oF - G ) ` x ) - ( ( F oF - G ) ` C ) ) ) <_ ( 0 x. ( abs ` ( x - C ) ) ) ) |
68 |
23 67
|
syldan |
|- ( ( ph /\ x e. X ) -> ( abs ` ( ( ( F oF - G ) ` x ) - ( ( F oF - G ) ` C ) ) ) <_ ( 0 x. ( abs ` ( x - C ) ) ) ) |
69 |
32
|
fveq1d |
|- ( ph -> ( ( F oF - G ) ` C ) = ( ( x e. X |-> ( ( F ` x ) - ( G ` x ) ) ) ` C ) ) |
70 |
|
fveq2 |
|- ( x = C -> ( F ` x ) = ( F ` C ) ) |
71 |
|
fveq2 |
|- ( x = C -> ( G ` x ) = ( G ` C ) ) |
72 |
70 71
|
oveq12d |
|- ( x = C -> ( ( F ` x ) - ( G ` x ) ) = ( ( F ` C ) - ( G ` C ) ) ) |
73 |
|
eqid |
|- ( x e. X |-> ( ( F ` x ) - ( G ` x ) ) ) = ( x e. X |-> ( ( F ` x ) - ( G ` x ) ) ) |
74 |
|
ovex |
|- ( ( F ` C ) - ( G ` C ) ) e. _V |
75 |
72 73 74
|
fvmpt |
|- ( C e. X -> ( ( x e. X |-> ( ( F ` x ) - ( G ` x ) ) ) ` C ) = ( ( F ` C ) - ( G ` C ) ) ) |
76 |
8 75
|
syl |
|- ( ph -> ( ( x e. X |-> ( ( F ` x ) - ( G ` x ) ) ) ` C ) = ( ( F ` C ) - ( G ` C ) ) ) |
77 |
4 8
|
ffvelrnd |
|- ( ph -> ( F ` C ) e. CC ) |
78 |
77 9
|
subeq0bd |
|- ( ph -> ( ( F ` C ) - ( G ` C ) ) = 0 ) |
79 |
69 76 78
|
3eqtrd |
|- ( ph -> ( ( F oF - G ) ` C ) = 0 ) |
80 |
79
|
adantr |
|- ( ( ph /\ x e. X ) -> ( ( F oF - G ) ` C ) = 0 ) |
81 |
80
|
oveq2d |
|- ( ( ph /\ x e. X ) -> ( ( ( F oF - G ) ` x ) - ( ( F oF - G ) ` C ) ) = ( ( ( F oF - G ) ` x ) - 0 ) ) |
82 |
22
|
subid1d |
|- ( ( ph /\ x e. X ) -> ( ( ( F oF - G ) ` x ) - 0 ) = ( ( F oF - G ) ` x ) ) |
83 |
81 82
|
eqtrd |
|- ( ( ph /\ x e. X ) -> ( ( ( F oF - G ) ` x ) - ( ( F oF - G ) ` C ) ) = ( ( F oF - G ) ` x ) ) |
84 |
83
|
fveq2d |
|- ( ( ph /\ x e. X ) -> ( abs ` ( ( ( F oF - G ) ` x ) - ( ( F oF - G ) ` C ) ) ) = ( abs ` ( ( F oF - G ) ` x ) ) ) |
85 |
27
|
sselda |
|- ( ( ph /\ x e. X ) -> x e. CC ) |
86 |
27 8
|
sseldd |
|- ( ph -> C e. CC ) |
87 |
86
|
adantr |
|- ( ( ph /\ x e. X ) -> C e. CC ) |
88 |
85 87
|
subcld |
|- ( ( ph /\ x e. X ) -> ( x - C ) e. CC ) |
89 |
88
|
abscld |
|- ( ( ph /\ x e. X ) -> ( abs ` ( x - C ) ) e. RR ) |
90 |
89
|
recnd |
|- ( ( ph /\ x e. X ) -> ( abs ` ( x - C ) ) e. CC ) |
91 |
90
|
mul02d |
|- ( ( ph /\ x e. X ) -> ( 0 x. ( abs ` ( x - C ) ) ) = 0 ) |
92 |
68 84 91
|
3brtr3d |
|- ( ( ph /\ x e. X ) -> ( abs ` ( ( F oF - G ) ` x ) ) <_ 0 ) |
93 |
22
|
absge0d |
|- ( ( ph /\ x e. X ) -> 0 <_ ( abs ` ( ( F oF - G ) ` x ) ) ) |
94 |
22
|
abscld |
|- ( ( ph /\ x e. X ) -> ( abs ` ( ( F oF - G ) ` x ) ) e. RR ) |
95 |
|
0re |
|- 0 e. RR |
96 |
|
letri3 |
|- ( ( ( abs ` ( ( F oF - G ) ` x ) ) e. RR /\ 0 e. RR ) -> ( ( abs ` ( ( F oF - G ) ` x ) ) = 0 <-> ( ( abs ` ( ( F oF - G ) ` x ) ) <_ 0 /\ 0 <_ ( abs ` ( ( F oF - G ) ` x ) ) ) ) ) |
97 |
94 95 96
|
sylancl |
|- ( ( ph /\ x e. X ) -> ( ( abs ` ( ( F oF - G ) ` x ) ) = 0 <-> ( ( abs ` ( ( F oF - G ) ` x ) ) <_ 0 /\ 0 <_ ( abs ` ( ( F oF - G ) ` x ) ) ) ) ) |
98 |
92 93 97
|
mpbir2and |
|- ( ( ph /\ x e. X ) -> ( abs ` ( ( F oF - G ) ` x ) ) = 0 ) |
99 |
22 98
|
abs00d |
|- ( ( ph /\ x e. X ) -> ( ( F oF - G ) ` x ) = 0 ) |
100 |
62
|
adantl |
|- ( ( ph /\ x e. X ) -> ( ( X X. { 0 } ) ` x ) = 0 ) |
101 |
99 100
|
eqtr4d |
|- ( ( ph /\ x e. X ) -> ( ( F oF - G ) ` x ) = ( ( X X. { 0 } ) ` x ) ) |
102 |
15 18 101
|
eqfnfvd |
|- ( ph -> ( F oF - G ) = ( X X. { 0 } ) ) |
103 |
|
ofsubeq0 |
|- ( ( X e. _V /\ F : X --> CC /\ G : X --> CC ) -> ( ( F oF - G ) = ( X X. { 0 } ) <-> F = G ) ) |
104 |
12 4 5 103
|
mp3an2i |
|- ( ph -> ( ( F oF - G ) = ( X X. { 0 } ) <-> F = G ) ) |
105 |
102 104
|
mpbid |
|- ( ph -> F = G ) |