Metamath Proof Explorer

Theorem polsubN

Description: The polarity of a set of atoms is a projective subspace. (Contributed by NM, 23-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses polsubsp.a ⊢ A = Atoms ⁡ K
polsubsp.s ⊢ S = PSubSp ⁡ K
polsubsp.p ⊢ ⊥ ˙ = ⊥ 𝑃 ⁡ K
Assertion polsubN ⊢ K ∈ HL ∧ X ⊆ A → ⊥ ˙ ⁡ X ∈ S

Proof

Step Hyp Ref Expression
1 polsubsp.a ⊢ A = Atoms ⁡ K
2 polsubsp.s ⊢ S = PSubSp ⁡ K
3 polsubsp.p ⊢ ⊥ ˙ = ⊥ 𝑃 ⁡ K
4 eqid ⊢ lub ⁡ K = lub ⁡ K
5 eqid ⊢ oc ⁡ K = oc ⁡ K
6 eqid ⊢ pmap ⁡ K = pmap ⁡ K
7 4 5 1 6 3 polval2N ⊢ K ∈ HL ∧ X ⊆ A → ⊥ ˙ ⁡ X = pmap ⁡ K ⁡ oc ⁡ K ⁡ lub ⁡ K ⁡ X
8 hllat ⊢ K ∈ HL → K ∈ Lat
9 8 adantr ⊢ K ∈ HL ∧ X ⊆ A → K ∈ Lat
10 hlop ⊢ K ∈ HL → K ∈ OP
11 10 adantr ⊢ K ∈ HL ∧ X ⊆ A → K ∈ OP
12 hlclat ⊢ K ∈ HL → K ∈ CLat
13 eqid ⊢ Base K = Base K
14 13 1 atssbase ⊢ A ⊆ Base K
15 sstr ⊢ X ⊆ A ∧ A ⊆ Base K → X ⊆ Base K
16 14 15 mpan2 ⊢ X ⊆ A → X ⊆ Base K
17 13 4 clatlubcl ⊢ K ∈ CLat ∧ X ⊆ Base K → lub ⁡ K ⁡ X ∈ Base K
18 12 16 17 syl2an ⊢ K ∈ HL ∧ X ⊆ A → lub ⁡ K ⁡ X ∈ Base K
19 13 5 opoccl ⊢ K ∈ OP ∧ lub ⁡ K ⁡ X ∈ Base K → oc ⁡ K ⁡ lub ⁡ K ⁡ X ∈ Base K
20 11 18 19 syl2anc ⊢ K ∈ HL ∧ X ⊆ A → oc ⁡ K ⁡ lub ⁡ K ⁡ X ∈ Base K
21 13 2 6 pmapsub ⊢ K ∈ Lat ∧ oc ⁡ K ⁡ lub ⁡ K ⁡ X ∈ Base K → pmap ⁡ K ⁡ oc ⁡ K ⁡ lub ⁡ K ⁡ X ∈ S
22 9 20 21 syl2anc ⊢ K ∈ HL ∧ X ⊆ A → pmap ⁡ K ⁡ oc ⁡ K ⁡ lub ⁡ K ⁡ X ∈ S
23 7 22 eqeltrd ⊢ K ∈ HL ∧ X ⊆ A → ⊥ ˙ ⁡ X ∈ S