Metamath Proof Explorer

Theorem polsubclN

Description: A polarity is a closed projective subspace. (Contributed by NM, 24-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses polsubcl.a ⊢ A = Atoms ⁡ K
polsubcl.p ⊢ ⊥ ˙ = ⊥ 𝑃 ⁡ K
polsubcl.c ⊢ C = PSubCl ⁡ K
Assertion polsubclN ⊢ K ∈ HL ∧ X ⊆ A → ⊥ ˙ ⁡ X ∈ C

Proof

Step Hyp Ref Expression
1 polsubcl.a ⊢ A = Atoms ⁡ K
2 polsubcl.p ⊢ ⊥ ˙ = ⊥ 𝑃 ⁡ K
3 polsubcl.c ⊢ C = PSubCl ⁡ K
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 ∧ X ⊆ A → ⊥ ˙ ⁡ X = pmap ⁡ K ⁡ oc ⁡ K ⁡ lub ⁡ K ⁡ X
8 hlop ⊢ K ∈ HL → K ∈ OP
9 8 adantr ⊢ K ∈ HL ∧ X ⊆ A → K ∈ OP
10 hlclat ⊢ K ∈ HL → K ∈ CLat
11 eqid ⊢ Base K = Base K
12 11 1 atssbase ⊢ A ⊆ Base K
13 sstr ⊢ X ⊆ A ∧ A ⊆ Base K → X ⊆ Base K
14 12 13 mpan2 ⊢ X ⊆ A → X ⊆ Base K
15 11 4 clatlubcl ⊢ K ∈ CLat ∧ X ⊆ Base K → lub ⁡ K ⁡ X ∈ Base K
16 10 14 15 syl2an ⊢ K ∈ HL ∧ X ⊆ A → lub ⁡ K ⁡ X ∈ Base K
17 11 5 opoccl ⊢ K ∈ OP ∧ lub ⁡ K ⁡ X ∈ Base K → oc ⁡ K ⁡ lub ⁡ K ⁡ X ∈ Base K
18 9 16 17 syl2anc ⊢ K ∈ HL ∧ X ⊆ A → oc ⁡ K ⁡ lub ⁡ K ⁡ X ∈ Base K
19 11 6 3 pmapsubclN ⊢ K ∈ HL ∧ oc ⁡ K ⁡ lub ⁡ K ⁡ X ∈ Base K → pmap ⁡ K ⁡ oc ⁡ K ⁡ lub ⁡ K ⁡ X ∈ C
20 18 19 syldan ⊢ K ∈ HL ∧ X ⊆ A → pmap ⁡ K ⁡ oc ⁡ K ⁡ lub ⁡ K ⁡ X ∈ C
21 7 20 eqeltrd ⊢ K ∈ HL ∧ X ⊆ A → ⊥ ˙ ⁡ X ∈ C