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 ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
Assertion psrbagcon ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → ( ( 𝐹 ∘f − 𝐺 ) ∈ 𝐷 ∧ ( 𝐹 ∘f − 𝐺 ) ∘r ≤ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 psrbag.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2 simpr1 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → 𝐹 ∈ 𝐷 )
3 1 psrbag ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐹 ∈ 𝐷 ↔ ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) ) )
4 3 adantr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → ( 𝐹 ∈ 𝐷 ↔ ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) ) )
5 2 4 mpbid ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) )
6 5 simpld ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → 𝐹 : 𝐼 ⟶ ℕ0 )
7 6 ffnd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → 𝐹 Fn 𝐼 )
8 simpr2 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → 𝐺 : 𝐼 ⟶ ℕ0 )
9 8 ffnd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → 𝐺 Fn 𝐼 )
10 simpl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → 𝐼 ∈ 𝑉 )
11 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
12 7 9 10 10 11 offn ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → ( 𝐹 ∘f − 𝐺 ) Fn 𝐼 )
13 eqidd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
14 eqidd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
15 7 9 10 10 11 13 14 ofval ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) )
16 simpr3 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → 𝐺 ∘r ≤ 𝐹 )
17 9 7 10 10 11 14 13 ofrfval ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → ( 𝐺 ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
18 16 17 mpbid ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
19 18 r19.21bi ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
20 8 ffvelrnda ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℕ0 )
21 6 ffvelrnda ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℕ0 )
22 nn0sub ⊢ ( ( ( 𝐺 ‘ 𝑥 ) ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ∈ ℕ0 ) )
23 20 21 22 syl2anc ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ∈ ℕ0 ) )
24 19 23 mpbid ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ∈ ℕ0 )
25 15 24 eqeltrd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) ∈ ℕ0 )
26 25 ralrimiva ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) ∈ ℕ0 )
27 ffnfv ⊢ ( ( 𝐹 ∘f − 𝐺 ) : 𝐼 ⟶ ℕ0 ↔ ( ( 𝐹 ∘f − 𝐺 ) Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) ∈ ℕ0 ) )
28 12 26 27 sylanbrc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → ( 𝐹 ∘f − 𝐺 ) : 𝐼 ⟶ ℕ0 )
29 5 simprd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → ( ◡ 𝐹 “ ℕ ) ∈ Fin )
30 20 nn0ge0d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ 𝐼 ) → 0 ≤ ( 𝐺 ‘ 𝑥 ) )
31 nn0re ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ℕ0 → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
32 nn0re ⊢ ( ( 𝐺 ‘ 𝑥 ) ∈ ℕ0 → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
33 subge02 ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ ( 𝐺 ‘ 𝑥 ) ∈ ℝ ) → ( 0 ≤ ( 𝐺 ‘ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
34 31 32 33 syl2an ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℕ0 ∧ ( 𝐺 ‘ 𝑥 ) ∈ ℕ0 ) → ( 0 ≤ ( 𝐺 ‘ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
35 21 20 34 syl2anc ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 0 ≤ ( 𝐺 ‘ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
36 30 35 mpbid ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ≤ ( 𝐹 ‘ 𝑥 ) )
37 36 ralrimiva ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ≤ ( 𝐹 ‘ 𝑥 ) )
38 12 7 10 10 11 15 13 ofrfval ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → ( ( 𝐹 ∘f − 𝐺 ) ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
39 37 38 mpbird ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → ( 𝐹 ∘f − 𝐺 ) ∘r ≤ 𝐹 )
40 1 psrbaglesupp ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ ( 𝐹 ∘f − 𝐺 ) : 𝐼 ⟶ ℕ0 ∧ ( 𝐹 ∘f − 𝐺 ) ∘r ≤ 𝐹 ) ) → ( ◡ ( 𝐹 ∘f − 𝐺 ) “ ℕ ) ⊆ ( ◡ 𝐹 “ ℕ ) )
41 10 2 28 39 40 syl13anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → ( ◡ ( 𝐹 ∘f − 𝐺 ) “ ℕ ) ⊆ ( ◡ 𝐹 “ ℕ ) )
42 29 41 ssfid ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → ( ◡ ( 𝐹 ∘f − 𝐺 ) “ ℕ ) ∈ Fin )
43 1 psrbag ⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝐹 ∘f − 𝐺 ) ∈ 𝐷 ↔ ( ( 𝐹 ∘f − 𝐺 ) : 𝐼 ⟶ ℕ0 ∧ ( ◡ ( 𝐹 ∘f − 𝐺 ) “ ℕ ) ∈ Fin ) ) )
44 43 adantr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → ( ( 𝐹 ∘f − 𝐺 ) ∈ 𝐷 ↔ ( ( 𝐹 ∘f − 𝐺 ) : 𝐼 ⟶ ℕ0 ∧ ( ◡ ( 𝐹 ∘f − 𝐺 ) “ ℕ ) ∈ Fin ) ) )
45 28 42 44 mpbir2and ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → ( 𝐹 ∘f − 𝐺 ) ∈ 𝐷 )
46 45 39 jca ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ) → ( ( 𝐹 ∘f − 𝐺 ) ∈ 𝐷 ∧ ( 𝐹 ∘f − 𝐺 ) ∘r ≤ 𝐹 ) )