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 ) ) )