suppcoss

Description: The support of the composition of two functions is a subset of the support of the inner function if the outer function preserves zero. Compare suppssfv , which has a sethood condition on A instead of B . (Contributed by SN, 25-May-2024)

	Ref	Expression
Hypotheses	suppcoss.f	$⊢ φ \to F Fn A$
	suppcoss.g	$⊢ φ \to G : B ⟶ A$
	suppcoss.b	$⊢ φ \to B \in W$
	suppcoss.y	$⊢ φ \to Y \in V$
	suppcoss.1	$⊢ φ \to F (Y) = Z$
Assertion	suppcoss	$⊢ φ \to (F \circ G) supp Z \subseteq G supp Y$

Proof

Step	Hyp	Ref	Expression
1		suppcoss.f	$⊢ φ \to F Fn A$
2		suppcoss.g	$⊢ φ \to G : B ⟶ A$
3		suppcoss.b	$⊢ φ \to B \in W$
4		suppcoss.y	$⊢ φ \to Y \in V$
5		suppcoss.1	$⊢ φ \to F (Y) = Z$
6		dffn3	$⊢ F Fn A \leftrightarrow F : A ⟶ ran F$
7	1 6	sylib	$⊢ φ \to F : A ⟶ ran F$
8	7 2	fcod	$⊢ φ \to (F \circ G) : B ⟶ ran F$
9		eldif	$⊢ k \in (B ∖ {supp}_{Y} (G)) \leftrightarrow (k \in B \land \neg k \in {supp}_{Y} (G))$
10	2	ffnd	$⊢ φ \to G Fn B$
11		elsuppfn	$⊢ (G Fn B \land B \in W \land Y \in V) \to (k \in {supp}_{Y} (G) \leftrightarrow (k \in B \land G (k) \neq Y))$
12	10 3 4 11	syl3anc	$⊢ φ \to (k \in {supp}_{Y} (G) \leftrightarrow (k \in B \land G (k) \neq Y))$
13	12	notbid	$⊢ φ \to (\neg k \in {supp}_{Y} (G) \leftrightarrow \neg (k \in B \land G (k) \neq Y))$
14	13	anbi2d	$⊢ φ \to ((k \in B \land \neg k \in {supp}_{Y} (G)) \leftrightarrow (k \in B \land \neg (k \in B \land G (k) \neq Y)))$
15		annotanannot	$⊢ (k \in B \land \neg (k \in B \land G (k) \neq Y)) \leftrightarrow (k \in B \land \neg G (k) \neq Y)$
16	14 15	bitrdi	$⊢ φ \to ((k \in B \land \neg k \in {supp}_{Y} (G)) \leftrightarrow (k \in B \land \neg G (k) \neq Y))$
17	9 16	bitrid	$⊢ φ \to (k \in (B ∖ {supp}_{Y} (G)) \leftrightarrow (k \in B \land \neg G (k) \neq Y))$
18		nne	$⊢ \neg G (k) \neq Y \leftrightarrow G (k) = Y$
19	18	anbi2i	$⊢ (k \in B \land \neg G (k) \neq Y) \leftrightarrow (k \in B \land G (k) = Y)$
20	2	adantr	$⊢ (φ \land (k \in B \land G (k) = Y)) \to G : B ⟶ A$
21		simprl	$⊢ (φ \land (k \in B \land G (k) = Y)) \to k \in B$
22	20 21	fvco3d	$⊢ (φ \land (k \in B \land G (k) = Y)) \to (F \circ G) (k) = F (G (k))$
23		simprr	$⊢ (φ \land (k \in B \land G (k) = Y)) \to G (k) = Y$
24	23	fveq2d	$⊢ (φ \land (k \in B \land G (k) = Y)) \to F (G (k)) = F (Y)$
25	5	adantr	$⊢ (φ \land (k \in B \land G (k) = Y)) \to F (Y) = Z$
26	22 24 25	3eqtrd	$⊢ (φ \land (k \in B \land G (k) = Y)) \to (F \circ G) (k) = Z$
27	26	ex	$⊢ φ \to ((k \in B \land G (k) = Y) \to (F \circ G) (k) = Z)$
28	19 27	biimtrid	$⊢ φ \to ((k \in B \land \neg G (k) \neq Y) \to (F \circ G) (k) = Z)$
29	17 28	sylbid	$⊢ φ \to (k \in (B ∖ {supp}_{Y} (G)) \to (F \circ G) (k) = Z)$
30	29	imp	$⊢ (φ \land k \in (B ∖ {supp}_{Y} (G))) \to (F \circ G) (k) = Z$
31	8 30	suppss	$⊢ φ \to (F \circ G) supp Z \subseteq G supp Y$

Metamath Proof Explorer

Theorem suppcoss

Proof