Metamath Proof Explorer

Theorem ispsubcl2N

Description: Alternate predicate for "is a closed projective subspace". Remark in Holland95 p. 223. (Contributed by NM, 24-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pmapsubcl.b 
|- B = ( Base ` K )
pmapsubcl.m 
|- M = ( pmap ` K )
pmapsubcl.c 
|- C = ( PSubCl ` K )
Assertion ispsubcl2N 
|- ( K e. HL -> ( X e. C <-> E. y e. B X = ( M ` y ) ) )

Proof

Step Hyp Ref Expression
1 pmapsubcl.b 
 |-  B = ( Base ` K )
2 pmapsubcl.m 
 |-  M = ( pmap ` K )
3 pmapsubcl.c 
 |-  C = ( PSubCl ` K )
4 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
5 eqid 
 |-  ( _|_P ` K ) = ( _|_P ` K )
6 4 5 3 ispsubclN 
 |-  ( K e. HL -> ( X e. C <-> ( X C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) ) )
7 hlop 
 |-  ( K e. HL -> K e. OP )
8 7 adantr 
 |-  ( ( K e. HL /\ X C_ ( Atoms ` K ) ) -> K e. OP )
9 hlclat 
 |-  ( K e. HL -> K e. CLat )
10 9 adantr 
 |-  ( ( K e. HL /\ X C_ ( Atoms ` K ) ) -> K e. CLat )
11 4 5 polssatN 
 |-  ( ( K e. HL /\ X C_ ( Atoms ` K ) ) -> ( ( _|_P ` K ) ` X ) C_ ( Atoms ` K ) )
12 1 4 atssbase 
 |-  ( Atoms ` K ) C_ B
13 11 12 sstrdi 
 |-  ( ( K e. HL /\ X C_ ( Atoms ` K ) ) -> ( ( _|_P ` K ) ` X ) C_ B )
14 eqid 
 |-  ( lub ` K ) = ( lub ` K )
15 1 14 clatlubcl 
 |-  ( ( K e. CLat /\ ( ( _|_P ` K ) ` X ) C_ B ) -> ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) e. B )
16 10 13 15 syl2anc 
 |-  ( ( K e. HL /\ X C_ ( Atoms ` K ) ) -> ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) e. B )
17 eqid 
 |-  ( oc ` K ) = ( oc ` K )
18 1 17 opoccl 
 |-  ( ( K e. OP /\ ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) e. B ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) e. B )
19 8 16 18 syl2anc 
 |-  ( ( K e. HL /\ X C_ ( Atoms ` K ) ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) e. B )
20 19 ex 
 |-  ( K e. HL -> ( X C_ ( Atoms ` K ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) e. B ) )
21 20 adantrd 
 |-  ( K e. HL -> ( ( X C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) e. B ) )
22 14 17 4 2 5 polval2N 
 |-  ( ( K e. HL /\ ( ( _|_P ` K ) ` X ) C_ ( Atoms ` K ) ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) )
23 11 22 syldan 
 |-  ( ( K e. HL /\ X C_ ( Atoms ` K ) ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) )
24 23 ex 
 |-  ( K e. HL -> ( X C_ ( Atoms ` K ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) ) )
25 eqeq1 
 |-  ( ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X -> ( ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) <-> X = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) ) )
26 25 biimpcd 
 |-  ( ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) -> ( ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X -> X = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) ) )
27 24 26 syl6 
 |-  ( K e. HL -> ( X C_ ( Atoms ` K ) -> ( ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X -> X = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) ) ) )
28 27 impd 
 |-  ( K e. HL -> ( ( X C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) -> X = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) ) )
29 21 28 jcad 
 |-  ( K e. HL -> ( ( X C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) -> ( ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) e. B /\ X = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) ) ) )
30 fveq2 
 |-  ( y = ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) -> ( M ` y ) = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) )
31 30 rspceeqv 
 |-  ( ( ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) e. B /\ X = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) ) -> E. y e. B X = ( M ` y ) )
32 29 31 syl6 
 |-  ( K e. HL -> ( ( X C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) -> E. y e. B X = ( M ` y ) ) )
33 1 4 2 pmapssat 
 |-  ( ( K e. HL /\ y e. B ) -> ( M ` y ) C_ ( Atoms ` K ) )
34 1 2 5 2polpmapN 
 |-  ( ( K e. HL /\ y e. B ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( M ` y ) ) ) = ( M ` y ) )
35 sseq1 
 |-  ( X = ( M ` y ) -> ( X C_ ( Atoms ` K ) <-> ( M ` y ) C_ ( Atoms ` K ) ) )
36 2fveq3 
 |-  ( X = ( M ` y ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( M ` y ) ) ) )
37 id 
 |-  ( X = ( M ` y ) -> X = ( M ` y ) )
38 36 37 eqeq12d 
 |-  ( X = ( M ` y ) -> ( ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X <-> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( M ` y ) ) ) = ( M ` y ) ) )
39 35 38 anbi12d 
 |-  ( X = ( M ` y ) -> ( ( X C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) <-> ( ( M ` y ) C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( M ` y ) ) ) = ( M ` y ) ) ) )
40 39 biimprcd 
 |-  ( ( ( M ` y ) C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( M ` y ) ) ) = ( M ` y ) ) -> ( X = ( M ` y ) -> ( X C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) ) )
41 33 34 40 syl2anc 
 |-  ( ( K e. HL /\ y e. B ) -> ( X = ( M ` y ) -> ( X C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) ) )
42 41 rexlimdva 
 |-  ( K e. HL -> ( E. y e. B X = ( M ` y ) -> ( X C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) ) )
43 32 42 impbid 
 |-  ( K e. HL -> ( ( X C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) <-> E. y e. B X = ( M ` y ) ) )
44 6 43 bitrd 
 |-  ( K e. HL -> ( X e. C <-> E. y e. B X = ( M ` y ) ) )