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 \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	Assertion	psrbagcon	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to (F -_{f} G \in D \land (F -_{f} G) \leq_{f} F)$

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
2		simpr1	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to F \in D$
3	1	psrbag	$⊢ I \in V \to (F \in D \leftrightarrow (F : I ⟶ ℕ_{0} \land F^{-1} [ℕ] \in Fin))$
4	3	adantr	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to (F \in D \leftrightarrow (F : I ⟶ ℕ_{0} \land F^{-1} [ℕ] \in Fin))$
5	2 4	mpbid	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to (F : I ⟶ ℕ_{0} \land F^{-1} [ℕ] \in Fin)$
6	5	simpld	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to F : I ⟶ ℕ_{0}$
7	6	ffnd	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to F Fn I$
8		simpr2	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to G : I ⟶ ℕ_{0}$
9	8	ffnd	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to G Fn I$
10		simpl	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to I \in V$
11		inidm	$⊢ I \cap I = I$
12	7 9 10 10 11	offn	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to (F -_{f} G) Fn I$
13		eqidd	$⊢ ((I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \land x \in I) \to F (x) = F (x)$
14		eqidd	$⊢ ((I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \land x \in I) \to G (x) = G (x)$
15	7 9 10 10 11 13 14	ofval	$⊢ ((I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \land x \in I) \to (F -_{f} G) (x) = F (x) - G (x)$
16		simpr3	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to G \leq_{f} F$
17	9 7 10 10 11 14 13	ofrfval	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to (G \leq_{f} F \leftrightarrow \forall x \in I G (x) \leq F (x))$
18	16 17	mpbid	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to \forall x \in I G (x) \leq F (x)$
19	18	r19.21bi	$⊢ ((I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \land x \in I) \to G (x) \leq F (x)$
20	8	ffvelrnda	$⊢ ((I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \land x \in I) \to G (x) \in ℕ_{0}$
21	6	ffvelrnda	$⊢ ((I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \land x \in I) \to F (x) \in ℕ_{0}$
22		nn0sub	$⊢ (G (x) \in ℕ_{0} \land F (x) \in ℕ_{0}) \to (G (x) \leq F (x) \leftrightarrow F (x) - G (x) \in ℕ_{0})$
23	20 21 22	syl2anc	$⊢ ((I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \land x \in I) \to (G (x) \leq F (x) \leftrightarrow F (x) - G (x) \in ℕ_{0})$
24	19 23	mpbid	$⊢ ((I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \land x \in I) \to F (x) - G (x) \in ℕ_{0}$
25	15 24	eqeltrd	$⊢ ((I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \land x \in I) \to (F -_{f} G) (x) \in ℕ_{0}$
26	25	ralrimiva	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to \forall x \in I (F -_{f} G) (x) \in ℕ_{0}$
27		ffnfv	$⊢ (F -_{f} G) : I ⟶ ℕ_{0} \leftrightarrow ((F -_{f} G) Fn I \land \forall x \in I (F -_{f} G) (x) \in ℕ_{0})$
28	12 26 27	sylanbrc	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to (F -_{f} G) : I ⟶ ℕ_{0}$
29	5	simprd	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to F^{-1} [ℕ] \in Fin$
30	20	nn0ge0d	$⊢ ((I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \land x \in I) \to 0 \leq G (x)$
31		nn0re	$⊢ F (x) \in ℕ_{0} \to F (x) \in ℝ$
32		nn0re	$⊢ G (x) \in ℕ_{0} \to G (x) \in ℝ$
33		subge02	$⊢ (F (x) \in ℝ \land G (x) \in ℝ) \to (0 \leq G (x) \leftrightarrow F (x) - G (x) \leq F (x))$
34	31 32 33	syl2an	$⊢ (F (x) \in ℕ_{0} \land G (x) \in ℕ_{0}) \to (0 \leq G (x) \leftrightarrow F (x) - G (x) \leq F (x))$
35	21 20 34	syl2anc	$⊢ ((I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \land x \in I) \to (0 \leq G (x) \leftrightarrow F (x) - G (x) \leq F (x))$
36	30 35	mpbid	$⊢ ((I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \land x \in I) \to F (x) - G (x) \leq F (x)$
37	36	ralrimiva	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to \forall x \in I F (x) - G (x) \leq F (x)$
38	12 7 10 10 11 15 13	ofrfval	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to ((F -_{f} G) \leq_{f} F \leftrightarrow \forall x \in I F (x) - G (x) \leq F (x))$
39	37 38	mpbird	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to (F -_{f} G) \leq_{f} F$
40	1	psrbaglesupp	$⊢ (I \in V \land (F \in D \land (F -_{f} G) : I ⟶ ℕ_{0} \land (F -_{f} G) \leq_{f} F)) \to {(F -_{f} G)}^{-1} [ℕ] \subseteq F^{-1} [ℕ]$
41	10 2 28 39 40	syl13anc	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to {(F -_{f} G)}^{-1} [ℕ] \subseteq F^{-1} [ℕ]$
42	29 41	ssfid	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to {(F -_{f} G)}^{-1} [ℕ] \in Fin$
43	1	psrbag	$⊢ I \in V \to (F -_{f} G \in D \leftrightarrow ((F -_{f} G) : I ⟶ ℕ_{0} \land {(F -_{f} G)}^{-1} [ℕ] \in Fin))$
44	43	adantr	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to (F -_{f} G \in D \leftrightarrow ((F -_{f} G) : I ⟶ ℕ_{0} \land {(F -_{f} G)}^{-1} [ℕ] \in Fin))$
45	28 42 44	mpbir2and	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to F -_{f} G \in D$
46	45 39	jca	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to (F -_{f} G \in D \land (F -_{f} G) \leq_{f} F)$

Metamath Proof Explorer

Theorem psrbagcon

Proof