gsumbagdiaglemOLD

Description: Obsolete version of gsumbagdiaglem as of 6-Aug-2024. (Contributed by Mario Carneiro, 5-Jan-2015) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	psrbag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	psrbagconf1o.s	$⊢ S = \{y \in D \| y \leq_{f} F\}$
	gsumbagdiagOLD.i	$⊢ φ \to I \in V$
	gsumbagdiagOLD.f	$⊢ φ \to F \in D$
Assertion	gsumbagdiaglemOLD	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to (Y \in S \land X \in \{x \in D \| x \leq_{f} (F -_{f} Y)\})$

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		gsumbagdiagOLD.i	$⊢ φ \to I \in V$
4		gsumbagdiagOLD.f	$⊢ φ \to F \in D$
5		simprr	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\}$
6		breq1	$⊢ x = Y \to (x \leq_{f} (F -_{f} X) \leftrightarrow Y \leq_{f} (F -_{f} X))$
7	6	elrab	$⊢ Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\} \leftrightarrow (Y \in D \land Y \leq_{f} (F -_{f} X))$
8	5 7	sylib	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to (Y \in D \land Y \leq_{f} (F -_{f} X))$
9	8	simpld	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to Y \in D$
10	8	simprd	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to Y \leq_{f} (F -_{f} X)$
11	3	adantr	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to I \in V$
12	4	adantr	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to F \in D$
13		simprl	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to X \in S$
14		breq1	$⊢ y = X \to (y \leq_{f} F \leftrightarrow X \leq_{f} F)$
15	14 2	elrab2	$⊢ X \in S \leftrightarrow (X \in D \land X \leq_{f} F)$
16	13 15	sylib	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to (X \in D \land X \leq_{f} F)$
17	16	simpld	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to X \in D$
18	1	psrbagfOLD	$⊢ (I \in V \land X \in D) \to X : I ⟶ ℕ_{0}$
19	11 17 18	syl2anc	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to X : I ⟶ ℕ_{0}$
20	16	simprd	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to X \leq_{f} F$
21	1	psrbagconOLD	$⊢ (I \in V \land (F \in D \land X : I ⟶ ℕ_{0} \land X \leq_{f} F)) \to (F -_{f} X \in D \land (F -_{f} X) \leq_{f} F)$
22	11 12 19 20 21	syl13anc	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to (F -_{f} X \in D \land (F -_{f} X) \leq_{f} F)$
23	22	simprd	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to (F -_{f} X) \leq_{f} F$
24	1	psrbagfOLD	$⊢ (I \in V \land Y \in D) \to Y : I ⟶ ℕ_{0}$
25	11 9 24	syl2anc	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to Y : I ⟶ ℕ_{0}$
26	22	simpld	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to F -_{f} X \in D$
27	1	psrbagfOLD	$⊢ (I \in V \land F -_{f} X \in D) \to (F -_{f} X) : I ⟶ ℕ_{0}$
28	11 26 27	syl2anc	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to (F -_{f} X) : I ⟶ ℕ_{0}$
29	1	psrbagfOLD	$⊢ (I \in V \land F \in D) \to F : I ⟶ ℕ_{0}$
30	11 12 29	syl2anc	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to F : I ⟶ ℕ_{0}$
31		nn0re	$⊢ u \in ℕ_{0} \to u \in ℝ$
32		nn0re	$⊢ v \in ℕ_{0} \to v \in ℝ$
33		nn0re	$⊢ w \in ℕ_{0} \to w \in ℝ$
34		letr	$⊢ (u \in ℝ \land v \in ℝ \land w \in ℝ) \to ((u \leq v \land v \leq w) \to u \leq w)$
35	31 32 33 34	syl3an	$⊢ (u \in ℕ_{0} \land v \in ℕ_{0} \land w \in ℕ_{0}) \to ((u \leq v \land v \leq w) \to u \leq w)$
36	35	adantl	$⊢ ((φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \land (u \in ℕ_{0} \land v \in ℕ_{0} \land w \in ℕ_{0})) \to ((u \leq v \land v \leq w) \to u \leq w)$
37	11 25 28 30 36	caoftrn	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to ((Y \leq_{f} (F -_{f} X) \land (F -_{f} X) \leq_{f} F) \to Y \leq_{f} F)$
38	10 23 37	mp2and	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to Y \leq_{f} F$
39		breq1	$⊢ y = Y \to (y \leq_{f} F \leftrightarrow Y \leq_{f} F)$
40	39 2	elrab2	$⊢ Y \in S \leftrightarrow (Y \in D \land Y \leq_{f} F)$
41	9 38 40	sylanbrc	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to Y \in S$
42		breq1	$⊢ x = X \to (x \leq_{f} (F -_{f} Y) \leftrightarrow X \leq_{f} (F -_{f} Y))$
43	19	ffvelcdmda	$⊢ ((φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \land z \in I) \to X (z) \in ℕ_{0}$
44	25	ffvelcdmda	$⊢ ((φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \land z \in I) \to Y (z) \in ℕ_{0}$
45	30	ffvelcdmda	$⊢ ((φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \land z \in I) \to F (z) \in ℕ_{0}$
46		nn0re	$⊢ X (z) \in ℕ_{0} \to X (z) \in ℝ$
47		nn0re	$⊢ Y (z) \in ℕ_{0} \to Y (z) \in ℝ$
48		nn0re	$⊢ F (z) \in ℕ_{0} \to F (z) \in ℝ$
49		leaddsub2	$⊢ (X (z) \in ℝ \land Y (z) \in ℝ \land F (z) \in ℝ) \to (X (z) + Y (z) \leq F (z) \leftrightarrow Y (z) \leq F (z) - X (z))$
50		leaddsub	$⊢ (X (z) \in ℝ \land Y (z) \in ℝ \land F (z) \in ℝ) \to (X (z) + Y (z) \leq F (z) \leftrightarrow X (z) \leq F (z) - Y (z))$
51	49 50	bitr3d	$⊢ (X (z) \in ℝ \land Y (z) \in ℝ \land F (z) \in ℝ) \to (Y (z) \leq F (z) - X (z) \leftrightarrow X (z) \leq F (z) - Y (z))$
52	46 47 48 51	syl3an	$⊢ (X (z) \in ℕ_{0} \land Y (z) \in ℕ_{0} \land F (z) \in ℕ_{0}) \to (Y (z) \leq F (z) - X (z) \leftrightarrow X (z) \leq F (z) - Y (z))$
53	43 44 45 52	syl3anc	$⊢ ((φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \land z \in I) \to (Y (z) \leq F (z) - X (z) \leftrightarrow X (z) \leq F (z) - Y (z))$
54	53	ralbidva	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to (\forall z \in I Y (z) \leq F (z) - X (z) \leftrightarrow \forall z \in I X (z) \leq F (z) - Y (z))$
55		ovexd	$⊢ ((φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \land z \in I) \to F (z) - X (z) \in V$
56	25	feqmptd	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to Y = (z \in I ⟼ Y (z))$
57	30	ffnd	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to F Fn I$
58	19	ffnd	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to X Fn I$
59		inidm	$⊢ I \cap I = I$
60		eqidd	$⊢ ((φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \land z \in I) \to F (z) = F (z)$
61		eqidd	$⊢ ((φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \land z \in I) \to X (z) = X (z)$
62	57 58 11 11 59 60 61	offval	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to F -_{f} X = (z \in I ⟼ F (z) - X (z))$
63	11 44 55 56 62	ofrfval2	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to (Y \leq_{f} (F -_{f} X) \leftrightarrow \forall z \in I Y (z) \leq F (z) - X (z))$
64		ovexd	$⊢ ((φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \land z \in I) \to F (z) - Y (z) \in V$
65	19	feqmptd	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to X = (z \in I ⟼ X (z))$
66	25	ffnd	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to Y Fn I$
67		eqidd	$⊢ ((φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \land z \in I) \to Y (z) = Y (z)$
68	57 66 11 11 59 60 67	offval	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to F -_{f} Y = (z \in I ⟼ F (z) - Y (z))$
69	11 43 64 65 68	ofrfval2	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to (X \leq_{f} (F -_{f} Y) \leftrightarrow \forall z \in I X (z) \leq F (z) - Y (z))$
70	54 63 69	3bitr4d	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to (Y \leq_{f} (F -_{f} X) \leftrightarrow X \leq_{f} (F -_{f} Y))$
71	10 70	mpbid	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to X \leq_{f} (F -_{f} Y)$
72	42 17 71	elrabd	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to X \in \{x \in D \| x \leq_{f} (F -_{f} Y)\}$
73	41 72	jca	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to (Y \in S \land X \in \{x \in D \| x \leq_{f} (F -_{f} Y)\})$

Metamath Proof Explorer

Theorem gsumbagdiaglemOLD

Proof