Metamath Proof Explorer


Theorem ofsubeq0

Description: Function analogue of subeq0 . (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Assertion ofsubeq0
|- ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( ( F oF - G ) = ( A X. { 0 } ) <-> F = G ) )

Proof

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 ) )