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 syl6bi
 |-  ( ( ( ( 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 )