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 ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihintcl.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dihintcl ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ∩ 𝑆 ∈ ran 𝐼 )

Proof

Step Hyp Ref Expression
1 dihintcl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dihintcl.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
4 3 1 2 dihfn ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn ( Base ‘ 𝐾 ) )
5 3 1 2 dihdm ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → dom 𝐼 = ( Base ‘ 𝐾 ) )
6 5 fneq2d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 Fn dom 𝐼 ↔ 𝐼 Fn ( Base ‘ 𝐾 ) ) )
7 4 6 mpbird ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn dom 𝐼 )
8 7 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → 𝐼 Fn dom 𝐼 )
9 cnvimass ⊢ ( ◡ 𝐼 “ 𝑆 ) ⊆ dom 𝐼
10 fnssres ⊢ ( ( 𝐼 Fn dom 𝐼 ∧ ( ◡ 𝐼 “ 𝑆 ) ⊆ dom 𝐼 ) → ( 𝐼 ↾ ( ◡ 𝐼 “ 𝑆 ) ) Fn ( ◡ 𝐼 “ 𝑆 ) )
11 8 9 10 sylancl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( 𝐼 ↾ ( ◡ 𝐼 “ 𝑆 ) ) Fn ( ◡ 𝐼 “ 𝑆 ) )
12 fniinfv ⊢ ( ( 𝐼 ↾ ( ◡ 𝐼 “ 𝑆 ) ) Fn ( ◡ 𝐼 “ 𝑆 ) → ∩ 𝑦 ∈ ( ◡ 𝐼 “ 𝑆 ) ( ( 𝐼 ↾ ( ◡ 𝐼 “ 𝑆 ) ) ‘ 𝑦 ) = ∩ ran ( 𝐼 ↾ ( ◡ 𝐼 “ 𝑆 ) ) )
13 11 12 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ∩ 𝑦 ∈ ( ◡ 𝐼 “ 𝑆 ) ( ( 𝐼 ↾ ( ◡ 𝐼 “ 𝑆 ) ) ‘ 𝑦 ) = ∩ ran ( 𝐼 ↾ ( ◡ 𝐼 “ 𝑆 ) ) )
14 df-ima ⊢ ( 𝐼 “ ( ◡ 𝐼 “ 𝑆 ) ) = ran ( 𝐼 ↾ ( ◡ 𝐼 “ 𝑆 ) )
15 4 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → 𝐼 Fn ( Base ‘ 𝐾 ) )
16 dffn4 ⊢ ( 𝐼 Fn ( Base ‘ 𝐾 ) ↔ 𝐼 : ( Base ‘ 𝐾 ) –onto→ ran 𝐼 )
17 15 16 sylib ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → 𝐼 : ( Base ‘ 𝐾 ) –onto→ ran 𝐼 )
18 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → 𝑆 ⊆ ran 𝐼 )
19 foimacnv ⊢ ( ( 𝐼 : ( Base ‘ 𝐾 ) –onto→ ran 𝐼 ∧ 𝑆 ⊆ ran 𝐼 ) → ( 𝐼 “ ( ◡ 𝐼 “ 𝑆 ) ) = 𝑆 )
20 17 18 19 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( 𝐼 “ ( ◡ 𝐼 “ 𝑆 ) ) = 𝑆 )
21 14 20 eqtr3id ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ran ( 𝐼 ↾ ( ◡ 𝐼 “ 𝑆 ) ) = 𝑆 )
22 21 inteqd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ∩ ran ( 𝐼 ↾ ( ◡ 𝐼 “ 𝑆 ) ) = ∩ 𝑆 )
23 13 22 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ∩ 𝑦 ∈ ( ◡ 𝐼 “ 𝑆 ) ( ( 𝐼 ↾ ( ◡ 𝐼 “ 𝑆 ) ) ‘ 𝑦 ) = ∩ 𝑆 )
24 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
25 5 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → dom 𝐼 = ( Base ‘ 𝐾 ) )
26 9 25 sseqtrid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( ◡ 𝐼 “ 𝑆 ) ⊆ ( Base ‘ 𝐾 ) )
27 simprr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → 𝑆 ≠ ∅ )
28 n0 ⊢ ( 𝑆 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝑆 )
29 27 28 sylib ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ∃ 𝑦 𝑦 ∈ 𝑆 )
30 18 sselda ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ ran 𝐼 )
31 25 fneq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( 𝐼 Fn dom 𝐼 ↔ 𝐼 Fn ( Base ‘ 𝐾 ) ) )
32 15 31 mpbird ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → 𝐼 Fn dom 𝐼 )
33 32 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ 𝑆 ) → 𝐼 Fn dom 𝐼 )
34 fvelrnb ⊢ ( 𝐼 Fn dom 𝐼 → ( 𝑦 ∈ ran 𝐼 ↔ ∃ 𝑥 ∈ dom 𝐼 ( 𝐼 ‘ 𝑥 ) = 𝑦 ) )
35 33 34 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑦 ∈ ran 𝐼 ↔ ∃ 𝑥 ∈ dom 𝐼 ( 𝐼 ‘ 𝑥 ) = 𝑦 ) )
36 30 35 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ 𝑆 ) → ∃ 𝑥 ∈ dom 𝐼 ( 𝐼 ‘ 𝑥 ) = 𝑦 )
37 fnfun ⊢ ( 𝐼 Fn ( Base ‘ 𝐾 ) → Fun 𝐼 )
38 15 37 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → Fun 𝐼 )
39 fvimacnv ⊢ ( ( Fun 𝐼 ∧ 𝑥 ∈ dom 𝐼 ) → ( ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ↔ 𝑥 ∈ ( ◡ 𝐼 “ 𝑆 ) ) )
40 38 39 sylan ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ dom 𝐼 ) → ( ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ↔ 𝑥 ∈ ( ◡ 𝐼 “ 𝑆 ) ) )
41 ne0i ⊢ ( 𝑥 ∈ ( ◡ 𝐼 “ 𝑆 ) → ( ◡ 𝐼 “ 𝑆 ) ≠ ∅ )
42 40 41 syl6bi ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ dom 𝐼 ) → ( ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 → ( ◡ 𝐼 “ 𝑆 ) ≠ ∅ ) )
43 42 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( 𝑥 ∈ dom 𝐼 → ( ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 → ( ◡ 𝐼 “ 𝑆 ) ≠ ∅ ) ) )
44 eleq1 ⊢ ( ( 𝐼 ‘ 𝑥 ) = 𝑦 → ( ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ↔ 𝑦 ∈ 𝑆 ) )
45 44 biimprd ⊢ ( ( 𝐼 ‘ 𝑥 ) = 𝑦 → ( 𝑦 ∈ 𝑆 → ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) )
46 45 imim1d ⊢ ( ( 𝐼 ‘ 𝑥 ) = 𝑦 → ( ( ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 → ( ◡ 𝐼 “ 𝑆 ) ≠ ∅ ) → ( 𝑦 ∈ 𝑆 → ( ◡ 𝐼 “ 𝑆 ) ≠ ∅ ) ) )
47 43 46 syl9 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( ( 𝐼 ‘ 𝑥 ) = 𝑦 → ( 𝑥 ∈ dom 𝐼 → ( 𝑦 ∈ 𝑆 → ( ◡ 𝐼 “ 𝑆 ) ≠ ∅ ) ) ) )
48 47 com24 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( 𝑦 ∈ 𝑆 → ( 𝑥 ∈ dom 𝐼 → ( ( 𝐼 ‘ 𝑥 ) = 𝑦 → ( ◡ 𝐼 “ 𝑆 ) ≠ ∅ ) ) ) )
49 48 imp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 ∈ dom 𝐼 → ( ( 𝐼 ‘ 𝑥 ) = 𝑦 → ( ◡ 𝐼 “ 𝑆 ) ≠ ∅ ) ) )
50 49 rexlimdv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ 𝑆 ) → ( ∃ 𝑥 ∈ dom 𝐼 ( 𝐼 ‘ 𝑥 ) = 𝑦 → ( ◡ 𝐼 “ 𝑆 ) ≠ ∅ ) )
51 36 50 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ 𝑆 ) → ( ◡ 𝐼 “ 𝑆 ) ≠ ∅ )
52 29 51 exlimddv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( ◡ 𝐼 “ 𝑆 ) ≠ ∅ )
53 eqid ⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
54 3 53 1 2 dihglb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ◡ 𝐼 “ 𝑆 ) ⊆ ( Base ‘ 𝐾 ) ∧ ( ◡ 𝐼 “ 𝑆 ) ≠ ∅ ) ) → ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ ( ◡ 𝐼 “ 𝑆 ) ) ) = ∩ 𝑦 ∈ ( ◡ 𝐼 “ 𝑆 ) ( 𝐼 ‘ 𝑦 ) )
55 24 26 52 54 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ ( ◡ 𝐼 “ 𝑆 ) ) ) = ∩ 𝑦 ∈ ( ◡ 𝐼 “ 𝑆 ) ( 𝐼 ‘ 𝑦 ) )
56 fvres ⊢ ( 𝑦 ∈ ( ◡ 𝐼 “ 𝑆 ) → ( ( 𝐼 ↾ ( ◡ 𝐼 “ 𝑆 ) ) ‘ 𝑦 ) = ( 𝐼 ‘ 𝑦 ) )
57 56 iineq2i ⊢ ∩ 𝑦 ∈ ( ◡ 𝐼 “ 𝑆 ) ( ( 𝐼 ↾ ( ◡ 𝐼 “ 𝑆 ) ) ‘ 𝑦 ) = ∩ 𝑦 ∈ ( ◡ 𝐼 “ 𝑆 ) ( 𝐼 ‘ 𝑦 )
58 55 57 eqtr4di ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ ( ◡ 𝐼 “ 𝑆 ) ) ) = ∩ 𝑦 ∈ ( ◡ 𝐼 “ 𝑆 ) ( ( 𝐼 ↾ ( ◡ 𝐼 “ 𝑆 ) ) ‘ 𝑦 ) )
59 hlclat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CLat )
60 59 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → 𝐾 ∈ CLat )
61 3 53 clatglbcl ⊢ ( ( 𝐾 ∈ CLat ∧ ( ◡ 𝐼 “ 𝑆 ) ⊆ ( Base ‘ 𝐾 ) ) → ( ( glb ‘ 𝐾 ) ‘ ( ◡ 𝐼 “ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) )
62 60 26 61 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( ( glb ‘ 𝐾 ) ‘ ( ◡ 𝐼 “ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) )
63 3 1 2 dihcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( glb ‘ 𝐾 ) ‘ ( ◡ 𝐼 “ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ ( ◡ 𝐼 “ 𝑆 ) ) ) ∈ ran 𝐼 )
64 62 63 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ ( ◡ 𝐼 “ 𝑆 ) ) ) ∈ ran 𝐼 )
65 58 64 eqeltrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ∩ 𝑦 ∈ ( ◡ 𝐼 “ 𝑆 ) ( ( 𝐼 ↾ ( ◡ 𝐼 “ 𝑆 ) ) ‘ 𝑦 ) ∈ ran 𝐼 )
66 23 65 eqeltrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ∩ 𝑆 ∈ ran 𝐼 )