This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ofsubge0

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

Ref Expression
Assertion ofsubge0 
|- ( ( A e. V /\ F : A --> RR /\ G : A --> RR ) -> ( ( A X. { 0 } ) oR <_ ( F oF - G ) <-> G oR <_ F ) )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( A e. V /\ F : A --> RR /\ G : A --> RR ) -> F : A --> RR )
2 1 ffvelcdmda 
 |-  ( ( ( A e. V /\ F : A --> RR /\ G : A --> RR ) /\ x e. A ) -> ( F ` x ) e. RR )
3 simp3 
 |-  ( ( A e. V /\ F : A --> RR /\ G : A --> RR ) -> G : A --> RR )
4 3 ffvelcdmda 
 |-  ( ( ( A e. V /\ F : A --> RR /\ G : A --> RR ) /\ x e. A ) -> ( G ` x ) e. RR )
5 2 4 subge0d 
 |-  ( ( ( A e. V /\ F : A --> RR /\ G : A --> RR ) /\ x e. A ) -> ( 0 <_ ( ( F ` x ) - ( G ` x ) ) <-> ( G ` x ) <_ ( F ` x ) ) )
6 5 ralbidva 
 |-  ( ( A e. V /\ F : A --> RR /\ G : A --> RR ) -> ( A. x e. A 0 <_ ( ( F ` x ) - ( G ` x ) ) <-> A. x e. A ( G ` x ) <_ ( F ` x ) ) )
7 0cn 
 |-  0 e. CC
8 fnconstg 
 |-  ( 0 e. CC -> ( A X. { 0 } ) Fn A )
9 7 8 mp1i 
 |-  ( ( A e. V /\ F : A --> RR /\ G : A --> RR ) -> ( A X. { 0 } ) Fn A )
10 1 ffnd 
 |-  ( ( A e. V /\ F : A --> RR /\ G : A --> RR ) -> F Fn A )
11 3 ffnd 
 |-  ( ( A e. V /\ F : A --> RR /\ G : A --> RR ) -> G Fn A )
12 simp1 
 |-  ( ( A e. V /\ F : A --> RR /\ G : A --> RR ) -> A e. V )
13 inidm 
 |-  ( A i^i A ) = A
14 10 11 12 12 13 offn 
 |-  ( ( A e. V /\ F : A --> RR /\ G : A --> RR ) -> ( F oF - G ) Fn A )
15 c0ex 
 |-  0 e. _V
16 15 fvconst2 
 |-  ( x e. A -> ( ( A X. { 0 } ) ` x ) = 0 )
17 16 adantl 
 |-  ( ( ( A e. V /\ F : A --> RR /\ G : A --> RR ) /\ x e. A ) -> ( ( A X. { 0 } ) ` x ) = 0 )
18 eqidd 
 |-  ( ( ( A e. V /\ F : A --> RR /\ G : A --> RR ) /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
19 eqidd 
 |-  ( ( ( A e. V /\ F : A --> RR /\ G : A --> RR ) /\ x e. A ) -> ( G ` x ) = ( G ` x ) )
20 10 11 12 12 13 18 19 ofval 
 |-  ( ( ( A e. V /\ F : A --> RR /\ G : A --> RR ) /\ x e. A ) -> ( ( F oF - G ) ` x ) = ( ( F ` x ) - ( G ` x ) ) )
21 9 14 12 12 13 17 20 ofrfval 
 |-  ( ( A e. V /\ F : A --> RR /\ G : A --> RR ) -> ( ( A X. { 0 } ) oR <_ ( F oF - G ) <-> A. x e. A 0 <_ ( ( F ` x ) - ( G ` x ) ) ) )
22 11 10 12 12 13 19 18 ofrfval 
 |-  ( ( A e. V /\ F : A --> RR /\ G : A --> RR ) -> ( G oR <_ F <-> A. x e. A ( G ` x ) <_ ( F ` x ) ) )
23 6 21 22 3bitr4d 
 |-  ( ( A e. V /\ F : A --> RR /\ G : A --> RR ) -> ( ( A X. { 0 } ) oR <_ ( F oF - G ) <-> G oR <_ F ) )