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 ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
Assertion psubclinN ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) → ( 𝑋 ∩ 𝑌 ) ∈ 𝐶 )

Proof

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