Metamath Proof Explorer


Theorem fmco

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

Ref Expression
Assertion fmco X V Y W B fBas Z F : Y X G : Z Y X FilMap F G B = X FilMap F Y FilMap G B

Proof

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