Metamath Proof Explorer

Theorem dibintclN

Description: The intersection of partial isomorphism B closed subspaces is a closed subspace. (Contributed by NM, 8-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dibintcl.h 
|- H = ( LHyp ` K )
dibintcl.i 
|- I = ( ( DIsoB ` K ) ` W )
Assertion dibintclN 
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> |^| S e. ran I )

Proof

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