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 𝐴 = ( Atoms ‘ 𝐾 )
polsubcl.p = ( ⊥𝑃𝐾 )
polsubcl.c 𝐶 = ( PSubCl ‘ 𝐾 )
Assertion polsubclN ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) → ( 𝑋 ) ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 polsubcl.a 𝐴 = ( Atoms ‘ 𝐾 )
2 polsubcl.p = ( ⊥𝑃𝐾 )
3 polsubcl.c 𝐶 = ( PSubCl ‘ 𝐾 )
4 eqid ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
5 eqid ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
6 eqid ( pmap ‘ 𝐾 ) = ( pmap ‘ 𝐾 )
7 4 5 1 6 2 polval2N ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) → ( 𝑋 ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ) )
8 hlop ( 𝐾 ∈ HL → 𝐾 ∈ OP )
9 8 adantr ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) → 𝐾 ∈ OP )
10 hlclat ( 𝐾 ∈ HL → 𝐾 ∈ CLat )
11 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12 11 1 atssbase 𝐴 ⊆ ( Base ‘ 𝐾 )
13 sstr ( ( 𝑋𝐴𝐴 ⊆ ( Base ‘ 𝐾 ) ) → 𝑋 ⊆ ( Base ‘ 𝐾 ) )
14 12 13 mpan2 ( 𝑋𝐴𝑋 ⊆ ( Base ‘ 𝐾 ) )
15 11 4 clatlubcl ( ( 𝐾 ∈ CLat ∧ 𝑋 ⊆ ( Base ‘ 𝐾 ) ) → ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
16 10 14 15 syl2an ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) → ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
17 11 5 opoccl ( ( 𝐾 ∈ OP ∧ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐾 ) )
18 9 16 17 syl2anc ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐾 ) )
19 11 6 3 pmapsubclN ( ( 𝐾 ∈ HL ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ) ∈ 𝐶 )
20 18 19 syldan ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ) ∈ 𝐶 )
21 7 20 eqeltrd ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) → ( 𝑋 ) ∈ 𝐶 )