supp0cosupp0

Description: The support of the composition of two functions is empty if the support of the outer function is empty. (Contributed by AV, 30-May-2019)

		Ref	Expression
	Assertion	supp0cosupp0	$⊢ (F \in V \land G \in W) \to (F supp Z = \emptyset \to (F \circ G) supp Z = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		suppco	$⊢ (F \in V \land G \in W) \to (F \circ G) supp Z = G^{-1} [F supp Z]$
2		imaeq2	$⊢ F supp Z = \emptyset \to G^{-1} [F supp Z] = G^{-1} [\emptyset]$
3		ima0	$⊢ G^{-1} [\emptyset] = \emptyset$
4	2 3	eqtrdi	$⊢ F supp Z = \emptyset \to G^{-1} [F supp Z] = \emptyset$
5	1 4	sylan9eq	$⊢ ((F \in V \land G \in W) \land F supp Z = \emptyset) \to (F \circ G) supp Z = \emptyset$
6	5	ex	$⊢ (F \in V \land G \in W) \to (F supp Z = \emptyset \to (F \circ G) supp Z = \emptyset)$

Metamath Proof Explorer

Theorem supp0cosupp0

Proof