fmco

Description: Composition of image filters. (Contributed by Mario Carneiro, 27-Aug-2015)

		Ref	Expression
	Assertion	fmco	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to (X FilMap (F \circ G)) (B) = (X FilMap F) ((Y FilMap G) (B))$

Proof

Step	Hyp	Ref	Expression
1		simpl3	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to B \in fBas (Z)$
2		ssfg	$⊢ B \in fBas (Z) \to B \subseteq Z filGen B$
3	1 2	syl	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to B \subseteq Z filGen B$
4	3	sseld	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to (u \in B \to u \in (Z filGen B))$
5		simpl2	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to Y \in W$
6		simprr	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to G : Z ⟶ Y$
7		eqid	$⊢ Z filGen B = Z filGen B$
8	7	imaelfm	$⊢ ((Y \in W \land B \in fBas (Z) \land G : Z ⟶ Y) \land u \in (Z filGen B)) \to G [u] \in (Y FilMap G) (B)$
9	8	ex	$⊢ (Y \in W \land B \in fBas (Z) \land G : Z ⟶ Y) \to (u \in (Z filGen B) \to G [u] \in (Y FilMap G) (B))$
10	5 1 6 9	syl3anc	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to (u \in (Z filGen B) \to G [u] \in (Y FilMap G) (B))$
11	4 10	syld	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to (u \in B \to G [u] \in (Y FilMap G) (B))$
12	11	imp	$⊢ (((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \land u \in B) \to G [u] \in (Y FilMap G) (B)$
13		imaeq2	$⊢ t = G [u] \to F [t] = F [G [u]]$
14		imaco	$⊢ (F \circ G) [u] = F [G [u]]$
15	13 14	eqtr4di	$⊢ t = G [u] \to F [t] = (F \circ G) [u]$
16	15	sseq1d	$⊢ t = G [u] \to (F [t] \subseteq s \leftrightarrow (F \circ G) [u] \subseteq s)$
17	16	rspcev	$⊢ (G [u] \in (Y FilMap G) (B) \land (F \circ G) [u] \subseteq s) \to \exists t \in (Y FilMap G) (B) F [t] \subseteq s$
18	17	ex	$⊢ G [u] \in (Y FilMap G) (B) \to ((F \circ G) [u] \subseteq s \to \exists t \in (Y FilMap G) (B) F [t] \subseteq s)$
19	12 18	syl	$⊢ (((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \land u \in B) \to ((F \circ G) [u] \subseteq s \to \exists t \in (Y FilMap G) (B) F [t] \subseteq s)$
20	19	rexlimdva	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to (\exists u \in B (F \circ G) [u] \subseteq s \to \exists t \in (Y FilMap G) (B) F [t] \subseteq s)$
21		elfm	$⊢ (Y \in W \land B \in fBas (Z) \land G : Z ⟶ Y) \to (t \in (Y FilMap G) (B) \leftrightarrow (t \subseteq Y \land \exists u \in B G [u] \subseteq t))$
22	5 1 6 21	syl3anc	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to (t \in (Y FilMap G) (B) \leftrightarrow (t \subseteq Y \land \exists u \in B G [u] \subseteq t))$
23		sstr2	$⊢ (F \circ G) [u] \subseteq F [t] \to (F [t] \subseteq s \to (F \circ G) [u] \subseteq s)$
24		imass2	$⊢ G [u] \subseteq t \to F [G [u]] \subseteq F [t]$
25	14 24	eqsstrid	$⊢ G [u] \subseteq t \to (F \circ G) [u] \subseteq F [t]$
26	23 25	syl11	$⊢ F [t] \subseteq s \to (G [u] \subseteq t \to (F \circ G) [u] \subseteq s)$
27	26	reximdv	$⊢ F [t] \subseteq s \to (\exists u \in B G [u] \subseteq t \to \exists u \in B (F \circ G) [u] \subseteq s)$
28	27	com12	$⊢ \exists u \in B G [u] \subseteq t \to (F [t] \subseteq s \to \exists u \in B (F \circ G) [u] \subseteq s)$
29	28	adantl	$⊢ (t \subseteq Y \land \exists u \in B G [u] \subseteq t) \to (F [t] \subseteq s \to \exists u \in B (F \circ G) [u] \subseteq s)$
30	22 29	biimtrdi	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to (t \in (Y FilMap G) (B) \to (F [t] \subseteq s \to \exists u \in B (F \circ G) [u] \subseteq s))$
31	30	rexlimdv	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to (\exists t \in (Y FilMap G) (B) F [t] \subseteq s \to \exists u \in B (F \circ G) [u] \subseteq s)$
32	20 31	impbid	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to (\exists u \in B (F \circ G) [u] \subseteq s \leftrightarrow \exists t \in (Y FilMap G) (B) F [t] \subseteq s)$
33	32	anbi2d	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to ((s \subseteq X \land \exists u \in B (F \circ G) [u] \subseteq s) \leftrightarrow (s \subseteq X \land \exists t \in (Y FilMap G) (B) F [t] \subseteq s))$
34		simpl1	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to X \in V$
35		fco	$⊢ (F : Y ⟶ X \land G : Z ⟶ Y) \to (F \circ G) : Z ⟶ X$
36	35	adantl	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to (F \circ G) : Z ⟶ X$
37		elfm	$⊢ (X \in V \land B \in fBas (Z) \land (F \circ G) : Z ⟶ X) \to (s \in (X FilMap (F \circ G)) (B) \leftrightarrow (s \subseteq X \land \exists u \in B (F \circ G) [u] \subseteq s))$
38	34 1 36 37	syl3anc	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to (s \in (X FilMap (F \circ G)) (B) \leftrightarrow (s \subseteq X \land \exists u \in B (F \circ G) [u] \subseteq s))$
39		fmfil	$⊢ (Y \in W \land B \in fBas (Z) \land G : Z ⟶ Y) \to (Y FilMap G) (B) \in Fil (Y)$
40	5 1 6 39	syl3anc	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to (Y FilMap G) (B) \in Fil (Y)$
41		filfbas	$⊢ (Y FilMap G) (B) \in Fil (Y) \to (Y FilMap G) (B) \in fBas (Y)$
42	40 41	syl	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to (Y FilMap G) (B) \in fBas (Y)$
43		simprl	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to F : Y ⟶ X$
44		elfm	$⊢ (X \in V \land (Y FilMap G) (B) \in fBas (Y) \land F : Y ⟶ X) \to (s \in (X FilMap F) ((Y FilMap G) (B)) \leftrightarrow (s \subseteq X \land \exists t \in (Y FilMap G) (B) F [t] \subseteq s))$
45	34 42 43 44	syl3anc	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to (s \in (X FilMap F) ((Y FilMap G) (B)) \leftrightarrow (s \subseteq X \land \exists t \in (Y FilMap G) (B) F [t] \subseteq s))$
46	33 38 45	3bitr4d	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to (s \in (X FilMap (F \circ G)) (B) \leftrightarrow s \in (X FilMap F) ((Y FilMap G) (B)))$
47	46	eqrdv	$⊢ ((X \in V \land Y \in W \land B \in fBas (Z)) \land (F : Y ⟶ X \land G : Z ⟶ Y)) \to (X FilMap (F \circ G)) (B) = (X FilMap F) ((Y FilMap G) (B))$

Metamath Proof Explorer

Theorem fmco

Proof