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