Metamath Proof Explorer

Theorem psubclinN

Description: The intersection of two closed subspaces is closed. (Contributed by NM, 25-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypothesis psubclin.c ⊢ C = PSubCl ⁡ K
Assertion psubclinN ⊢ K ∈ HL ∧ X ∈ C ∧ Y ∈ C → X ∩ Y ∈ C

Proof

Step Hyp Ref Expression
1 psubclin.c ⊢ C = PSubCl ⁡ K
2 simp1 ⊢ K ∈ HL ∧ X ∈ C ∧ Y ∈ C → K ∈ HL
3 hlclat ⊢ K ∈ HL → K ∈ CLat
4 3 3ad2ant1 ⊢ K ∈ HL ∧ X ∈ C ∧ Y ∈ C → K ∈ CLat
5 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
6 5 1 psubclssatN ⊢ K ∈ HL ∧ X ∈ C → X ⊆ Atoms ⁡ K
7 6 3adant3 ⊢ K ∈ HL ∧ X ∈ C ∧ Y ∈ C → X ⊆ Atoms ⁡ K
8 eqid ⊢ Base K = Base K
9 8 5 atssbase ⊢ Atoms ⁡ K ⊆ Base K
10 7 9 sstrdi ⊢ K ∈ HL ∧ X ∈ C ∧ Y ∈ C → X ⊆ Base K
11 eqid ⊢ lub ⁡ K = lub ⁡ K
12 8 11 clatlubcl ⊢ K ∈ CLat ∧ X ⊆ Base K → lub ⁡ K ⁡ X ∈ Base K
13 4 10 12 syl2anc ⊢ K ∈ HL ∧ X ∈ C ∧ Y ∈ C → lub ⁡ K ⁡ X ∈ Base K
14 5 1 psubclssatN ⊢ K ∈ HL ∧ Y ∈ C → Y ⊆ Atoms ⁡ K
15 14 3adant2 ⊢ K ∈ HL ∧ X ∈ C ∧ Y ∈ C → Y ⊆ Atoms ⁡ K
16 15 9 sstrdi ⊢ K ∈ HL ∧ X ∈ C ∧ Y ∈ C → Y ⊆ Base K
17 8 11 clatlubcl ⊢ K ∈ CLat ∧ Y ⊆ Base K → lub ⁡ K ⁡ Y ∈ Base K
18 4 16 17 syl2anc ⊢ K ∈ HL ∧ X ∈ C ∧ Y ∈ C → lub ⁡ K ⁡ Y ∈ Base K
19 eqid ⊢ meet ⁡ K = meet ⁡ K
20 eqid ⊢ pmap ⁡ K = pmap ⁡ K
21 8 19 5 20 pmapmeet ⊢ K ∈ HL ∧ lub ⁡ K ⁡ X ∈ Base K ∧ lub ⁡ K ⁡ Y ∈ Base K → pmap ⁡ K ⁡ lub ⁡ K ⁡ X meet ⁡ K lub ⁡ K ⁡ Y = pmap ⁡ K ⁡ lub ⁡ K ⁡ X ∩ pmap ⁡ K ⁡ lub ⁡ K ⁡ Y
22 2 13 18 21 syl3anc ⊢ K ∈ HL ∧ X ∈ C ∧ Y ∈ C → pmap ⁡ K ⁡ lub ⁡ K ⁡ X meet ⁡ K lub ⁡ K ⁡ Y = pmap ⁡ K ⁡ lub ⁡ K ⁡ X ∩ pmap ⁡ K ⁡ lub ⁡ K ⁡ Y
23 11 20 1 pmapidclN ⊢ K ∈ HL ∧ X ∈ C → pmap ⁡ K ⁡ lub ⁡ K ⁡ X = X
24 23 3adant3 ⊢ K ∈ HL ∧ X ∈ C ∧ Y ∈ C → pmap ⁡ K ⁡ lub ⁡ K ⁡ X = X
25 11 20 1 pmapidclN ⊢ K ∈ HL ∧ Y ∈ C → pmap ⁡ K ⁡ lub ⁡ K ⁡ Y = Y
26 25 3adant2 ⊢ K ∈ HL ∧ X ∈ C ∧ Y ∈ C → pmap ⁡ K ⁡ lub ⁡ K ⁡ Y = Y
27 24 26 ineq12d ⊢ K ∈ HL ∧ X ∈ C ∧ Y ∈ C → pmap ⁡ K ⁡ lub ⁡ K ⁡ X ∩ pmap ⁡ K ⁡ lub ⁡ K ⁡ Y = X ∩ Y
28 22 27 eqtrd ⊢ K ∈ HL ∧ X ∈ C ∧ Y ∈ C → pmap ⁡ K ⁡ lub ⁡ K ⁡ X meet ⁡ K lub ⁡ K ⁡ Y = X ∩ Y
29 hllat ⊢ K ∈ HL → K ∈ Lat
30 29 3ad2ant1 ⊢ K ∈ HL ∧ X ∈ C ∧ Y ∈ C → K ∈ Lat
31 8 19 latmcl ⊢ K ∈ Lat ∧ lub ⁡ K ⁡ X ∈ Base K ∧ lub ⁡ K ⁡ Y ∈ Base K → lub ⁡ K ⁡ X meet ⁡ K lub ⁡ K ⁡ Y ∈ Base K
32 30 13 18 31 syl3anc ⊢ K ∈ HL ∧ X ∈ C ∧ Y ∈ C → lub ⁡ K ⁡ X meet ⁡ K lub ⁡ K ⁡ Y ∈ Base K
33 8 20 1 pmapsubclN ⊢ K ∈ HL ∧ lub ⁡ K ⁡ X meet ⁡ K lub ⁡ K ⁡ Y ∈ Base K → pmap ⁡ K ⁡ lub ⁡ K ⁡ X meet ⁡ K lub ⁡ K ⁡ Y ∈ C
34 2 32 33 syl2anc ⊢ K ∈ HL ∧ X ∈ C ∧ Y ∈ C → pmap ⁡ K ⁡ lub ⁡ K ⁡ X meet ⁡ K lub ⁡ K ⁡ Y ∈ C
35 28 34 eqeltrrd ⊢ K ∈ HL ∧ X ∈ C ∧ Y ∈ C → X ∩ Y ∈ C