Metamath Proof Explorer

Theorem dihintcl

Description: The intersection of closed subspaces (the range of isomorphism H) is a closed subspace. (Contributed by NM, 14-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 dihintcl.h 
 |-  H = ( LHyp ` K )
2 dihintcl.i 
 |-  I = ( ( DIsoH ` K ) ` W )
3 eqid 
 |-  ( Base ` K ) = ( Base ` K )
4 3 1 2 dihfn 
 |-  ( ( K e. HL /\ W e. H ) -> I Fn ( Base ` K ) )
5 3 1 2 dihdm 
 |-  ( ( K e. HL /\ W e. H ) -> dom I = ( Base ` K ) )
6 5 fneq2d 
 |-  ( ( K e. HL /\ W e. H ) -> ( I Fn dom I <-> I Fn ( Base ` K ) ) )
7 4 6 mpbird 
 |-  ( ( K e. HL /\ W e. H ) -> I Fn dom I )
8 7 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> I Fn dom I )
9 cnvimass 
 |-  ( `' I " S ) C_ dom I
10 fnssres 
 |-  ( ( I Fn dom I /\ ( `' I " S ) C_ dom I ) -> ( I |` ( `' I " S ) ) Fn ( `' I " S ) )
11 8 9 10 sylancl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( I |` ( `' I " S ) ) Fn ( `' I " S ) )
12 fniinfv 
 |-  ( ( I |` ( `' I " S ) ) Fn ( `' I " S ) -> |^|_ y e. ( `' I " S ) ( ( I |` ( `' I " S ) ) ` y ) = |^| ran ( I |` ( `' I " S ) ) )
13 11 12 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> |^|_ y e. ( `' I " S ) ( ( I |` ( `' I " S ) ) ` y ) = |^| ran ( I |` ( `' I " S ) ) )
14 df-ima 
 |-  ( I " ( `' I " S ) ) = ran ( I |` ( `' I " S ) )
15 4 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> I Fn ( Base ` K ) )
16 dffn4 
 |-  ( I Fn ( Base ` K ) <-> I : ( Base ` K ) -onto-> ran I )
17 15 16 sylib 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> I : ( Base ` K ) -onto-> ran I )
18 simprl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> S C_ ran I )
19 foimacnv 
 |-  ( ( I : ( Base ` K ) -onto-> ran I /\ S C_ ran I ) -> ( I " ( `' I " S ) ) = S )
20 17 18 19 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( I " ( `' I " S ) ) = S )
21 14 20 eqtr3id 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ran ( I |` ( `' I " S ) ) = S )
22 21 inteqd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> |^| ran ( I |` ( `' I " S ) ) = |^| S )
23 13 22 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> |^|_ y e. ( `' I " S ) ( ( I |` ( `' I " S ) ) ` y ) = |^| S )
24 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( K e. HL /\ W e. H ) )
25 5 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> dom I = ( Base ` K ) )
26 9 25 sseqtrid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( `' I " S ) C_ ( Base ` K ) )
27 simprr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> S =/= (/) )
28 n0 
 |-  ( S =/= (/) <-> E. y y e. S )
29 27 28 sylib 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> E. y y e. S )
30 18 sselda 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. S ) -> y e. ran I )
31 25 fneq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( I Fn dom I <-> I Fn ( Base ` K ) ) )
32 15 31 mpbird 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> I Fn dom I )
33 32 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. S ) -> I Fn dom I )
34 fvelrnb 
 |-  ( I Fn dom I -> ( y e. ran I <-> E. x e. dom I ( I ` x ) = y ) )
35 33 34 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 ) )
36 30 35 mpbid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. S ) -> E. x e. dom I ( I ` x ) = y )
37 fnfun 
 |-  ( I Fn ( Base ` K ) -> Fun I )
38 15 37 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> Fun I )
39 fvimacnv 
 |-  ( ( Fun I /\ x e. dom I ) -> ( ( I ` x ) e. S <-> x e. ( `' I " S ) ) )
40 38 39 sylan 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ x e. dom I ) -> ( ( I ` x ) e. S <-> x e. ( `' I " S ) ) )
41 ne0i 
 |-  ( x e. ( `' I " S ) -> ( `' I " S ) =/= (/) )
42 40 41 syl6bi 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ x e. dom I ) -> ( ( I ` x ) e. S -> ( `' I " S ) =/= (/) ) )
43 42 ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( x e. dom I -> ( ( I ` x ) e. S -> ( `' I " S ) =/= (/) ) ) )
44 eleq1 
 |-  ( ( I ` x ) = y -> ( ( I ` x ) e. S <-> y e. S ) )
45 44 biimprd 
 |-  ( ( I ` x ) = y -> ( y e. S -> ( I ` x ) e. S ) )
46 45 imim1d 
 |-  ( ( I ` x ) = y -> ( ( ( I ` x ) e. S -> ( `' I " S ) =/= (/) ) -> ( y e. S -> ( `' I " S ) =/= (/) ) ) )
47 43 46 syl9 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( ( I ` x ) = y -> ( x e. dom I -> ( y e. S -> ( `' I " S ) =/= (/) ) ) ) )
48 47 com24 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( y e. S -> ( x e. dom I -> ( ( I ` x ) = y -> ( `' I " S ) =/= (/) ) ) ) )
49 48 imp 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. S ) -> ( x e. dom I -> ( ( I ` x ) = y -> ( `' I " S ) =/= (/) ) ) )
50 49 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 ) =/= (/) ) )
51 36 50 mpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. S ) -> ( `' I " S ) =/= (/) )
52 29 51 exlimddv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( `' I " S ) =/= (/) )
53 eqid 
 |-  ( glb ` K ) = ( glb ` K )
54 3 53 1 2 dihglb 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( `' I " S ) C_ ( Base ` K ) /\ ( `' I " S ) =/= (/) ) ) -> ( I ` ( ( glb ` K ) ` ( `' I " S ) ) ) = |^|_ y e. ( `' I " S ) ( I ` y ) )
55 24 26 52 54 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( I ` ( ( glb ` K ) ` ( `' I " S ) ) ) = |^|_ y e. ( `' I " S ) ( I ` y ) )
56 fvres 
 |-  ( y e. ( `' I " S ) -> ( ( I |` ( `' I " S ) ) ` y ) = ( I ` y ) )
57 56 iineq2i 
 |-  |^|_ y e. ( `' I " S ) ( ( I |` ( `' I " S ) ) ` y ) = |^|_ y e. ( `' I " S ) ( I ` y )
58 55 57 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 ) )
59 hlclat 
 |-  ( K e. HL -> K e. CLat )
60 59 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> K e. CLat )
61 3 53 clatglbcl 
 |-  ( ( K e. CLat /\ ( `' I " S ) C_ ( Base ` K ) ) -> ( ( glb ` K ) ` ( `' I " S ) ) e. ( Base ` K ) )
62 60 26 61 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( ( glb ` K ) ` ( `' I " S ) ) e. ( Base ` K ) )
63 3 1 2 dihcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( glb ` K ) ` ( `' I " S ) ) e. ( Base ` K ) ) -> ( I ` ( ( glb ` K ) ` ( `' I " S ) ) ) e. ran I )
64 62 63 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( I ` ( ( glb ` K ) ` ( `' I " S ) ) ) e. ran I )
65 58 64 eqeltrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> |^|_ y e. ( `' I " S ) ( ( I |` ( `' I " S ) ) ` y ) e. ran I )
66 23 65 eqeltrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> |^| S e. ran I )