Metamath Proof Explorer

Theorem psrbagcon

Description: The analogue of the statement " 0 <_ G <_ F implies 0 <_ F - G <_ F " for finite bags. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypothesis psrbag.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
Assertion psrbagcon 
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( ( F oF - G ) e. D /\ ( F oF - G ) oR <_ F ) )

Proof

Step Hyp Ref Expression
1 psrbag.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2 simpr1 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> F e. D )
3 1 psrbag 
 |-  ( I e. V -> ( F e. D <-> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) )
4 3 adantr 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( F e. D <-> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) )
5 2 4 mpbid 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) )
6 5 simpld 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> F : I --> NN0 )
7 6 ffnd 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> F Fn I )
8 simpr2 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> G : I --> NN0 )
9 8 ffnd 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> G Fn I )
10 simpl 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> I e. V )
11 inidm 
 |-  ( I i^i I ) = I
12 7 9 10 10 11 offn 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( F oF - G ) Fn I )
13 eqidd 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( F ` x ) = ( F ` x ) )
14 eqidd 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( G ` x ) = ( G ` x ) )
15 7 9 10 10 11 13 14 ofval 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( ( F oF - G ) ` x ) = ( ( F ` x ) - ( G ` x ) ) )
16 simpr3 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> G oR <_ F )
17 9 7 10 10 11 14 13 ofrfval 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( G oR <_ F <-> A. x e. I ( G ` x ) <_ ( F ` x ) ) )
18 16 17 mpbid 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> A. x e. I ( G ` x ) <_ ( F ` x ) )
19 18 r19.21bi 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( G ` x ) <_ ( F ` x ) )
20 8 ffvelrnda 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( G ` x ) e. NN0 )
21 6 ffvelrnda 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( F ` x ) e. NN0 )
22 nn0sub 
 |-  ( ( ( G ` x ) e. NN0 /\ ( F ` x ) e. NN0 ) -> ( ( G ` x ) <_ ( F ` x ) <-> ( ( F ` x ) - ( G ` x ) ) e. NN0 ) )
23 20 21 22 syl2anc 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( ( G ` x ) <_ ( F ` x ) <-> ( ( F ` x ) - ( G ` x ) ) e. NN0 ) )
24 19 23 mpbid 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( ( F ` x ) - ( G ` x ) ) e. NN0 )
25 15 24 eqeltrd 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( ( F oF - G ) ` x ) e. NN0 )
26 25 ralrimiva 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> A. x e. I ( ( F oF - G ) ` x ) e. NN0 )
27 ffnfv 
 |-  ( ( F oF - G ) : I --> NN0 <-> ( ( F oF - G ) Fn I /\ A. x e. I ( ( F oF - G ) ` x ) e. NN0 ) )
28 12 26 27 sylanbrc 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( F oF - G ) : I --> NN0 )
29 5 simprd 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( `' F " NN ) e. Fin )
30 20 nn0ge0d 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> 0 <_ ( G ` x ) )
31 nn0re 
 |-  ( ( F ` x ) e. NN0 -> ( F ` x ) e. RR )
32 nn0re 
 |-  ( ( G ` x ) e. NN0 -> ( G ` x ) e. RR )
33 subge02 
 |-  ( ( ( F ` x ) e. RR /\ ( G ` x ) e. RR ) -> ( 0 <_ ( G ` x ) <-> ( ( F ` x ) - ( G ` x ) ) <_ ( F ` x ) ) )
34 31 32 33 syl2an 
 |-  ( ( ( F ` x ) e. NN0 /\ ( G ` x ) e. NN0 ) -> ( 0 <_ ( G ` x ) <-> ( ( F ` x ) - ( G ` x ) ) <_ ( F ` x ) ) )
35 21 20 34 syl2anc 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( 0 <_ ( G ` x ) <-> ( ( F ` x ) - ( G ` x ) ) <_ ( F ` x ) ) )
36 30 35 mpbid 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( ( F ` x ) - ( G ` x ) ) <_ ( F ` x ) )
37 36 ralrimiva 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> A. x e. I ( ( F ` x ) - ( G ` x ) ) <_ ( F ` x ) )
38 12 7 10 10 11 15 13 ofrfval 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( ( F oF - G ) oR <_ F <-> A. x e. I ( ( F ` x ) - ( G ` x ) ) <_ ( F ` x ) ) )
39 37 38 mpbird 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( F oF - G ) oR <_ F )
40 1 psrbaglesupp 
 |-  ( ( I e. V /\ ( F e. D /\ ( F oF - G ) : I --> NN0 /\ ( F oF - G ) oR <_ F ) ) -> ( `' ( F oF - G ) " NN ) C_ ( `' F " NN ) )
41 10 2 28 39 40 syl13anc 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( `' ( F oF - G ) " NN ) C_ ( `' F " NN ) )
42 29 41 ssfid 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( `' ( F oF - G ) " NN ) e. Fin )
43 1 psrbag 
 |-  ( I e. V -> ( ( F oF - G ) e. D <-> ( ( F oF - G ) : I --> NN0 /\ ( `' ( F oF - G ) " NN ) e. Fin ) ) )
44 43 adantr 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( ( F oF - G ) e. D <-> ( ( F oF - G ) : I --> NN0 /\ ( `' ( F oF - G ) " NN ) e. Fin ) ) )
45 28 42 44 mpbir2and 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( F oF - G ) e. D )
46 45 39 jca 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( ( F oF - G ) e. D /\ ( F oF - G ) oR <_ F ) )