suppco

Description: The support of the composition of two functions is the inverse image by the inner function of the support of the outer function. (Contributed by AV, 30-May-2019) Extract this statement from the proof of supp0cosupp0 . (Revised by SN, 15-Sep-2023)

		Ref	Expression
	Assertion	suppco	$⊢ (F \in V \land G \in W) \to (F \circ G) supp Z = G^{-1} [F supp Z]$

Proof

Step	Hyp	Ref	Expression
1		coexg	$⊢ (F \in V \land G \in W) \to F \circ G \in V$
2		simpl	$⊢ (Z \in V \land (F \in V \land G \in W)) \to Z \in V$
3		suppimacnv	$⊢ (F \circ G \in V \land Z \in V) \to (F \circ G) supp Z = {(F \circ G)}^{-1} [V ∖ \{Z\}]$
4	1 2 3	syl2an2	$⊢ (Z \in V \land (F \in V \land G \in W)) \to (F \circ G) supp Z = {(F \circ G)}^{-1} [V ∖ \{Z\}]$
5		cnvco	$⊢ {(F \circ G)}^{-1} = G^{-1} \circ F^{-1}$
6	5	imaeq1i	$⊢ {(F \circ G)}^{-1} [V ∖ \{Z\}] = (G^{-1} \circ F^{-1}) [V ∖ \{Z\}]$
7	6	a1i	$⊢ (Z \in V \land (F \in V \land G \in W)) \to {(F \circ G)}^{-1} [V ∖ \{Z\}] = (G^{-1} \circ F^{-1}) [V ∖ \{Z\}]$
8		imaco	$⊢ (G^{-1} \circ F^{-1}) [V ∖ \{Z\}] = G^{-1} [F^{-1} [V ∖ \{Z\}]]$
9		simprl	$⊢ (Z \in V \land (F \in V \land G \in W)) \to F \in V$
10		suppimacnv	$⊢ (F \in V \land Z \in V) \to F supp Z = F^{-1} [V ∖ \{Z\}]$
11	9 2 10	syl2anc	$⊢ (Z \in V \land (F \in V \land G \in W)) \to F supp Z = F^{-1} [V ∖ \{Z\}]$
12	11	imaeq2d	$⊢ (Z \in V \land (F \in V \land G \in W)) \to G^{-1} [F supp Z] = G^{-1} [F^{-1} [V ∖ \{Z\}]]$
13	8 12	eqtr4id	$⊢ (Z \in V \land (F \in V \land G \in W)) \to (G^{-1} \circ F^{-1}) [V ∖ \{Z\}] = G^{-1} [F supp Z]$
14	4 7 13	3eqtrd	$⊢ (Z \in V \land (F \in V \land G \in W)) \to (F \circ G) supp Z = G^{-1} [F supp Z]$
15	14	ex	$⊢ Z \in V \to ((F \in V \land G \in W) \to (F \circ G) supp Z = G^{-1} [F supp Z])$
16		prcnel	$⊢ \neg Z \in V \to \neg Z \in V$
17	16	intnand	$⊢ \neg Z \in V \to \neg (F \circ G \in V \land Z \in V)$
18		supp0prc	$⊢ \neg (F \circ G \in V \land Z \in V) \to (F \circ G) supp Z = \emptyset$
19	17 18	syl	$⊢ \neg Z \in V \to (F \circ G) supp Z = \emptyset$
20	16	intnand	$⊢ \neg Z \in V \to \neg (F \in V \land Z \in V)$
21		supp0prc	$⊢ \neg (F \in V \land Z \in V) \to F supp Z = \emptyset$
22	20 21	syl	$⊢ \neg Z \in V \to F supp Z = \emptyset$
23	22	imaeq2d	$⊢ \neg Z \in V \to G^{-1} [F supp Z] = G^{-1} [\emptyset]$
24		ima0	$⊢ G^{-1} [\emptyset] = \emptyset$
25	23 24	eqtrdi	$⊢ \neg Z \in V \to G^{-1} [F supp Z] = \emptyset$
26	19 25	eqtr4d	$⊢ \neg Z \in V \to (F \circ G) supp Z = G^{-1} [F supp Z]$
27	26	a1d	$⊢ \neg Z \in V \to ((F \in V \land G \in W) \to (F \circ G) supp Z = G^{-1} [F supp Z])$
28	15 27	pm2.61i	$⊢ (F \in V \land G \in W) \to (F \circ G) supp Z = G^{-1} [F supp Z]$

Metamath Proof Explorer

Theorem suppco

Proof