ofsubeq0

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

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

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to F : A ⟶ ℂ$
2	1	ffnd	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to F Fn A$
3		simp3	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to G : A ⟶ ℂ$
4	3	ffnd	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to G Fn A$
5		simp1	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to A \in V$
6		inidm	$⊢ A \cap A = A$
7		eqidd	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \land x \in A) \to F (x) = F (x)$
8		eqidd	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \land x \in A) \to G (x) = G (x)$
9	2 4 5 5 6 7 8	ofval	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \land x \in A) \to (F -_{f} G) (x) = F (x) - G (x)$
10		c0ex	$⊢ 0 \in V$
11	10	fvconst2	$⊢ x \in A \to (A \times \{0\}) (x) = 0$
12	11	adantl	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \land x \in A) \to (A \times \{0\}) (x) = 0$
13	9 12	eqeq12d	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \land x \in A) \to ((F -_{f} G) (x) = (A \times \{0\}) (x) \leftrightarrow F (x) - G (x) = 0)$
14	1	ffvelcdmda	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \land x \in A) \to F (x) \in ℂ$
15	3	ffvelcdmda	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \land x \in A) \to G (x) \in ℂ$
16	14 15	subeq0ad	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \land x \in A) \to (F (x) - G (x) = 0 \leftrightarrow F (x) = G (x))$
17	13 16	bitrd	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \land x \in A) \to ((F -_{f} G) (x) = (A \times \{0\}) (x) \leftrightarrow F (x) = G (x))$
18	17	ralbidva	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to (\forall x \in A (F -_{f} G) (x) = (A \times \{0\}) (x) \leftrightarrow \forall x \in A F (x) = G (x))$
19	2 4 5 5 6	offn	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to (F -_{f} G) Fn A$
20	10	fconst	$⊢ (A \times \{0\}) : A ⟶ \{0\}$
21		ffn	$⊢ (A \times \{0\}) : A ⟶ \{0\} \to (A \times \{0\}) Fn A$
22	20 21	ax-mp	$⊢ (A \times \{0\}) Fn A$
23		eqfnfv	$⊢ ((F -_{f} G) Fn A \land (A \times \{0\}) Fn A) \to (F -_{f} G = A \times \{0\} \leftrightarrow \forall x \in A (F -_{f} G) (x) = (A \times \{0\}) (x))$
24	19 22 23	sylancl	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to (F -_{f} G = A \times \{0\} \leftrightarrow \forall x \in A (F -_{f} G) (x) = (A \times \{0\}) (x))$
25		eqfnfv	$⊢ (F Fn A \land G Fn A) \to (F = G \leftrightarrow \forall x \in A F (x) = G (x))$
26	2 4 25	syl2anc	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to (F = G \leftrightarrow \forall x \in A F (x) = G (x))$
27	18 24 26	3bitr4d	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to (F -_{f} G = A \times \{0\} \leftrightarrow F = G)$

Metamath Proof Explorer

Theorem ofsubeq0

Proof