Metamath Proof Explorer


Theorem diaintclN

Description: The intersection of partial isomorphism A closed subspaces is a closed subspace. (Contributed by NM, 3-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses diaintcl.h H = LHyp K
diaintcl.i I = DIsoA K W
Assertion diaintclN K HL W H S ran I S S ran I

Proof

Step Hyp Ref Expression
1 diaintcl.h H = LHyp K
2 diaintcl.i I = DIsoA K W
3 1 2 diaf11N K HL W H I : dom I 1-1 onto ran I
4 3 adantr K HL W H S ran I S I : dom I 1-1 onto ran I
5 f1ofn I : dom I 1-1 onto ran I I Fn dom I
6 4 5 syl K HL W H S ran I S I Fn dom I
7 cnvimass I -1 S dom I
8 fnssres I Fn dom I I -1 S dom I I I -1 S Fn I -1 S
9 6 7 8 sylancl K HL W H S ran I S I I -1 S Fn I -1 S
10 fniinfv I I -1 S Fn I -1 S y I -1 S I I -1 S y = ran I I -1 S
11 9 10 syl K HL W H S ran I S y I -1 S I I -1 S y = ran I I -1 S
12 df-ima I I -1 S = ran I I -1 S
13 f1ofo I : dom I 1-1 onto ran I I : dom I onto ran I
14 3 13 syl K HL W H I : dom I onto ran I
15 14 adantr K HL W H S ran I S I : dom I onto ran I
16 simprl K HL W H S ran I S S ran I
17 foimacnv I : dom I onto ran I S ran I I I -1 S = S
18 15 16 17 syl2anc K HL W H S ran I S I I -1 S = S
19 12 18 eqtr3id K HL W H S ran I S ran I I -1 S = S
20 19 inteqd K HL W H S ran I S ran I I -1 S = S
21 11 20 eqtrd K HL W H S ran I S y I -1 S I I -1 S y = S
22 simpl K HL W H S ran I S K HL W H
23 7 a1i K HL W H S ran I S I -1 S dom I
24 simprr K HL W H S ran I S S
25 n0 S y y S
26 24 25 sylib K HL W H S ran I S y y S
27 16 sselda K HL W H S ran I S y S y ran I
28 3 ad2antrr K HL W H S ran I S y S I : dom I 1-1 onto ran I
29 28 5 syl K HL W H S ran I S y S I Fn dom I
30 fvelrnb I Fn dom I y ran I x dom I I x = y
31 29 30 syl K HL W H S ran I S y S y ran I x dom I I x = y
32 27 31 mpbid K HL W H S ran I S y S x dom I I x = y
33 f1ofun I : dom I 1-1 onto ran I Fun I
34 3 33 syl K HL W H Fun I
35 34 adantr K HL W H S ran I S Fun I
36 fvimacnv Fun I x dom I I x S x I -1 S
37 35 36 sylan K HL W H S ran I S x dom I I x S x I -1 S
38 ne0i x I -1 S I -1 S
39 37 38 syl6bi K HL W H S ran I S x dom I I x S I -1 S
40 39 ex K HL W H S ran I S x dom I I x S I -1 S
41 eleq1 I x = y I x S y S
42 41 biimprd I x = y y S I x S
43 42 imim1d I x = y I x S I -1 S y S I -1 S
44 40 43 syl9 K HL W H S ran I S I x = y x dom I y S I -1 S
45 44 com24 K HL W H S ran I S y S x dom I I x = y I -1 S
46 45 imp K HL W H S ran I S y S x dom I I x = y I -1 S
47 46 rexlimdv K HL W H S ran I S y S x dom I I x = y I -1 S
48 32 47 mpd K HL W H S ran I S y S I -1 S
49 26 48 exlimddv K HL W H S ran I S I -1 S
50 eqid glb K = glb K
51 50 1 2 diaglbN K HL W H I -1 S dom I I -1 S I glb K I -1 S = y I -1 S I y
52 22 23 49 51 syl12anc K HL W H S ran I S I glb K I -1 S = y I -1 S I y
53 fvres y I -1 S I I -1 S y = I y
54 53 iineq2i y I -1 S I I -1 S y = y I -1 S I y
55 52 54 eqtr4di K HL W H S ran I S I glb K I -1 S = y I -1 S I I -1 S y
56 hlclat K HL K CLat
57 56 ad2antrr K HL W H S ran I S K CLat
58 eqid Base K = Base K
59 eqid K = K
60 58 59 1 2 diadm K HL W H dom I = x Base K | x K W
61 ssrab2 x Base K | x K W Base K
62 60 61 eqsstrdi K HL W H dom I Base K
63 62 adantr K HL W H S ran I S dom I Base K
64 7 63 sstrid K HL W H S ran I S I -1 S Base K
65 58 50 clatglbcl K CLat I -1 S Base K glb K I -1 S Base K
66 57 64 65 syl2anc K HL W H S ran I S glb K I -1 S Base K
67 n0 I -1 S y y I -1 S
68 49 67 sylib K HL W H S ran I S y y I -1 S
69 hllat K HL K Lat
70 69 ad3antrrr K HL W H S ran I S y I -1 S K Lat
71 66 adantr K HL W H S ran I S y I -1 S glb K I -1 S Base K
72 64 sselda K HL W H S ran I S y I -1 S y Base K
73 58 1 lhpbase W H W Base K
74 73 ad3antlr K HL W H S ran I S y I -1 S W Base K
75 56 ad3antrrr K HL W H S ran I S y I -1 S K CLat
76 60 adantr K HL W H S ran I S dom I = x Base K | x K W
77 7 76 sseqtrid K HL W H S ran I S I -1 S x Base K | x K W
78 77 61 sstrdi K HL W H S ran I S I -1 S Base K
79 78 adantr K HL W H S ran I S y I -1 S I -1 S Base K
80 simpr K HL W H S ran I S y I -1 S y I -1 S
81 58 59 50 clatglble K CLat I -1 S Base K y I -1 S glb K I -1 S K y
82 75 79 80 81 syl3anc K HL W H S ran I S y I -1 S glb K I -1 S K y
83 7 sseli y I -1 S y dom I
84 83 adantl K HL W H S ran I S y I -1 S y dom I
85 58 59 1 2 diaeldm K HL W H y dom I y Base K y K W
86 85 ad2antrr K HL W H S ran I S y I -1 S y dom I y Base K y K W
87 84 86 mpbid K HL W H S ran I S y I -1 S y Base K y K W
88 87 simprd K HL W H S ran I S y I -1 S y K W
89 58 59 70 71 72 74 82 88 lattrd K HL W H S ran I S y I -1 S glb K I -1 S K W
90 68 89 exlimddv K HL W H S ran I S glb K I -1 S K W
91 58 59 1 2 diaeldm K HL W H glb K I -1 S dom I glb K I -1 S Base K glb K I -1 S K W
92 91 adantr K HL W H S ran I S glb K I -1 S dom I glb K I -1 S Base K glb K I -1 S K W
93 66 90 92 mpbir2and K HL W H S ran I S glb K I -1 S dom I
94 1 2 diaclN K HL W H glb K I -1 S dom I I glb K I -1 S ran I
95 93 94 syldan K HL W H S ran I S I glb K I -1 S ran I
96 55 95 eqeltrrd K HL W H S ran I S y I -1 S I I -1 S y ran I
97 21 96 eqeltrrd K HL W H S ran I S S ran I