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 ⊢ Base K = Base K
11 10 1 atbase ⊢ p ∈ A → p ∈ Base K
12 eqid ⊢ ≤ K = ≤ K
13 eqid ⊢ 1. ⁡ K = 1. ⁡ K
14 10 12 13 ople1 ⊢ K ∈ OP ∧ p ∈ Base K → p ≤ K 1. ⁡ K
15 9 11 14 syl2an ⊢ K ∈ HL ∧ p ∈ A → p ≤ K 1. ⁡ K
16 15 ralrimiva ⊢ K ∈ HL → ∀ p ∈ A p ≤ K 1. ⁡ K
17 rabid2 ⊢ A = p ∈ A | p ≤ K 1. ⁡ K ↔ ∀ p ∈ A p ≤ K 1. ⁡ K
18 16 17 sylibr ⊢ K ∈ HL → A = p ∈ A | p ≤ K 1. ⁡ K
19 18 fveq2d ⊢ K ∈ HL → lub ⁡ K ⁡ A = lub ⁡ K ⁡ p ∈ A | p ≤ K 1. ⁡ K
20 hlomcmat ⊢ K ∈ HL → K ∈ OML ∧ K ∈ CLat ∧ K ∈ AtLat
21 10 13 op1cl ⊢ K ∈ OP → 1. ⁡ K ∈ Base K
22 9 21 syl ⊢ K ∈ HL → 1. ⁡ K ∈ Base K
23 10 12 4 1 atlatmstc ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ AtLat ∧ 1. ⁡ K ∈ Base K → lub ⁡ K ⁡ p ∈ A | p ≤ K 1. ⁡ K = 1. ⁡ K
24 20 22 23 syl2anc ⊢ K ∈ HL → lub ⁡ K ⁡ p ∈ A | p ≤ K 1. ⁡ 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 = ∅