Step |
Hyp |
Ref |
Expression |
1 |
|
simp2 |
|- ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> F : A --> CC ) |
2 |
1
|
ffnd |
|- ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> F Fn A ) |
3 |
|
simp3 |
|- ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> G : A --> CC ) |
4 |
3
|
ffnd |
|- ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> G Fn A ) |
5 |
|
simp1 |
|- ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> A e. V ) |
6 |
|
inidm |
|- ( A i^i A ) = A |
7 |
|
eqidd |
|- ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( F ` x ) = ( F ` x ) ) |
8 |
|
eqidd |
|- ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( G ` x ) = ( G ` x ) ) |
9 |
2 4 5 5 6 7 8
|
ofval |
|- ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( ( F oF - G ) ` x ) = ( ( F ` x ) - ( G ` x ) ) ) |
10 |
|
c0ex |
|- 0 e. _V |
11 |
10
|
fvconst2 |
|- ( x e. A -> ( ( A X. { 0 } ) ` x ) = 0 ) |
12 |
11
|
adantl |
|- ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( ( A X. { 0 } ) ` x ) = 0 ) |
13 |
9 12
|
eqeq12d |
|- ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( ( ( F oF - G ) ` x ) = ( ( A X. { 0 } ) ` x ) <-> ( ( F ` x ) - ( G ` x ) ) = 0 ) ) |
14 |
1
|
ffvelrnda |
|- ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( F ` x ) e. CC ) |
15 |
3
|
ffvelrnda |
|- ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( G ` x ) e. CC ) |
16 |
14 15
|
subeq0ad |
|- ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( ( ( F ` x ) - ( G ` x ) ) = 0 <-> ( F ` x ) = ( G ` x ) ) ) |
17 |
13 16
|
bitrd |
|- ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( ( ( F oF - G ) ` x ) = ( ( A X. { 0 } ) ` x ) <-> ( F ` x ) = ( G ` x ) ) ) |
18 |
17
|
ralbidva |
|- ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( A. x e. A ( ( F oF - G ) ` x ) = ( ( A X. { 0 } ) ` x ) <-> A. x e. A ( F ` x ) = ( G ` x ) ) ) |
19 |
2 4 5 5 6
|
offn |
|- ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( F oF - G ) Fn A ) |
20 |
10
|
fconst |
|- ( A X. { 0 } ) : A --> { 0 } |
21 |
|
ffn |
|- ( ( A X. { 0 } ) : A --> { 0 } -> ( A X. { 0 } ) Fn A ) |
22 |
20 21
|
ax-mp |
|- ( A X. { 0 } ) Fn A |
23 |
|
eqfnfv |
|- ( ( ( F oF - G ) Fn A /\ ( A X. { 0 } ) Fn A ) -> ( ( F oF - G ) = ( A X. { 0 } ) <-> A. x e. A ( ( F oF - G ) ` x ) = ( ( A X. { 0 } ) ` x ) ) ) |
24 |
19 22 23
|
sylancl |
|- ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( ( F oF - G ) = ( A X. { 0 } ) <-> A. x e. A ( ( F oF - G ) ` x ) = ( ( A X. { 0 } ) ` x ) ) ) |
25 |
|
eqfnfv |
|- ( ( F Fn A /\ G Fn A ) -> ( F = G <-> A. x e. A ( F ` x ) = ( G ` x ) ) ) |
26 |
2 4 25
|
syl2anc |
|- ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( F = G <-> A. x e. A ( F ` x ) = ( G ` x ) ) ) |
27 |
18 24 26
|
3bitr4d |
|- ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( ( F oF - G ) = ( A X. { 0 } ) <-> F = G ) ) |