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 ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
polsubsp.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
polsubsp.p ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
Assertion polsubN ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝑆 )

Proof

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