psrbagleadd1

Description: The analogue of " X <_ F implies X + G <_ F + G " (compare leadd1d ) for bags. (Contributed by SN, 2-May-2025)

	Ref	Expression
Hypotheses	psrbag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	psrbagconf1o.s	$⊢ S = \{y \in D \| y \leq_{f} F\}$
	psrbagleadd1.t	$⊢ T = \{z \in D \| z \leq_{f} (F +_{f} G)\}$
Assertion	psrbagleadd1	$⊢ (F \in D \land G \in D \land X \in S) \to X +_{f} G \in T$

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
2		psrbagconf1o.s	$⊢ S = \{y \in D \| y \leq_{f} F\}$
3		psrbagleadd1.t	$⊢ T = \{z \in D \| z \leq_{f} (F +_{f} G)\}$
4		elrabi	$⊢ X \in \{y \in D \| y \leq_{f} F\} \to X \in D$
5	4 2	eleq2s	$⊢ X \in S \to X \in D$
6	5	3ad2ant3	$⊢ (F \in D \land G \in D \land X \in S) \to X \in D$
7		simp2	$⊢ (F \in D \land G \in D \land X \in S) \to G \in D$
8	1	psrbagaddcl	$⊢ (X \in D \land G \in D) \to X +_{f} G \in D$
9	6 7 8	syl2anc	$⊢ (F \in D \land G \in D \land X \in S) \to X +_{f} G \in D$
10	1	psrbagf	$⊢ X \in D \to X : I ⟶ ℕ_{0}$
11	6 10	syl	$⊢ (F \in D \land G \in D \land X \in S) \to X : I ⟶ ℕ_{0}$
12	11	ffvelcdmda	$⊢ ((F \in D \land G \in D \land X \in S) \land x \in I) \to X (x) \in ℕ_{0}$
13	12	nn0red	$⊢ ((F \in D \land G \in D \land X \in S) \land x \in I) \to X (x) \in ℝ$
14	1	psrbagf	$⊢ F \in D \to F : I ⟶ ℕ_{0}$
15	14	3ad2ant1	$⊢ (F \in D \land G \in D \land X \in S) \to F : I ⟶ ℕ_{0}$
16	15	ffvelcdmda	$⊢ ((F \in D \land G \in D \land X \in S) \land x \in I) \to F (x) \in ℕ_{0}$
17	16	nn0red	$⊢ ((F \in D \land G \in D \land X \in S) \land x \in I) \to F (x) \in ℝ$
18	1	psrbagf	$⊢ G \in D \to G : I ⟶ ℕ_{0}$
19	18	3ad2ant2	$⊢ (F \in D \land G \in D \land X \in S) \to G : I ⟶ ℕ_{0}$
20	19	ffvelcdmda	$⊢ ((F \in D \land G \in D \land X \in S) \land x \in I) \to G (x) \in ℕ_{0}$
21	20	nn0red	$⊢ ((F \in D \land G \in D \land X \in S) \land x \in I) \to G (x) \in ℝ$
22		breq1	$⊢ y = X \to (y \leq_{f} F \leftrightarrow X \leq_{f} F)$
23	22 2	elrab2	$⊢ X \in S \leftrightarrow (X \in D \land X \leq_{f} F)$
24	23	simprbi	$⊢ X \in S \to X \leq_{f} F$
25	24	3ad2ant3	$⊢ (F \in D \land G \in D \land X \in S) \to X \leq_{f} F$
26	10	ffnd	$⊢ X \in D \to X Fn I$
27	5 26	syl	$⊢ X \in S \to X Fn I$
28	27	3ad2ant3	$⊢ (F \in D \land G \in D \land X \in S) \to X Fn I$
29	14	ffnd	$⊢ F \in D \to F Fn I$
30	29	3ad2ant1	$⊢ (F \in D \land G \in D \land X \in S) \to F Fn I$
31		id	$⊢ F \in D \to F \in D$
32	31 29	fndmexd	$⊢ F \in D \to I \in V$
33	32	3ad2ant1	$⊢ (F \in D \land G \in D \land X \in S) \to I \in V$
34		inidm	$⊢ I \cap I = I$
35		eqidd	$⊢ ((F \in D \land G \in D \land X \in S) \land x \in I) \to X (x) = X (x)$
36		eqidd	$⊢ ((F \in D \land G \in D \land X \in S) \land x \in I) \to F (x) = F (x)$
37	28 30 33 33 34 35 36	ofrfval	$⊢ (F \in D \land G \in D \land X \in S) \to (X \leq_{f} F \leftrightarrow \forall x \in I X (x) \leq F (x))$
38	25 37	mpbid	$⊢ (F \in D \land G \in D \land X \in S) \to \forall x \in I X (x) \leq F (x)$
39	38	r19.21bi	$⊢ ((F \in D \land G \in D \land X \in S) \land x \in I) \to X (x) \leq F (x)$
40	13 17 21 39	leadd1dd	$⊢ ((F \in D \land G \in D \land X \in S) \land x \in I) \to X (x) + G (x) \leq F (x) + G (x)$
41	40	ralrimiva	$⊢ (F \in D \land G \in D \land X \in S) \to \forall x \in I X (x) + G (x) \leq F (x) + G (x)$
42	1	psrbagf	$⊢ X +_{f} G \in D \to (X +_{f} G) : I ⟶ ℕ_{0}$
43	42	ffnd	$⊢ X +_{f} G \in D \to (X +_{f} G) Fn I$
44	9 43	syl	$⊢ (F \in D \land G \in D \land X \in S) \to (X +_{f} G) Fn I$
45	1	psrbagaddcl	$⊢ (F \in D \land G \in D) \to F +_{f} G \in D$
46	45	3adant3	$⊢ (F \in D \land G \in D \land X \in S) \to F +_{f} G \in D$
47	1	psrbagf	$⊢ F +_{f} G \in D \to (F +_{f} G) : I ⟶ ℕ_{0}$
48	47	ffnd	$⊢ F +_{f} G \in D \to (F +_{f} G) Fn I$
49	46 48	syl	$⊢ (F \in D \land G \in D \land X \in S) \to (F +_{f} G) Fn I$
50	18	ffnd	$⊢ G \in D \to G Fn I$
51	50	3ad2ant2	$⊢ (F \in D \land G \in D \land X \in S) \to G Fn I$
52		eqidd	$⊢ ((F \in D \land G \in D \land X \in S) \land x \in I) \to G (x) = G (x)$
53	28 51 33 33 34 35 52	ofval	$⊢ ((F \in D \land G \in D \land X \in S) \land x \in I) \to (X +_{f} G) (x) = X (x) + G (x)$
54	30 51 33 33 34 36 52	ofval	$⊢ ((F \in D \land G \in D \land X \in S) \land x \in I) \to (F +_{f} G) (x) = F (x) + G (x)$
55	44 49 33 33 34 53 54	ofrfval	$⊢ (F \in D \land G \in D \land X \in S) \to ((X +_{f} G) \leq_{f} (F +_{f} G) \leftrightarrow \forall x \in I X (x) + G (x) \leq F (x) + G (x))$
56	41 55	mpbird	$⊢ (F \in D \land G \in D \land X \in S) \to (X +_{f} G) \leq_{f} (F +_{f} G)$
57		breq1	$⊢ z = X +_{f} G \to (z \leq_{f} (F +_{f} G) \leftrightarrow (X +_{f} G) \leq_{f} (F +_{f} G))$
58	57 3	elrab2	$⊢ X +_{f} G \in T \leftrightarrow (X +_{f} G \in D \land (X +_{f} G) \leq_{f} (F +_{f} G))$
59	9 56 58	sylanbrc	$⊢ (F \in D \land G \in D \land X \in S) \to X +_{f} G \in T$

Metamath Proof Explorer

Theorem psrbagleadd1

Proof