Metamath Proof Explorer

Theorem pol1N

Description: The polarity of the whole projective subspace is the empty space. Remark in Holland95 p. 223. (Contributed by NM, 24-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses polssat.a ⊢A=Atoms⁡K
polssat.p ⊢⊥˙=⊥𝑃⁡K
Assertion pol1N ⊢K∈HL→⊥˙⁡A=∅

Proof

Step Hyp Ref Expression
1 polssat.a ⊢A=Atoms⁡K
2 polssat.p ⊢⊥˙=⊥𝑃⁡K
3 ssid ⊢A⊆A
4 eqid ⊢lub⁡K=lub⁡K
5 eqid ⊢oc⁡K=oc⁡K
6 eqid ⊢pmap⁡K=pmap⁡K
7 4 5 1 6 2 polval2N ⊢K∈HL∧A⊆A→⊥˙⁡A=pmap⁡K⁡oc⁡K⁡lub⁡K⁡A
8 3 7 mpan2 ⊢K∈HL→⊥˙⁡A=pmap⁡K⁡oc⁡K⁡lub⁡K⁡A
9 hlop ⊢K∈HL→K∈OP
10 eqid ⊢BaseK=BaseK
11 10 1 atbase ⊢p∈A→p∈BaseK
12 eqid ⊢≤K=≤K
13 eqid ⊢1.⁡K=1.⁡K
14 10 12 13 ople1 ⊢K∈OP∧p∈BaseK→p≤K1.⁡K
15 9 11 14 syl2an ⊢K∈HL∧p∈A→p≤K1.⁡K
16 15 ralrimiva ⊢K∈HL→∀p∈Ap≤K1.⁡K
17 rabid2 ⊢A=p∈A|p≤K1.⁡K↔∀p∈Ap≤K1.⁡K
18 16 17 sylibr ⊢K∈HL→A=p∈A|p≤K1.⁡K
19 18 fveq2d ⊢K∈HL→lub⁡K⁡A=lub⁡K⁡p∈A|p≤K1.⁡K
20 hlomcmat ⊢K∈HL→K∈OML∧K∈CLat∧K∈AtLat
21 10 13 op1cl ⊢K∈OP→1.⁡K∈BaseK
22 9 21 syl ⊢K∈HL→1.⁡K∈BaseK
23 10 12 4 1 atlatmstc ⊢K∈OML∧K∈CLat∧K∈AtLat∧1.⁡K∈BaseK→lub⁡K⁡p∈A|p≤K1.⁡K=1.⁡K
24 20 22 23 syl2anc ⊢K∈HL→lub⁡K⁡p∈A|p≤K1.⁡K=1.⁡K
25 19 24 eqtr2d ⊢K∈HL→1.⁡K=lub⁡K⁡A
26 25 fveq2d ⊢K∈HL→oc⁡K⁡1.⁡K=oc⁡K⁡lub⁡K⁡A
27 eqid ⊢0.⁡K=0.⁡K
28 27 13 5 opoc1 ⊢K∈OP→oc⁡K⁡1.⁡K=0.⁡K
29 9 28 syl ⊢K∈HL→oc⁡K⁡1.⁡K=0.⁡K
30 26 29 eqtr3d ⊢K∈HL→oc⁡K⁡lub⁡K⁡A=0.⁡K
31 30 fveq2d ⊢K∈HL→pmap⁡K⁡oc⁡K⁡lub⁡K⁡A=pmap⁡K⁡0.⁡K
32 hlatl ⊢K∈HL→K∈AtLat
33 27 6 pmap0 ⊢K∈AtLat→pmap⁡K⁡0.⁡K=∅
34 32 33 syl ⊢K∈HL→pmap⁡K⁡0.⁡K=∅
35 8 31 34 3eqtrd ⊢K∈HL→⊥˙⁡A=∅