# 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}=\mathrm{LHyp}\left({K}\right)$
dihintcl.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
Assertion dihintcl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \bigcap {S}\in \mathrm{ran}{I}$

### Proof

Step Hyp Ref Expression
1 dihintcl.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dihintcl.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
3 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
4 3 1 2 dihfn ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}Fn{\mathrm{Base}}_{{K}}$
5 3 1 2 dihdm ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{dom}{I}={\mathrm{Base}}_{{K}}$
6 5 fneq2d ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left({I}Fn\mathrm{dom}{I}↔{I}Fn{\mathrm{Base}}_{{K}}\right)$
7 4 6 mpbird ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}Fn\mathrm{dom}{I}$
8 7 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {I}Fn\mathrm{dom}{I}$
9 cnvimass ${⊢}{{I}}^{-1}\left[{S}\right]\subseteq \mathrm{dom}{I}$
10 fnssres ${⊢}\left({I}Fn\mathrm{dom}{I}\wedge {{I}}^{-1}\left[{S}\right]\subseteq \mathrm{dom}{I}\right)\to \left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)Fn{{I}}^{-1}\left[{S}\right]$
11 8 9 10 sylancl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)Fn{{I}}^{-1}\left[{S}\right]$
12 fniinfv ${⊢}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)Fn{{I}}^{-1}\left[{S}\right]\to \bigcap _{{y}\in {{I}}^{-1}\left[{S}\right]}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)\left({y}\right)=\bigcap \mathrm{ran}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)$
13 11 12 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \bigcap _{{y}\in {{I}}^{-1}\left[{S}\right]}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)\left({y}\right)=\bigcap \mathrm{ran}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)$
14 df-ima ${⊢}{I}\left[{{I}}^{-1}\left[{S}\right]\right]=\mathrm{ran}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)$
15 4 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {I}Fn{\mathrm{Base}}_{{K}}$
16 dffn4 ${⊢}{I}Fn{\mathrm{Base}}_{{K}}↔{I}:{\mathrm{Base}}_{{K}}\underset{onto}{⟶}\mathrm{ran}{I}$
17 15 16 sylib ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {I}:{\mathrm{Base}}_{{K}}\underset{onto}{⟶}\mathrm{ran}{I}$
18 simprl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {S}\subseteq \mathrm{ran}{I}$
19 foimacnv ${⊢}\left({I}:{\mathrm{Base}}_{{K}}\underset{onto}{⟶}\mathrm{ran}{I}\wedge {S}\subseteq \mathrm{ran}{I}\right)\to {I}\left[{{I}}^{-1}\left[{S}\right]\right]={S}$
20 17 18 19 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {I}\left[{{I}}^{-1}\left[{S}\right]\right]={S}$
21 14 20 syl5eqr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \mathrm{ran}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)={S}$
22 21 inteqd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \bigcap \mathrm{ran}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)=\bigcap {S}$
23 13 22 eqtrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \bigcap _{{y}\in {{I}}^{-1}\left[{S}\right]}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)\left({y}\right)=\bigcap {S}$
24 simpl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
25 5 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \mathrm{dom}{I}={\mathrm{Base}}_{{K}}$
26 9 25 sseqtrid ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {{I}}^{-1}\left[{S}\right]\subseteq {\mathrm{Base}}_{{K}}$
27 simprr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {S}\ne \varnothing$
28 n0 ${⊢}{S}\ne \varnothing ↔\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {S}$
29 27 28 sylib ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {S}$
30 18 sselda ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {S}\right)\to {y}\in \mathrm{ran}{I}$
31 25 fneq2d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \left({I}Fn\mathrm{dom}{I}↔{I}Fn{\mathrm{Base}}_{{K}}\right)$
32 15 31 mpbird ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {I}Fn\mathrm{dom}{I}$
33 32 adantr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {S}\right)\to {I}Fn\mathrm{dom}{I}$
34 fvelrnb ${⊢}{I}Fn\mathrm{dom}{I}\to \left({y}\in \mathrm{ran}{I}↔\exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)={y}\right)$
35 33 34 syl ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {S}\right)\to \left({y}\in \mathrm{ran}{I}↔\exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)={y}\right)$
36 30 35 mpbid ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {S}\right)\to \exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)={y}$
37 fnfun ${⊢}{I}Fn{\mathrm{Base}}_{{K}}\to \mathrm{Fun}{I}$
38 15 37 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \mathrm{Fun}{I}$
39 fvimacnv ${⊢}\left(\mathrm{Fun}{I}\wedge {x}\in \mathrm{dom}{I}\right)\to \left({I}\left({x}\right)\in {S}↔{x}\in {{I}}^{-1}\left[{S}\right]\right)$
40 38 39 sylan ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {x}\in \mathrm{dom}{I}\right)\to \left({I}\left({x}\right)\in {S}↔{x}\in {{I}}^{-1}\left[{S}\right]\right)$
41 ne0i ${⊢}{x}\in {{I}}^{-1}\left[{S}\right]\to {{I}}^{-1}\left[{S}\right]\ne \varnothing$
42 40 41 syl6bi ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {x}\in \mathrm{dom}{I}\right)\to \left({I}\left({x}\right)\in {S}\to {{I}}^{-1}\left[{S}\right]\ne \varnothing \right)$
43 42 ex ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \left({x}\in \mathrm{dom}{I}\to \left({I}\left({x}\right)\in {S}\to {{I}}^{-1}\left[{S}\right]\ne \varnothing \right)\right)$
44 eleq1 ${⊢}{I}\left({x}\right)={y}\to \left({I}\left({x}\right)\in {S}↔{y}\in {S}\right)$
45 44 biimprd ${⊢}{I}\left({x}\right)={y}\to \left({y}\in {S}\to {I}\left({x}\right)\in {S}\right)$
46 45 imim1d ${⊢}{I}\left({x}\right)={y}\to \left(\left({I}\left({x}\right)\in {S}\to {{I}}^{-1}\left[{S}\right]\ne \varnothing \right)\to \left({y}\in {S}\to {{I}}^{-1}\left[{S}\right]\ne \varnothing \right)\right)$
47 43 46 syl9 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \left({I}\left({x}\right)={y}\to \left({x}\in \mathrm{dom}{I}\to \left({y}\in {S}\to {{I}}^{-1}\left[{S}\right]\ne \varnothing \right)\right)\right)$
48 47 com24 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \left({y}\in {S}\to \left({x}\in \mathrm{dom}{I}\to \left({I}\left({x}\right)={y}\to {{I}}^{-1}\left[{S}\right]\ne \varnothing \right)\right)\right)$
49 48 imp ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {S}\right)\to \left({x}\in \mathrm{dom}{I}\to \left({I}\left({x}\right)={y}\to {{I}}^{-1}\left[{S}\right]\ne \varnothing \right)\right)$
50 49 rexlimdv ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {S}\right)\to \left(\exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)={y}\to {{I}}^{-1}\left[{S}\right]\ne \varnothing \right)$
51 36 50 mpd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {S}\right)\to {{I}}^{-1}\left[{S}\right]\ne \varnothing$
52 29 51 exlimddv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {{I}}^{-1}\left[{S}\right]\ne \varnothing$
53 eqid ${⊢}\mathrm{glb}\left({K}\right)=\mathrm{glb}\left({K}\right)$
54 3 53 1 2 dihglb ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({{I}}^{-1}\left[{S}\right]\subseteq {\mathrm{Base}}_{{K}}\wedge {{I}}^{-1}\left[{S}\right]\ne \varnothing \right)\right)\to {I}\left(\mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right)\right)=\bigcap _{{y}\in {{I}}^{-1}\left[{S}\right]}{I}\left({y}\right)$
55 24 26 52 54 syl12anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {I}\left(\mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right)\right)=\bigcap _{{y}\in {{I}}^{-1}\left[{S}\right]}{I}\left({y}\right)$
56 fvres ${⊢}{y}\in {{I}}^{-1}\left[{S}\right]\to \left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)\left({y}\right)={I}\left({y}\right)$
57 56 iineq2i ${⊢}\bigcap _{{y}\in {{I}}^{-1}\left[{S}\right]}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)\left({y}\right)=\bigcap _{{y}\in {{I}}^{-1}\left[{S}\right]}{I}\left({y}\right)$
58 55 57 syl6eqr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {I}\left(\mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right)\right)=\bigcap _{{y}\in {{I}}^{-1}\left[{S}\right]}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)\left({y}\right)$
59 hlclat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{CLat}$
60 59 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {K}\in \mathrm{CLat}$
61 3 53 clatglbcl ${⊢}\left({K}\in \mathrm{CLat}\wedge {{I}}^{-1}\left[{S}\right]\subseteq {\mathrm{Base}}_{{K}}\right)\to \mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right)\in {\mathrm{Base}}_{{K}}$
62 60 26 61 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right)\in {\mathrm{Base}}_{{K}}$
63 3 1 2 dihcl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right)\in {\mathrm{Base}}_{{K}}\right)\to {I}\left(\mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right)\right)\in \mathrm{ran}{I}$
64 62 63 syldan ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {I}\left(\mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right)\right)\in \mathrm{ran}{I}$
65 58 64 eqeltrrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \bigcap _{{y}\in {{I}}^{-1}\left[{S}\right]}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)\left({y}\right)\in \mathrm{ran}{I}$
66 23 65 eqeltrrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \bigcap {S}\in \mathrm{ran}{I}$