ofsubge0

Description: Function analogue of subge0 . (Contributed by Mario Carneiro, 24-Jul-2014)

		Ref	Expression
	Assertion	ofsubge0	$⊢ (A \in V \land F : A ⟶ ℝ \land G : A ⟶ ℝ) \to ((A \times \{0\}) \leq_{f} (F -_{f} G) \leftrightarrow G \leq_{f} F)$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (A \in V \land F : A ⟶ ℝ \land G : A ⟶ ℝ) \to F : A ⟶ ℝ$
2	1	ffvelcdmda	$⊢ ((A \in V \land F : A ⟶ ℝ \land G : A ⟶ ℝ) \land x \in A) \to F (x) \in ℝ$
3		simp3	$⊢ (A \in V \land F : A ⟶ ℝ \land G : A ⟶ ℝ) \to G : A ⟶ ℝ$
4	3	ffvelcdmda	$⊢ ((A \in V \land F : A ⟶ ℝ \land G : A ⟶ ℝ) \land x \in A) \to G (x) \in ℝ$
5	2 4	subge0d	$⊢ ((A \in V \land F : A ⟶ ℝ \land G : A ⟶ ℝ) \land x \in A) \to (0 \leq F (x) - G (x) \leftrightarrow G (x) \leq F (x))$
6	5	ralbidva	$⊢ (A \in V \land F : A ⟶ ℝ \land G : A ⟶ ℝ) \to (\forall x \in A 0 \leq F (x) - G (x) \leftrightarrow \forall x \in A G (x) \leq F (x))$
7		0cn	$⊢ 0 \in ℂ$
8		fnconstg	$⊢ 0 \in ℂ \to (A \times \{0\}) Fn A$
9	7 8	mp1i	$⊢ (A \in V \land F : A ⟶ ℝ \land G : A ⟶ ℝ) \to (A \times \{0\}) Fn A$
10	1	ffnd	$⊢ (A \in V \land F : A ⟶ ℝ \land G : A ⟶ ℝ) \to F Fn A$
11	3	ffnd	$⊢ (A \in V \land F : A ⟶ ℝ \land G : A ⟶ ℝ) \to G Fn A$
12		simp1	$⊢ (A \in V \land F : A ⟶ ℝ \land G : A ⟶ ℝ) \to A \in V$
13		inidm	$⊢ A \cap A = A$
14	10 11 12 12 13	offn	$⊢ (A \in V \land F : A ⟶ ℝ \land G : A ⟶ ℝ) \to (F -_{f} G) Fn A$
15		c0ex	$⊢ 0 \in V$
16	15	fvconst2	$⊢ x \in A \to (A \times \{0\}) (x) = 0$
17	16	adantl	$⊢ ((A \in V \land F : A ⟶ ℝ \land G : A ⟶ ℝ) \land x \in A) \to (A \times \{0\}) (x) = 0$
18		eqidd	$⊢ ((A \in V \land F : A ⟶ ℝ \land G : A ⟶ ℝ) \land x \in A) \to F (x) = F (x)$
19		eqidd	$⊢ ((A \in V \land F : A ⟶ ℝ \land G : A ⟶ ℝ) \land x \in A) \to G (x) = G (x)$
20	10 11 12 12 13 18 19	ofval	$⊢ ((A \in V \land F : A ⟶ ℝ \land G : A ⟶ ℝ) \land x \in A) \to (F -_{f} G) (x) = F (x) - G (x)$
21	9 14 12 12 13 17 20	ofrfval	$⊢ (A \in V \land F : A ⟶ ℝ \land G : A ⟶ ℝ) \to ((A \times \{0\}) \leq_{f} (F -_{f} G) \leftrightarrow \forall x \in A 0 \leq F (x) - G (x))$
22	11 10 12 12 13 19 18	ofrfval	$⊢ (A \in V \land F : A ⟶ ℝ \land G : A ⟶ ℝ) \to (G \leq_{f} F \leftrightarrow \forall x \in A G (x) \leq F (x))$
23	6 21 22	3bitr4d	$⊢ (A \in V \land F : A ⟶ ℝ \land G : A ⟶ ℝ) \to ((A \times \{0\}) \leq_{f} (F -_{f} G) \leftrightarrow G \leq_{f} F)$

Metamath Proof Explorer

Theorem ofsubge0

Proof