0pledm

Description: Adjust the domain of the left argument to match the right, which works better in our theorems. (Contributed by Mario Carneiro, 28-Jul-2014)

	Ref	Expression
Hypotheses	0pledm.1	$⊢ φ \to A \subseteq ℂ$
	0pledm.2	$⊢ φ \to F Fn A$
Assertion	0pledm	$⊢ φ \to (0_{𝑝} \leq_{f} F \leftrightarrow (A \times \{0\}) \leq_{f} F)$

Proof

Step	Hyp	Ref	Expression
1		0pledm.1	$⊢ φ \to A \subseteq ℂ$
2		0pledm.2	$⊢ φ \to F Fn A$
3		sseqin2	$⊢ A \subseteq ℂ \leftrightarrow ℂ \cap A = A$
4	1 3	sylib	$⊢ φ \to ℂ \cap A = A$
5	4	raleqdv	$⊢ φ \to (\forall x \in (ℂ \cap A) 0 \leq F (x) \leftrightarrow \forall x \in A 0 \leq F (x))$
6		0cn	$⊢ 0 \in ℂ$
7		fnconstg	$⊢ 0 \in ℂ \to (ℂ \times \{0\}) Fn ℂ$
8	6 7	ax-mp	$⊢ (ℂ \times \{0\}) Fn ℂ$
9		df-0p	$⊢ 0_{𝑝} = ℂ \times \{0\}$
10	9	fneq1i	$⊢ 0_{𝑝} Fn ℂ \leftrightarrow (ℂ \times \{0\}) Fn ℂ$
11	8 10	mpbir	$⊢ 0_{𝑝} Fn ℂ$
12	11	a1i	$⊢ φ \to 0_{𝑝} Fn ℂ$
13		cnex	$⊢ ℂ \in V$
14	13	a1i	$⊢ φ \to ℂ \in V$
15		ssexg	$⊢ (A \subseteq ℂ \land ℂ \in V) \to A \in V$
16	1 13 15	sylancl	$⊢ φ \to A \in V$
17		eqid	$⊢ ℂ \cap A = ℂ \cap A$
18		0pval	$⊢ x \in ℂ \to 0_{𝑝} (x) = 0$
19	18	adantl	$⊢ (φ \land x \in ℂ) \to 0_{𝑝} (x) = 0$
20		eqidd	$⊢ (φ \land x \in A) \to F (x) = F (x)$
21	12 2 14 16 17 19 20	ofrfval	$⊢ φ \to (0_{𝑝} \leq_{f} F \leftrightarrow \forall x \in (ℂ \cap A) 0 \leq F (x))$
22		fnconstg	$⊢ 0 \in ℂ \to (A \times \{0\}) Fn A$
23	6 22	ax-mp	$⊢ (A \times \{0\}) Fn A$
24	23	a1i	$⊢ φ \to (A \times \{0\}) Fn A$
25		inidm	$⊢ A \cap A = A$
26		c0ex	$⊢ 0 \in V$
27	26	fvconst2	$⊢ x \in A \to (A \times \{0\}) (x) = 0$
28	27	adantl	$⊢ (φ \land x \in A) \to (A \times \{0\}) (x) = 0$
29	24 2 16 16 25 28 20	ofrfval	$⊢ φ \to ((A \times \{0\}) \leq_{f} F \leftrightarrow \forall x \in A 0 \leq F (x))$
30	5 21 29	3bitr4d	$⊢ φ \to (0_{𝑝} \leq_{f} F \leftrightarrow (A \times \{0\}) \leq_{f} F)$

Metamath Proof Explorer

Theorem 0pledm

Proof