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 e. HL /\ X e. C /\ Y e. C ) -> ( X i^i Y ) e. C )

Proof

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